Skip checking frame conditions for local variables

It avoids unnecessary assertions (improving performance) and
it prevents cases where memory primitives are invoked with dead objects.

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

Author: feliperodri

regression/contracts/assigns_enforce_16/main.c

@@ -0,0 +1,16 @@
+void foo(int *xp) __CPROVER_assigns(*xp)
+{
+  {
+    int y;
+    y = 2;
+  }
+  int z = 3;
+  *xp = 1;
+}
+
+int main()
+{
+  int *xp = malloc(sizeof(*xp));
+  foo(xp);
+  return 0;
+}

regression/contracts/assigns_enforce_16/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether verification fails when enforcing a contract
+for functions, without assigns clauses, that modify an input.

regression/contracts/assigns_enforce_scoping_01/test.desc

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

regression/contracts/assigns_type_checking_valid_cases/test.desc

@@ -5,6 +5,7 @@ main.c
 ^SIGNAL=0$
 ^\[foo1.\d+\] line \d+ Check that a is assignable: SUCCESS$
 ^\[foo10.\d+\] line \d+ Check that buffer\-\>len is assignable: SUCCESS$
+^\[foo10.\d+\] line \d+ Check that buffer\-\>aux\.allocated is assignable: SUCCESS$
 ^\[foo2.\d+\] line \d+ Check that b is assignable: SUCCESS$
 ^\[foo3.\d+\] line \d+ Check that b is assignable: SUCCESS$
 ^\[foo3.\d+\] line \d+ Check that y is assignable: SUCCESS$
@@ -27,7 +28,6 @@ main.c
 ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)7\] is assignable: SUCCESS$
 ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)8\] is assignable: SUCCESS$
 ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)9\] is assignable: SUCCESS$
-^\[foo9.\d+\] line \d+ Check that new_array is assignable: SUCCESS$
 ^\[foo9.\d+\] line \d+ Check that array is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --

regression/contracts/function-calls-05/test.desc

@@ -4,7 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
-\[foo.\d+\] line \d+ Check that sum is assignable: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion foo\(\&x, \&y\) \=\= 10: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --

regression/contracts/history-pointer-enforce-10/test.desc

@@ -7,8 +7,6 @@ main.c
 ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause\: SUCCESS$
 ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause\: SUCCESS$
 ^\[bar.\d+\] line \d+ Check that p\-\>y is assignable\: SUCCESS$
-^\[baz.\d+\] line \d+ Check that pp is assignable\: SUCCESS$
-^\[baz.\d+\] line \d+ Check that empty is assignable\: SUCCESS$
 ^\[baz.\d+\] line \d+ Check that p is assignable\: SUCCESS$
 ^\[baz.\d+\] line \d+ Check that p is assignable\: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*p\-\>y is assignable\: SUCCESS$

regression/contracts/quantifiers-exists-requires-enforce/test.desc

@@ -4,10 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
-^\[f1.\d+\] line \d+ Check that found\_four is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that found\_four is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/contracts/quantifiers-forall-ensures-enforce/test.desc

@@ -4,8 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
-^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
 ^\[f1.\d+\] line \d+ Check that arr\[\(.*\)i\] is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --

regression/contracts/quantifiers-forall-requires-enforce/test.desc

@@ -4,10 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
-^\[f1.\d+\] line \d+ Check that is\_identity is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that is\_identity is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/contracts/test_array_memory_enforce/test.desc

@@ -7,7 +7,6 @@ main.c
 \[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS
 \[foo.\d+\] line \d+ Check that x\[\(.* int\)5\] is assignable: SUCCESS
 \[foo.\d+\] line \d+ Check that x\[\(.* int\)9\] is assignable: SUCCESS
-\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
 --