Skip to content

Commit 7675e1c

Browse files
author
Remi Delmas
committed
CONTRACTS: requires_contract/ensures_contract tests
1 parent 73198ac commit 7675e1c

File tree

4 files changed

+168
-0
lines changed

4 files changed

+168
-0
lines changed

‎regression/contracts-dfcc/function-pointer-contracts-enforce-1/main.c

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
#include <assert.h>
2+
#include <stdbool.h>
3+
#include <stdlib.h>
4+
5+
typedef int (*fun_t)(int);
6+
7+
int add_one(int x)
8+
__CPROVER_ensures(__CPROVER_return_value == __CPROVER_old(x) + 1);
9+
10+
int foo(fun_t f_in, int x, fun_t *f_out)
11+
// clang-format off
12+
__CPROVER_requires_contract(f_in, add_one, NULL)
13+
__CPROVER_assigns(f_out)
14+
__CPROVER_ensures(f_in ==>__CPROVER_return_value == __CPROVER_old(x) + 1)
15+
__CPROVER_ensures(!f_in ==>__CPROVER_return_value == __CPROVER_old(x))
16+
__CPROVER_ensures_contract(*f_out, add_one, NULL)
17+
// clang-format on
18+
{
19+
*f_out = NULL;
20+
if(f_in)
21+
{
22+
*f_out = f_in;
23+
// this branch must be reachable
24+
__CPROVER_assert(false, "then branch is reachable, expecting FAILURE");
25+
CALL_F_IN:
26+
return f_in(x);
27+
}
28+
else
29+
{
30+
// this branch must be reachable
31+
__CPROVER_assert(false, "else branch is reachable, expecting FAILURE");
32+
return x;
33+
}
34+
}
35+
36+
int main()
37+
{
38+
fun_t f_in;
39+
int x;
40+
fun_t f_out;
41+
foo(f_in, x, &f_out);
42+
if(f_out)
43+
{
44+
__CPROVER_assert(false, "then branch is reachable, expecting FAILURE");
45+
CALL_F_OUT:
46+
__CPROVER_assert(f_out(1) == 2, "f_out satisfies add_one");
47+
}
48+
else
49+
{
50+
__CPROVER_assert(false, "else branch is reachable, expecting FAILURE");
51+
}
52+
}

‎regression/contracts-dfcc/function-pointer-contracts-enforce-1/test.desc

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
CORE
2+
main.c
3+
--restrict-function-pointer foo.CALL_F_IN/add_one --restrict-function-pointer main.CALL_F_OUT/add_one --dfcc main --enforce-contract foo
4+
main.c function foo
5+
^\[foo.postcondition.\d+\] line 14 Check ensures clause of contract contract::foo for function foo: SUCCESS$
6+
^\[foo.postcondition.\d+\] line 15 Check ensures clause of contract contract::foo for function foo: SUCCESS$
7+
^\[foo.postcondition.\d+\] line 16 Assert function pointer '\*f_out_wrapper' obeys contract 'add_one' or '\(fun_t\)NULL': SUCCESS$
8+
^\[foo.assigns.\d+\] line 19 Check that \*f_out is assignable: FAILURE$
9+
^\[foo.assigns.\d+\] line 22 Check that \*f_out is assignable: FAILURE$
10+
^\[foo.assertion.\d+\] line 24 then branch is reachable, expecting FAILURE: FAILURE$
11+
^\[foo.pointer_dereference.\d+\] line 26 dereferenced function pointer must be add_one: SUCCESS$
12+
^\[foo.assertion.\d+\] line 31 else branch is reachable, expecting FAILURE: FAILURE$
13+
^\[main.assertion.\d+\] line 44 then branch is reachable, expecting FAILURE: FAILURE$
14+
^\[main.assertion.\d+\] line 46 f_out satisfies add_one: SUCCESS$
15+
^\[main.pointer_dereference.\d+\] line 46 dereferenced function pointer must be add_one: SUCCESS$
16+
^\[main.assertion.\d+\] line 50 else branch is reachable, expecting FAILURE: FAILURE$
17+
^VERIFICATION FAILED$
18+
^EXIT=10$
19+
^SIGNAL=0$
20+
--
21+
--
22+
foo requires that function pointer f_in satisfies the contract add_one or is NULL.
23+
When f_in is not NULL, foo calls f_in and the post condition of foo is that
24+
of add_one `__CPROVER_return_value == old(x) + 1`.
25+
When f_in is not NULL, foo returns x directly post condition of foo is that
26+
of add_one `__CPROVER_return_value == old(x)`.
27+
The function pointer f_out is ensured to satisfy the add_one contract or be NULL
28+
as a post condition.
29+
The main program calls f_out on a particular value if it is not null and asserts
30+
that the add_one post condition holds for a particular value.
31+
Assertions `assert(false)` are added to all branches to demonstrate reachability.

‎regression/contracts-dfcc/function-pointer-contracts-replace-1/main.c

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
#include <assert.h>
2+
#include <stdbool.h>
3+
#include <stdlib.h>
4+
5+
typedef int (*fun_t)(int);
6+
7+
int add_one(int x)
8+
__CPROVER_ensures(__CPROVER_return_value == __CPROVER_old(x) + 1);
9+
10+
// returns either a pointer to a function that satisfies add_one or NULL
11+
fun_t get_add_one()
12+
__CPROVER_ensures_contract(__CPROVER_return_value, add_one, NULL);
13+
14+
int foo(int x, fun_t *f_out)
15+
// clang-format off
16+
__CPROVER_assigns(*f_out)
17+
__CPROVER_ensures(
18+
__CPROVER_return_value == __CPROVER_old(x) + 1 ||
19+
__CPROVER_return_value == __CPROVER_old(x))
20+
__CPROVER_ensures_contract(*f_out, add_one, NULL)
21+
// clang-format on
22+
{
23+
*f_out = NULL;
24+
// obtain a pointer to a function that satisfies add_one;
25+
fun_t f_in = get_add_one();
26+
if(f_in)
27+
{
28+
*f_out = f_in;
29+
// this branch must be reachable
30+
__CPROVER_assert(false, "then branch is reachable, expecting FAILURE");
31+
CALL_F_IN:
32+
return f_in(x);
33+
}
34+
else
35+
{
36+
// this branch must be reachable
37+
__CPROVER_assert(false, "else branch is reachable, expecting FAILURE");
38+
return x;
39+
}
40+
}
41+
42+
int main()
43+
{
44+
int x;
45+
fun_t f_out;
46+
foo(x, &f_out);
47+
if(f_out)
48+
{
49+
__CPROVER_assert(false, "then branch is reachable, expecting FAILURE");
50+
CALL_F_OUT:
51+
__CPROVER_assert(f_out(1) == 2, "f_out satisfies add_one");
52+
}
53+
else
54+
{
55+
__CPROVER_assert(false, "else branch is reachable, expecting FAILURE");
56+
}
57+
}

‎regression/contracts-dfcc/function-pointer-contracts-replace-1/test.desc

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
CORE
2+
main.c
3+
--restrict-function-pointer foo.CALL_F_IN/add_one --restrict-function-pointer main.CALL_F_OUT/add_one --dfcc main --enforce-contract foo --replace-call-with-contract get_add_one
4+
^\[foo.postcondition.\d+\] line 18 Check ensures clause of contract contract::foo for function foo: SUCCESS$
5+
^\[foo.postcondition.\d+\] line 20 Assert function pointer '\*f_out_wrapper' obeys contract 'add_one' or '\(fun_t\)NULL': SUCCESS$
6+
^\[foo.assertion.\d+\] line 30 then branch is reachable, expecting FAILURE: FAILURE$
7+
^\[foo.pointer_dereference.\d+\] line 32 dereferenced function pointer must be add_one: SUCCESS$
8+
^\[foo.assertion.\d+\] line 37 else branch is reachable, expecting FAILURE: FAILURE$
9+
^\[main.assertion.\d+\] line 49 then branch is reachable, expecting FAILURE: FAILURE$
10+
^\[main.assertion.\d+\] line 51 f_out satisfies add_one: SUCCESS$
11+
^\[main.pointer_dereference.\d+\] line 51 dereferenced function pointer must be add_one: SUCCESS$
12+
^\[main.assertion.\d+\] line 55 else branch is reachable, expecting FAILURE: FAILURE$
13+
^VERIFICATION FAILED$
14+
^EXIT=10$
15+
^SIGNAL=0$
16+
--
17+
--
18+
foo obtains function pointer f_in through get_add_one, which is replaced by
19+
its contract.
20+
When f_in is not NULL, foo calls f_in and the post condition of foo is that
21+
of add_one `__CPROVER_return_value == old(x) + 1`.
22+
When f_in is not NULL, foo returns x directly post condition of foo is that
23+
of add_one `__CPROVER_return_value == old(x)`.
24+
The function pointer f_out is ensured to satisfy the add_one contract or be NULL
25+
as a post condition.
26+
The main program calls f_out on a particular value if it is not null and asserts
27+
that the add_one post condition holds for a particular value.
28+
Assertions `assert(false)` are added to all branches to demonstrate reachability.

0 commit comments

Comments
 (0)