From 49e8e53396e5ad57a06fe709bfcdc2d159d36b98 Mon Sep 17 00:00:00 2001
From: Thomas Spriggs <thomas.spriggs@diffblue.com>
Date: Tue, 5 Dec 2023 21:20:57 +0000
Subject: [PATCH] Add tests to cover variables entering scope via goto

---
 regression/cbmc/declaration-goto/issue7997.c  | 16 ++++++++++
 .../cbmc/declaration-goto/issue7997.desc      | 12 ++++++++
 .../multiple_goto_single_label.c              | 29 +++++++++++++++++++
 .../multiple_goto_single_label.desc           | 12 ++++++++
 .../cbmc/declaration-goto/re-enter_scope.c    | 24 +++++++++++++++
 .../cbmc/declaration-goto/re-enter_scope.desc | 13 +++++++++
 6 files changed, 106 insertions(+)
 create mode 100644 regression/cbmc/declaration-goto/issue7997.c
 create mode 100644 regression/cbmc/declaration-goto/issue7997.desc
 create mode 100644 regression/cbmc/declaration-goto/multiple_goto_single_label.c
 create mode 100644 regression/cbmc/declaration-goto/multiple_goto_single_label.desc
 create mode 100644 regression/cbmc/declaration-goto/re-enter_scope.c
 create mode 100644 regression/cbmc/declaration-goto/re-enter_scope.desc

diff --git a/regression/cbmc/declaration-goto/issue7997.c b/regression/cbmc/declaration-goto/issue7997.c
new file mode 100644
index 00000000000..12be101de9b
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/declaration-goto/issue7997.desc b/regression/cbmc/declaration-goto/issue7997.desc
new file mode 100644
index 00000000000..5e08f943068
--- /dev/null
+++ b/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.
diff --git a/regression/cbmc/declaration-goto/multiple_goto_single_label.c b/regression/cbmc/declaration-goto/multiple_goto_single_label.c
new file mode 100644
index 00000000000..48e4a12c824
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/declaration-goto/multiple_goto_single_label.desc b/regression/cbmc/declaration-goto/multiple_goto_single_label.desc
new file mode 100644
index 00000000000..529bff11759
--- /dev/null
+++ b/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.
diff --git a/regression/cbmc/declaration-goto/re-enter_scope.c b/regression/cbmc/declaration-goto/re-enter_scope.c
new file mode 100644
index 00000000000..3a4eb043cc9
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/declaration-goto/re-enter_scope.desc b/regression/cbmc/declaration-goto/re-enter_scope.desc
new file mode 100644
index 00000000000..27d1f83f75d
--- /dev/null
+++ b/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.