diff --git a/tests/value/oracle/switch.0.res.oracle b/tests/value/oracle/switch.0.res.oracle index d0f062ed39d0626f7af30855321b8f710011c91b..8350a6f7166baa800f5dbdd7c88114d1baa2a78e 100644 --- a/tests/value/oracle/switch.0.res.oracle +++ b/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 diff --git a/tests/value/oracle/switch.1.res.oracle b/tests/value/oracle/switch.1.res.oracle index d0f062ed39d0626f7af30855321b8f710011c91b..8350a6f7166baa800f5dbdd7c88114d1baa2a78e 100644 --- a/tests/value/oracle/switch.1.res.oracle +++ b/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 diff --git a/tests/value/switch.i b/tests/value/switch.i index 17032e4113066be95dc414702bfb7ef54d06529b..fb7661b209b4cd098cc1e13e3398d3e52627103a 100644 --- a/tests/value/switch.i +++ b/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; }