diff --git a/tests/builtins/oracle/allocated.0.res.oracle b/tests/builtins/oracle/allocated.0.res.oracle index 9a9940ee92a7f051dba7f72784b2871d9cfe7882..53996c93021c6cccab5e34b52c79a0da159e8edb 100644 --- a/tests/builtins/oracle/allocated.0.res.oracle +++ b/tests/builtins/oracle/allocated.0.res.oracle @@ -233,34 +233,31 @@ [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc [eva:malloc] tests/builtins/allocated.c:127: resizing variable `__malloc_main_l127' (0..31/95) to fit 0..63/127 -[eva] tests/builtins/allocated.c:131: Frama_C_show_each: {0; 1; 2; 3} +[eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..2147483647] [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free [eva:malloc] tests/builtins/allocated.c:127: strong free on bases: {__malloc_main_l127} [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc [eva:malloc] tests/builtins/allocated.c:127: resizing variable `__malloc_main_l127' (0..31/127) to fit 0..63/159 -[eva] tests/builtins/allocated.c:131: Frama_C_show_each: {0; 1; 2; 3; 4} +[eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..2147483647] [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free [eva:malloc] tests/builtins/allocated.c:127: strong free on bases: {__malloc_main_l127} [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc [eva:malloc] tests/builtins/allocated.c:127: resizing variable `__malloc_main_l127' (0..31/159) to fit 0..63/191 -[eva] tests/builtins/allocated.c:131: Frama_C_show_each: {0; 1; 2; 3; 4; 5} +[eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..2147483647] [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free [eva:malloc] tests/builtins/allocated.c:127: strong free on bases: {__malloc_main_l127} [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc [eva:malloc] tests/builtins/allocated.c:127: resizing variable `__malloc_main_l127' (0..31/191) to fit 0..63/319 -[eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..9] +[eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..2147483647] [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free [eva:malloc] tests/builtins/allocated.c:127: strong free on bases: {__malloc_main_l127} -[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc -[eva:malloc] tests/builtins/allocated.c:127: - resizing variable `__malloc_main_l127' (0..31/319) to fit 0..63/319 [eva] Recording results for main [eva] done for function main [eva] tests/builtins/allocated.c:27: @@ -279,7 +276,8 @@ size ∈ [1..100] pb ∈ ESCAPINGADDR __retres ∈ {0} - __malloc_w_main_l82[0..2] ∈ [7..27] or UNINITIALIZED + __malloc_w_main_l82[0..1] ∈ [7..2147483647] or UNINITIALIZED + [2] ∈ [7..27] or UNINITIALIZED [from] Computing for function main [from] Computing for function malloc <-main [from] Done for function malloc diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle index 36bad43db983e76366739462388ea353314b6ce6..2c7e41c81de51023519cf04af34b7d44f3d10625 100644 --- a/tests/idct/oracle/ieee_1180_1990.res.oracle +++ b/tests/idct/oracle/ieee_1180_1990.res.oracle @@ -369,6 +369,8 @@ [eva] tests/idct/ieee_1180_1990.c:215: starting to merge loop iterations [eva] tests/idct/ieee_1180_1990.c:234: starting to merge loop iterations [eva] tests/idct/ieee_1180_1990.c:233: starting to merge loop iterations +[eva] tests/idct/ieee_1180_1990.c:235: Warning: + 2's complement assumed for overflow [eva] computing for function IEEE_1180_1990_dctf <- main. Called from tests/idct/ieee_1180_1990.c:236. [eva] Recording results for IEEE_1180_1990_dctf @@ -446,6 +448,8 @@ [eva] tests/idct/ieee_1180_1990.c:277: Warning: 2's complement assumed for overflow [eva] tests/idct/ieee_1180_1990.c:261: starting to merge loop iterations +[eva] tests/idct/ieee_1180_1990.c:281: Warning: + 2's complement assumed for overflow [eva] tests/idct/ieee_1180_1990.c:280: starting to merge loop iterations [eva] tests/idct/ieee_1180_1990.c:279: starting to merge loop iterations [eva] tests/idct/ieee_1180_1990.c:282: @@ -518,6 +522,8 @@ [eva] tests/idct/ieee_1180_1990.c:323: Warning: 2's complement assumed for overflow [eva] tests/idct/ieee_1180_1990.c:307: starting to merge loop iterations +[eva] tests/idct/ieee_1180_1990.c:327: Warning: + 2's complement assumed for overflow [eva] tests/idct/ieee_1180_1990.c:326: starting to merge loop iterations [eva] tests/idct/ieee_1180_1990.c:325: starting to merge loop iterations [eva] tests/idct/ieee_1180_1990.c:328: @@ -898,7 +904,7 @@ [eva:final-states] Values at end of function IEEE_1180_1990_mkbk: i ∈ {8} j ∈ {8} or UNINITIALIZED - M1[0..7][0..7] ∈ [-2147483647..2147483647] + M1[0..7][0..7] ∈ [--..--] IEEE_1180_1990_rand_randx ∈ [--..--] [eva:final-states] Values at end of function IEEE_1180_1990_dctf: i ∈ {8} @@ -951,7 +957,7 @@ omse ∈ [--..--] or UNINITIALIZED ome ∈ [--..--] or UNINITIALIZED err ∈ [--..--] or UNINITIALIZED - M1[0..7][0..7] ∈ [-2147483647..2147483647] + M1[0..7][0..7] ∈ [--..--] IEEE_1180_1990_rand_randx ∈ [--..--] IEEE_1180_1990_dctf_mcos[0..7][0..7] ∈ [-1.0000000000000000*2^-1 .. 1.0000000000000000*2^-1] diff --git a/tests/value/inversion2.i b/tests/value/inversion2.i index d1f31a4f0e4cbf1d819eecfe4e5ed048bac130fe..e9a935555be48a67a2c5722bd65e1bda1bfb50fd 100644 --- a/tests/value/inversion2.i +++ b/tests/value/inversion2.i @@ -1,5 +1,5 @@ /* run.config* - STDOPT: +"-then -wlevel 4" + STDOPT: +"-then -eva-widening-delay 4 -eva-widening-period 3" */ int T[3] = {3,1,2}; diff --git a/tests/value/oracle/inversion2.res.oracle b/tests/value/oracle/inversion2.res.oracle index 60312c7f1728df66638131403a085b9f6e987df8..1c380b36ac4a4bbe4dd58f99f4b37a66e0a01831 100644 --- a/tests/value/oracle/inversion2.res.oracle +++ b/tests/value/oracle/inversion2.res.oracle @@ -21,7 +21,7 @@ [eva] done for function main [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function main: - G ∈ {5; 7; 15; 99} + G ∈ [5..99],1%2 i ∈ {3} j ∈ {1; 2; 3; 4; 77} [from] Computing for function main diff --git a/tests/value/precise_locations.i b/tests/value/precise_locations.i index 3f3051f0dc6324e869083ba75cd0e769a668e19d..06340dba48ae65c8c9ed814351463b7a34cc27ab 100644 --- a/tests/value/precise_locations.i +++ b/tests/value/precise_locations.i @@ -1,5 +1,5 @@ /* run.config* - STDOPT: +"-then -inout -load-module report -report -then -plevel 250" + STDOPT: +"-eva-widening-period 3 -then -inout -load-module report -report -then -plevel 250" */ struct s {