Merge pull request #6371 from feliperodri/propagate-assigns-checks

Propagate write-set checks to sub-functions

Author: feliperodri

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,9 +1,18 @@
 CORE
 main.c
---enforce-all-contracts
-^EXIT=10$
+--enforce-contract f1
+^EXIT=0$
 ^SIGNAL=0$
-^VERIFICATION FAILED$
+^\[f1.\d+\] line \d+ Check that x2 is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that y2 is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that z2 is assignable: SUCCESS$
+^\[f2.\d+\] line \d+ Check that x3 is assignable: SUCCESS$
+^\[f2.\d+\] line \d+ Check that y3 is assignable: SUCCESS$
+^\[f2.\d+\] line \d+ Check that z3 is assignable: SUCCESS$
+^\[f3.\d+\] line \d+ Check that \*x3 is assignable: SUCCESS$
+^\[f3.\d+\] line \d+ Check that \*y3 is assignable: SUCCESS$
+^\[f3.\d+\] line \d+ Check that \*z3 is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
 --
 --
-This test checks that verification fails when an assigns clause is not respected through multiple function calls.
+This test checks that verification only considers assigns clause from enforced function.

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$