Propagate write-set checks to sub-functions

regression/contracts/assigns_enforce_01/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_02/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract foo
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_03/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract f2 --enforce-contract f3
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_04/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract f2 --enforce-contract f3
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_05/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract f2 --enforce-contract f3
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[f1.1\] line \d+ .*: SUCCESS$

regression/contracts/assigns_enforce_06/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract f2 --enforce-contract f3
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_07/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract f2 --enforce-contract f3
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_08/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract f2
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_09/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract f2
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_10/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract f2
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_11/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract f2
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_12/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_13/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_14/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_15/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract foo --enforce-contract bar --enforce-contract baz --enforce-contract qux
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[bar\.1\] line \d+ .*: FAILURE$

regression/contracts/assigns_enforce_16/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts _ --pointer-primitive-check
+--enforce-contract foo _ --pointer-primitive-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_17/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract pure
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.\d+\] line \d+ assertion x \=\= 0: SUCCESS$

regression/contracts/assigns_enforce_18/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts _ --pointer-primitive-check
+--enforce-contract foo --enforce-contract bar --enforce-contract baz _ --pointer-primitive-check
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[bar.\d+\] line \d+ Check that \*a is assignable: SUCCESS$

regression/contracts/assigns_enforce_19/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f --enforce-contract g
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[f.\d+\] line \d+ Check that a is assignable: SUCCESS$

regression/contracts/assigns_enforce_20/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract foo
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[foo.\d+\] line \d+ Check that \*y is assignable: FAILURE$

regression/contracts/assigns_enforce_arrays_01/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_arrays_02/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract nextIdx
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_arrays_03/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract assign_out_under
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_arrays_04/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract assigns_single --enforce-contract assigns_range --enforce-contract assigns_big_range
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_arrays_05/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract assigns_ptr --enforce-contract assigns_range
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_arrays_10/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract nextIdx
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_functions_in_contracts/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_malloc_01/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_malloc_02/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1
 ^EXIT=6$
 ^SIGNAL=0$
 Unable to complete instrumentation, as this malloc may be in a loop.$

regression/contracts/assigns_enforce_multi_file_01/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract f2 --enforce-contract f3
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_multi_file_02/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_scoping_01/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[f1.\d+\] line \d+ Check that \*f1\$\$1\$\$1\$\$b is assignable: SUCCESS$

regression/contracts/assigns_enforce_scoping_02/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[f1.\d+\] line \d+ Check that \*f1\$\$1\$\$1\$\$b is assignable: SUCCESS$

regression/contracts/assigns_enforce_structs_01/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_structs_02/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_structs_03/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_structs_04/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract f2 --enforce-contract f3 --enforce-contract f4
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[f1.\d+\] line \d+ Check that p->y is assignable: FAILURE$

regression/contracts/assigns_enforce_structs_05/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[f1.\d+\] line \d+ Check that p->y is assignable: FAILURE$

regression/contracts/assigns_enforce_structs_06/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract f1 --enforce-contract f2 --enforce-contract f3
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$

regression/contracts/assigns_enforce_structs_07/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts _ --malloc-may-fail --malloc-fail-null --pointer-check
+--enforce-contract f1 --enforce-contract f2 _ --malloc-may-fail --malloc-fail-null --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$

regression/contracts/assigns_function_pointer/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract bar
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[bar.1\] line \d+ Check that fun\_ptr is assignable: SUCCESS$

regression/contracts/assigns_repeated_ignored/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--enforce-contract foo
 ^Ignored duplicate expression '\*x' in assigns clause at file main\.c line \d+$
 ^EXIT=0$
 ^SIGNAL=0$

regression/contracts/assigns_replace_01/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-all-calls-with-contracts
+--replace-call-with-contract foo
 ^EXIT=10$
 ^SIGNAL=0$
 assertion n == 7: FAILURE

regression/contracts/assigns_replace_02/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-all-calls-with-contracts
+--replace-call-with-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_replace_03/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-all-calls-with-contracts _ --pointer-primitive-check
+--replace-call-with-contract bar _ --pointer-primitive-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_replace_04/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-all-calls-with-contracts
+--replace-call-with-contract f2 --replace-call-with-contract f3
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_replace_05/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
---replace-all-calls-with-contracts
+--replace-call-with-contract f2 --replace-call-with-contract f3
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_replace_06/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-all-calls-with-contracts _ --pointer-primitive-check
+--replace-call-with-contract foo --replace-call-with-contract bar _ --pointer-primitive-check
 ^\[main.assertion.1\] line \d+ assertion b\[0\] == 'a': FAILURE$
 ^\[main.assertion.2\] line \d+ assertion b\[1\] == 'b': FAILURE$
 ^\[main.assertion.3\] line \d+ assertion b\[2\] == 'c': FAILURE$

regression/contracts/assigns_replace_07/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-all-calls-with-contracts _ --malloc-may-fail --malloc-fail-null --pointer-check
+--replace-call-with-contract f1 _ --malloc-may-fail --malloc-fail-null --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.\d+\] line \d+ assertion p == NULL \|\| p->buf\[0\] == 0: SUCCESS$