Add tests to cover variables entering scope via goto

Author: thomasspriggs

regression/cbmc/declaration-goto/issue7997.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+extern void __VERIFIER_assume(int cond);
+extern int __VERIFIER_nondet_int(void);
+
+int main(void)
+{
+  if(__VERIFIER_nondet_int())
+    goto switch_2_1;
+  int tmp_ndt_4 = __VERIFIER_nondet_int();
+  __VERIFIER_assume(__VERIFIER_nondet_int());
+  __VERIFIER_assume(tmp_ndt_4 == 1);
+switch_2_1:
+  assert(tmp_ndt_4 > 0);
+  return 0;
+}

regression/cbmc/declaration-goto/issue7997.desc

@@ -0,0 +1,12 @@
+CORE
+issue7997.c
+--trace
+\[main\.assertion\.1\] line \d+ assertion tmp_ndt_4 \> 0\: FAILURE
+return_value___VERIFIER_nondet_int=[1-9]\d*
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+The assertion should be falsifiable when `goto switch_2_1` introduces
+`tmp_ndt_4` to the scope without initialising it.

regression/cbmc/declaration-goto/multiple_goto_single_label.c

@@ -0,0 +1,29 @@
+#include <assert.h>
+
+extern void __VERIFIER_assume(int cond);
+
+int main(void)
+{
+  int l = 2;
+  int if_condition1;
+  if(if_condition1)
+  {
+    unsigned int j = 42;
+    l = 3;
+    goto merge_point;
+  }
+  int if_condition2;
+  if(if_condition2)
+  {
+    l = 4;
+    unsigned int k = 24;
+    goto merge_point;
+  }
+  int i = 3;
+  int m = 9;
+
+merge_point:
+  assert(i == 3 || m == 9 || l == 3);
+  assert(i == 3 || m == 9 || l == 4);
+  return 0;
+}

regression/cbmc/declaration-goto/multiple_goto_single_label.desc

@@ -0,0 +1,12 @@
+CORE
+multiple_goto_single_label.c
+
+\[main\.assertion\.1\] line \d+ assertion i \=\= 3 \|\| m \=\= 9 \|\| l \=\= 3\: FAILURE
+\[main\.assertion\.2\] line \d+ assertion i \=\= 3 \|\| m \=\= 9 \|\| l \=\= 4\: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Test for the case where there are multiple gotos which target the same label
+and both introduce variables into the scope.

regression/cbmc/declaration-goto/re-enter_scope.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+
+extern void __VERIFIER_assume(int cond);
+
+int main(void)
+{
+  int if_condition;
+  if(if_condition)
+  {
+    unsigned int i = 42;
+    goto j_scope;
+  i_scope:
+    assert(i == 42);
+    return 0;
+  }
+  int j = 3;
+  assert(j == 3);
+
+j_scope:
+  assert(j == 3);
+  if(if_condition)
+    goto i_scope;
+  return 0;
+}

regression/cbmc/declaration-goto/re-enter_scope.desc

@@ -0,0 +1,13 @@
+CORE
+re-enter_scope.c
+
+\[main\.assertion\.1\] line 13 assertion i \=\= 42\: FAILURE
+\[main\.assertion\.2\] line 17 assertion j \=\= 3\: SUCCESS
+\[main\.assertion\.3\] line 20 assertion j \=\= 3\: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Test that if execution re-enters a scope via a goto the pre-existing variable
+becomes non-det.