Merge branch 'fix/eva/switch-test' into 'master'

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

See merge request frama-c/frama-c!4316

tests/value/oracle/switch.0.res.oracle

@@ -11,6 +11,9 @@
   result2 ∈ {7}
   d2 ∈ {0}
 [eva] switch.i:29: Frama_C_show_each_F: {0}
+[eva:alarm] switch.i:63: Warning: check 'unknown' got status unknown.
+[eva:alarm] switch.i:64: Warning: 
+  accessing uninitialized left-value. assert \initialized(&i);
 [eva] Recording results for main
 [eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -21,6 +24,7 @@
   result2 ∈ {0; 7}
   d2 ∈ [-0.0000000000000000 .. 1.9999999999999998*2^1023]
   f ∈ [--..--]
+  x ∈ {18} or UNINITIALIZED
   __retres ∈ {0; 2; 77}
 [from] Computing for function main
 [from] Done for function main
@@ -35,6 +39,6 @@
   \result FROM c
 [from] ====== END OF DEPENDENCIES ======
 [inout] Out (internal) for function main:
-    result1; result3; result4; result2; d2; f; __retres
+    result1; result3; result4; result2; d2; f; x; i; __retres
 [inout] Inputs for function main:
     \nothing

tests/value/oracle/switch.1.res.oracle

@@ -11,6 +11,9 @@
   result2 ∈ {7}
   d2 ∈ {0}
 [eva] switch.i:29: Frama_C_show_each_F: {0}
+[eva:alarm] switch.i:63: Warning: check 'unknown' got status unknown.
+[eva:alarm] switch.i:64: Warning: 
+  accessing uninitialized left-value. assert \initialized(&i);
 [eva] Recording results for main
 [eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -21,6 +24,7 @@
   result2 ∈ {0; 7}
   d2 ∈ [-0.0000000000000000 .. 1.9999999999999998*2^1023]
   f ∈ [--..--]
+  x ∈ {18} or UNINITIALIZED
   __retres ∈ {0; 2; 77}
 [from] Computing for function main
 [from] Done for function main
@@ -35,6 +39,6 @@
   \result FROM c
 [from] ====== END OF DEPENDENCIES ======
 [inout] Out (internal) for function main:
-    result1; result3; result4; result2; d2; f; __retres
+    result1; result3; result4; result2; d2; f; x; i; __retres
 [inout] Inputs for function main:
     \nothing

tests/value/switch.i

@@ -51,5 +51,18 @@ int main (int c, int d, int e, int f, double d1, long l) {
     case 0x0FFFFFFF: result4 = 1; break;
     case 0xFFFFFFFF: result4 = 2; break;
     }
+
+  int x;
+  /* This switch skips the declaration of variable i, as code between the
+     switch and the first case is not executed. */
+  switch(d) {
+    int i = 5; // dead code
+    case 0:
+      i = 17;
+    default:
+      //@ check unknown: i == 17;
+      x = i+1; // Initialization alarm: i may be uninitialized.
+  }
+
   return 77;
 }