[Eva] Adds a test of a goto statement skipping a local variable declaration.

tests/value/goto.i

+/* 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 ();
 }

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