Test whether frame conditions correctly consider scope

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

Author: feliperodri

regression/contracts/assigns_enforce_17/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int x = 0;
+
+void pure() __CPROVER_assigns()
+{
+  int x;
+  x++;
+}
+
+int main()
+{
+  pure();
+  assert(x == 0);
+  return 0;
+}

regression/contracts/assigns_enforce_17/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts _ --pointer-primitive-check
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.\d+\] line \d+ assertion x \=\= 0\: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether verification correctly distincts local variables
+and global variables with same name when checking frame conditions.