Inline sub-function calls

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

regression/contracts/assigns_enforce_04/test.desc

@@ -1,9 +1,18 @@
 CORE
 main.c
---enforce-contract f1 --enforce-contract f2 --enforce-contract f3
-^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_15/test.desc

@@ -1,11 +1,10 @@
 CORE
 main.c
---enforce-contract foo --enforce-contract bar --enforce-contract baz --enforce-contract qux
+--enforce-contract foo --enforce-contract baz --enforce-contract qux
 ^EXIT=10$
 ^SIGNAL=0$
-^\[bar\.1\] line \d+ .*: FAILURE$
-^\[baz\.1\] line \d+ .*: FAILURE$
-^\[qux\.1\] line \d+ .*: FAILURE$
+^\[baz.\d+\] line \d+ Check that global is assignable: FAILURE$
+^\[qux.\d+\] line \d+ Check that global is assignable: FAILURE$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/assigns_enforce_22/main.c

@@ -0,0 +1,41 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int x = 0;
+
+void quz() __CPROVER_assigns(x)
+{
+  x = -1;
+}
+
+int baz() __CPROVER_assigns()
+{
+  return 5;
+}
+
+void bar(int *y, int w) __CPROVER_assigns(*y)
+{
+  *y = 3;
+  w = baz();
+  quz();
+}
+
+void foo(int *y, int z) __CPROVER_assigns(*y)
+{
+  int w = 5;
+  assert(w == 5);
+  bar(y, w);
+  z = -2;
+}
+
+int main()
+{
+  int *y = malloc(sizeof(*y));
+  *y = 0;
+  int z = 1;
+  foo(y, z);
+  assert(x == -1);
+  assert(*y == 3);
+  assert(z == 1);
+  return 0;
+}

regression/contracts/assigns_enforce_22/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--enforce-contract foo
+^EXIT=10$
+^SIGNAL=0$
+main.c function bar
+^\[bar.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
+^\[baz.\d+\] line \d+ Check that w is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that w is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
+^\[quz.\d+\] line \d+ Check that x is assignable: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+Checks whether checks write set for sub-function calls.

regression/contracts/assigns_enforce_multi_file_01/test.desc

@@ -1,9 +1,9 @@
 CORE
 main.c
---enforce-contract f1 --enforce-contract f2 --enforce-contract f3
-^EXIT=10$
+--enforce-contract f1
+^EXIT=0$
 ^SIGNAL=0$
-^VERIFICATION FAILED$
+^VERIFICATION SUCCESSFUL$
 --
 --
 This test replicates the behavior of assigns_enforce_04, but separates

regression/contracts/assigns_validity_pointer_02/test.desc

@@ -4,9 +4,12 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
-^\[foo.\d+\] line \d+ Check that bar\'s assigns clause is a subset of foo\'s assigns clause: SUCCESS$
+^\[bar.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
+^\[bar.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
+^\[baz.\d+\] line \d+ Check that \*z is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that x is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that baz\'s assigns clause is a subset of foo\'s assigns clause: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: FAILURE$

regression/contracts/function-calls-03-1/test-enf.desc

@@ -1,16 +1,17 @@
 CORE
 main.c
---enforce-contract f1 --enforce-contract f2 _ --unwind 20 --unwinding-assertions
+--enforce-contract f1 _ --unwind 20 --unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
+^file main.c line \d+ function f2: recursion is ignored on call to \'f2\'$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
 Verification:
   function | pre-cond | post-cond
   ---------|----------|----------
   f1       | assumed  | asserted
-  f2       | assumed  | asserted
 
 Test should fail:
 The postcondition of f2 is incorrect, considering the recursion particularity. 

regression/contracts/function-calls-03/test-enf.desc

@@ -1,17 +1,17 @@
 CORE
 main.c
---enforce-contract f1 --enforce-contract f2_out --enforce-contract f2_in _ --unwind 20 --unwinding-assertions
+--enforce-contract f1 _ --unwind 20 --unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
+^file main.c line \d+ function f2\_in: recursion is ignored on call to \'f2\_out\'$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
 Verification:
   function | pre-cond | post-cond
   ---------|----------|----------
   f1       | assumed  | asserted
-  f2_out   | assumed  | asserted
-  f2_in    | assumed  | asserted
 
 Test should fail:
 The postcondition of f2 is incorrect, considering the recursion particularity.