From c0e0c0af5d7d139c5b3bed0752bce5fa84bdfd1c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 17 Jul 2023 11:33:07 +0200
Subject: [PATCH] [Eva] Adds a test of a goto statement skipping a local
 variable declaration.

---
 tests/value/goto.i                 | 23 +++++++++++++++++++++++
 tests/value/oracle/goto.res.oracle | 30 +++++++++++++++++++++++++++---
 2 files changed, 50 insertions(+), 3 deletions(-)

diff --git a/tests/value/goto.i b/tests/value/goto.i
index 9a2430a1ea5..d4f59d0f5f2 100644
--- a/tests/value/goto.i
+++ b/tests/value/goto.i
@@ -1,6 +1,28 @@
+/* run.config*
+  STDOPT: +""
+*/
+
+volatile int nondet;
+
 int stop () {
  L: goto L;
+}
 
+void skip_declaration(void) {
+  int y, r;
+  if (nondet) {
+    goto l; // This goto skips the declaration of variable x below.
+  }
+  int x = 1;
+  y = 2;
+  l: // x and y are both uninitialized when coming from the goto
+  //@ check unknown: \initialized(&x);
+  //@ check unknown: x > 0;
+  //@ check unknown: \initialized(&y);
+  //@ check unknown: y > 0;
+  r = x + 1; // An initialization alarm must be emitted.
+  r = y + 1; // An initialization alarm must be emitted.
+  return;
 }
 
 int main() {
@@ -9,4 +31,5 @@ int main() {
 
   if (c) stop ();
 
+  skip_declaration ();
 }
diff --git a/tests/value/oracle/goto.res.oracle b/tests/value/oracle/goto.res.oracle
index 0a9dd76826c..d258a57ce28 100644
--- a/tests/value/oracle/goto.res.oracle
+++ b/tests/value/oracle/goto.res.oracle
@@ -3,19 +3,37 @@
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
-  
+  nondet ∈ [--..--]
 [eva] computing for function stop <- main.
-  Called from goto.i:10.
+  Called from goto.i:32.
 [eva] Recording results for stop
 [eva] Done for function stop
+[eva] computing for function skip_declaration <- main.
+  Called from goto.i:34.
+[eva:alarm] goto.i:19: Warning: check 'unknown' got status unknown.
+[eva:alarm] goto.i:20: Warning: check 'unknown' got status unknown.
+[eva:alarm] goto.i:21: Warning: check 'unknown' got status unknown.
+[eva:alarm] goto.i:22: Warning: check 'unknown' got status unknown.
+[eva:alarm] goto.i:23: Warning: 
+  accessing uninitialized left-value. assert \initialized(&x);
+[eva:alarm] goto.i:24: Warning: 
+  accessing uninitialized left-value. assert \initialized(&y);
+[eva] Recording results for skip_declaration
+[eva] Done for function skip_declaration
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function skip_declaration:
+  y ∈ {2}
+  r ∈ {3}
+  x ∈ {1}
 [eva:final-states] Values at end of function stop:
   NON TERMINATING FUNCTION
 [eva:final-states] Values at end of function main:
   c ∈ [--..--]
   __retres ∈ {0}
+[from] Computing for function skip_declaration
+[from] Done for function skip_declaration
 [from] Computing for function stop
 [from] Non-terminating function stop (no dependencies)
 [from] Done for function stop
@@ -23,11 +41,17 @@
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
+[from] Function skip_declaration:
+  NO EFFECTS
 [from] Function stop:
   NON TERMINATING - NO EFFECTS
 [from] Function main:
   \result FROM \nothing
 [from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function skip_declaration:
+    y; r; x
+[inout] Inputs for function skip_declaration:
+    nondet
 [inout] Out (internal) for function stop:
     \nothing
 [inout] Inputs for function stop:
@@ -35,4 +59,4 @@
 [inout] Out (internal) for function main:
     c; __retres
 [inout] Inputs for function main:
-    \nothing
+    nondet
-- 
GitLab