Skip to content

Commit a5d0f97

Browse files
author
Remi Delmas
committed
CONTRACTS: dfcc_dsl_wrappert cleanup
- don't use pointers to symbols - use wrapper function location for all instructions - do not conjoin requires exprs - do not conjoin ensures exprs
1 parent d761684 commit a5d0f97

File tree

16 files changed

+430
-410
lines changed

16 files changed

+430
-410
lines changed

‎regression/contracts-dfcc/assigns_enforce_21/test.desc

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,7 @@
11
CORE
22
main.c
33
--dfcc main --enforce-contract foo --replace-call-with-contract quz
4-
^\[bar.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
5-
^\[quz.assigns.\d+\] Check that the assigns clause of contract::quz is included in the caller's assigns clause: FAILURE$
4+
^\[bar.assigns.\d+\].*Check that \*y is assignable: SUCCESS$
65
^VERIFICATION FAILED$
76
^EXIT=10$
87
^SIGNAL=0$

‎regression/contracts-dfcc/assigns_enforce_malloc_02/test.desc

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,6 @@ CORE
22
main.c
33
--dfcc main --enforce-contract f
44
main.c function f
5-
^\[f.postcondition.\d+\] line 3 Check ensures clause of contract contract::f for function f: SUCCESS$
65
^\[f.assigns.\d+\] line 7 Check that ptr is assignable: SUCCESS$
76
^\[f.assigns.\d+\] line 12 Check that \*ptr is assignable: SUCCESS$
87
^\[f.assigns.\d+\] line 13 Check that n is assignable: SUCCESS$

‎regression/contracts-dfcc/assigns_replace_08/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33
--dfcc main --enforce-contract foo --replace-call-with-contract bar _ --pointer-primitive-check
4-
^\[bar.assigns.\d+\] Check that the assigns clause of contract::bar is included in the caller's assigns clause: FAILURE$
4+
^\[bar.assigns.\d+\].*Check that the assigns clause of contract::bar is included in the caller's assigns clause: FAILURE$
55
^VERIFICATION FAILED$
66
^EXIT=10$
77
^SIGNAL=0$

‎regression/contracts-dfcc/assigns_replace_09/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--dfcc main --replace-call-with-contract bar --enforce-contract foo
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[bar.assigns.\d+\] Check that the assigns clause of contract::bar is included in the caller's assigns clause: SUCCESS$
6+
^\[bar.assigns.\d+\].*Check that the assigns clause of contract::bar is included in the caller's assigns clause: SUCCESS$
77
^VERIFICATION SUCCESSFUL$
88
--
99
--

‎regression/contracts-dfcc/assigns_replace_havoc_dependent_targets_fail/replace.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
main_replace.c
33
--dfcc main --replace-call-with-contract resize_vec --enforce-contract resize_vec_incr10 _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check
4-
^\[resize_vec.assigns.\d+\] Check that the assigns clause of contract::resize_vec is included in the caller's assigns clause: FAILURE$
5-
^\[resize_vec.frees.\d+\] Check that the frees clause of contract::resize_vec is included in the caller's frees clause: FAILURE$
4+
^\[resize_vec.assigns.\d+\].*Check that the assigns clause of contract::resize_vec is included in the caller's assigns clause: FAILURE$
5+
^\[resize_vec.frees.\d+\].*Check that the frees clause of contract::resize_vec is included in the caller's frees clause: FAILURE$
66
^VERIFICATION FAILED$
77
^EXIT=10$
88
^SIGNAL=0$

‎regression/contracts-dfcc/assigns_replace_havoc_dependent_targets_pass/replace.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
main_replace.c
33
--dfcc main --replace-call-with-contract resize_vec --enforce-contract resize_vec_incr10 _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check
4-
^\[resize_vec.assigns.\d+\] Check that the assigns clause of contract::resize_vec is included in the caller's assigns clause: SUCCESS$
5-
^\[resize_vec.frees.\d+\] Check that the frees clause of contract::resize_vec is included in the caller's frees clause: SUCCESS$
4+
^\[resize_vec.assigns.\d+\].*Check that the assigns clause of contract::resize_vec is included in the caller's assigns clause: SUCCESS$
5+
^\[resize_vec.frees.\d+\].*Check that the frees clause of contract::resize_vec is included in the caller's frees clause: SUCCESS$
66
^VERIFICATION SUCCESSFUL$
77
^EXIT=0$
88
^SIGNAL=0$

‎regression/contracts-dfcc/function-calls-03-direct-recursion/test-rec.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
CORE
22
main.c
33
--dfcc main --enforce-contract-rec f
4-
^\[f.postcondition.\d+\] .* Check ensures clause of contract contract::f for function f: SUCCESS$
5-
^\[f.precondition.\d+\] .* Check requires clause of contract contract::f for function f: SUCCESS$
6-
^\[f.assigns.\d+\] Check that the assigns clause of contract::f is included in the caller's assigns clause: SUCCESS$
7-
^\[f.frees.\d+\] Check that the frees clause of contract::f is included in the caller's frees clause: SUCCESS$
4+
^\[f.postcondition.\d+\].*Check ensures clause of contract contract::f for function f: SUCCESS$
5+
^\[f.precondition.\d+\].*Check requires clause of contract contract::f for function f: SUCCESS$
6+
^\[f.assigns.\d+\].*Check that the assigns clause of contract::f is included in the caller's assigns clause: SUCCESS$
7+
^\[f.frees.\d+\].*Check that the frees clause of contract::f is included in the caller's frees clause: SUCCESS$
88
^EXIT=0$
99
^SIGNAL=0$
1010
^VERIFICATION SUCCESSFUL$

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
CORE
22
main.c
33
--restrict-function-pointer foo.function_pointer_call.1/arr_fun_contract --dfcc main --enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract arr_fun_contract
4-
^\[arr_fun_contract.assigns.\d+\] Check that the assigns clause of contract::arr_fun_contract is included in the caller's assigns clause: SUCCESS$
5-
^\[arr_fun_contract.frees.\d+\] Check that the frees clause of contract::arr_fun_contract is included in the caller's frees clause: SUCCESS$
6-
^\[arr_fun_contract.precondition.\d+\] line 14 Check requires clause of contract contract::arr_fun_contract for function arr_fun_contract: SUCCESS$
4+
^\[arr_fun_contract.assigns.\d+\].*Check that the assigns clause of contract::arr_fun_contract is included in the caller's assigns clause: SUCCESS$
5+
^\[arr_fun_contract.frees.\d+\].*Check that the frees clause of contract::arr_fun_contract is included in the caller's frees clause: SUCCESS$
6+
^\[arr_fun_contract.precondition.\d+\].*Check requires clause of contract contract::arr_fun_contract for function arr_fun_contract: SUCCESS$
77
^EXIT=0$
88
^SIGNAL=0$
99
^VERIFICATION SUCCESSFUL$

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
CORE
22
main.c
33
--restrict-function-pointer foo.function_pointer_call.1/arr_fun_contract --dfcc main --enforce-contract foo --replace-call-with-contract bar
4-
^\[arr_fun_contract.assigns.\d+\] Check that the assigns clause of contract::arr_fun_contract is included in the caller's assigns clause: SUCCESS$
5-
^\[arr_fun_contract.frees.\d+\] Check that the frees clause of contract::arr_fun_contract is included in the caller's frees clause: SUCCESS$
6-
^\[arr_fun_contract.precondition.\d+\] line 14 Check requires clause of contract contract::arr_fun_contract for function arr_fun_contract: SUCCESS$
4+
^\[arr_fun_contract.assigns.\d+\].*Check that the assigns clause of contract::arr_fun_contract is included in the caller's assigns clause: SUCCESS$
5+
^\[arr_fun_contract.frees.\d+\].*Check that the frees clause of contract::arr_fun_contract is included in the caller's frees clause: SUCCESS$
6+
^\[arr_fun_contract.precondition.\d+\].*Check requires clause of contract contract::arr_fun_contract for function arr_fun_contract: SUCCESS$
77
^EXIT=0$
88
^SIGNAL=0$
99
^VERIFICATION SUCCESSFUL$

‎regression/contracts-dfcc/loop-freeness-check/test.desc

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
CORE
22
main.c
33
--dfcc main --enforce-contract foo
4-
^\[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: SUCCESS$
54
^\[foo.assigns.\d+\].*Check that i is assignable: SUCCESS$
65
^\[foo.assigns.\d+\].*Check that arr\[\(.*\)i\] is assignable: SUCCESS$
76
^VERIFICATION SUCCESSFUL$

‎regression/contracts-dfcc/test_is_fresh_replace_ensures_pass/test-replace.desc

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
CORE
22
main.c
33
--dfcc main --replace-call-with-contract foo
4-
^\[foo.precondition.\d+\].*Check requires clause of contract contract::foo for function foo: SUCCESS$
54
^\[main.assertion.\d+\].*out1 is rw_ok: SUCCESS$
65
^\[main.assertion.\d+\].*out2 is rw_ok: SUCCESS$
76
^\[main.assertion.\d+\].*out1 and out2 are not aliased: SUCCESS$

‎src/goto-instrument/contracts/dynamic-frames/dfcc_dsl_contract_handler.h

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,10 @@ class function_pointer_obeys_contract_exprt;
6161
///
6262
/// Translation results are cached so it is safe to call
6363
/// `get_contract_functions` several times.
64+
///
65+
/// This class also implements the \ref dfcc_contract_handlert interface
66+
/// and allows to generate instructions modelling contract checking and
67+
/// contract replacement.
6468
class dfcc_dsl_contract_handlert : public dfcc_contract_handlert
6569
{
6670
public:

0 commit comments

Comments
 (0)