Commit aefb889a authored by David Bühler's avatar David Bühler
Browse files

[Eva] Updates alternative test oracles.

parent eef7ed47
......@@ -11,34 +11,35 @@ diff tests/builtins/oracle/alloc_weak.res.oracle tests/builtins/oracle_equalitie
36,37d35
< [eva:alarm] tests/builtins/alloc_weak.c:30: Warning:
< accessing uninitialized left-value. assert \initialized(p);
900c898
908c906
< r ∈ [--..--]
---
> r ∈ {42}
diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equalities/allocated.1.res.oracle
191a192,197
191a192,194
> [eva] tests/builtins/allocated.c:82:
> Call to builtin Frama_C_malloc_fresh for function malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_7
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_7}
208a215,217
208a212,214
> strong free on bases: {__malloc_main_l82_7}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
223a233,235
223a230,232
> strong free on bases: {__malloc_main_l82_7}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
238a251,253
238a248,250
> strong free on bases: {__malloc_main_l82_7}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
254,256d268
< [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_7
252,254c264,266
< [eva] tests/builtins/allocated.c:82:
< Call to builtin Frama_C_malloc_fresh for function malloc
< [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_7
---
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_7}
323a336,356
> [eva] tests/builtins/allocated.c:82:
> Call to builtin Frama_C_malloc_fresh for function malloc
......@@ -61,9 +62,10 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:82:
> Call to builtin Frama_C_malloc_fresh for function malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_37
326d358
< [eva] Semantic level unrolling superposing up to 300 states
329a362,382
329,330d361
< Trace partitioning superposing up to 300 states
< [eva] tests/builtins/allocated.c:84:
333a365,385
> strong free on bases: {__malloc_main_l82_37}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
......@@ -85,7 +87,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> strong free on bases: {__malloc_main_l82_31}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
399c452,470
403c455,473
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
......@@ -107,7 +109,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
471c542,560
475c545,563
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
......@@ -129,7 +131,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
543c632,650
547c635,653
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
......@@ -151,7 +153,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
615c722,740
619c725,743
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
......@@ -173,7 +175,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
687c812,830
691c815,833
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
......@@ -195,7 +197,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
759c902,920
763c905,923
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
......@@ -217,7 +219,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
831c992,1010
835c995,1013
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
......@@ -239,20 +241,21 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
901,903c1080
905,907c1083,1084
< [eva] tests/builtins/allocated.c:87: Call to builtin free
< [eva:malloc] tests/builtins/allocated.c:87:
< strong free on bases: {__malloc_main_l82_7}
---
> [eva] Semantic level unrolling superposing up to 500 states
1065,1067c1242,1243
> [eva] tests/builtins/allocated.c:81:
> Trace partitioning superposing up to 500 states
1069,1071c1246,1247
< __malloc_main_l82_7[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
---
> __malloc_main_l82_7[0] ∈ {14} or UNINITIALIZED
> [1] ∈ {17} or UNINITIALIZED
1136a1313,1333
1140a1317,1337
> __malloc_main_l82_31[0] ∈ {21} or UNINITIALIZED
> [1] ∈ {24} or UNINITIALIZED
> [2] ∈ {27} or UNINITIALIZED
......@@ -274,11 +277,11 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> __malloc_main_l82_37[0] ∈ {21} or UNINITIALIZED
> [1] ∈ {24} or UNINITIALIZED
> [2] ∈ {27} or UNINITIALIZED
1180c1377
1184c1381
< __malloc_main_l82_7[0..2] FROM __fc_heap_status; nondet (and SELF)
---
> __malloc_main_l82_7[0..1] FROM __fc_heap_status; nondet (and SELF)
1203a1401,1407
1207a1405,1411
> __malloc_main_l82_31[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_32[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_33[0..2] FROM __fc_heap_status; nondet (and SELF)
......@@ -286,11 +289,11 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> __malloc_main_l82_35[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_36[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_37[0..2] FROM __fc_heap_status; nondet (and SELF)
1227c1431
1231c1435
< __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..2];
---
> __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..1];
1239,1240c1443,1448
1243,1244c1447,1452
< __malloc_main_l82_30[0..2]; __malloc_main_l97[0]; __malloc_main_l114[0..3];
< __malloc_main_l127; __malloc_main_l127_0[0..1]; __malloc_main_l127_1[0..2];
---
......
......@@ -36,10 +36,10 @@ diff tests/builtins/oracle/malloc-size-zero.1.res.oracle tests/builtins/oracle_g
> [eva] Recording results for my_calloc
> [eva] Done for function my_calloc
diff tests/builtins/oracle/memcpy.res.oracle tests/builtins/oracle_gauges/memcpy.res.oracle
167a168,169
168a169,170
> [eva] tests/builtins/memcpy.c:96: Call to builtin memcpy
> [eva] tests/builtins/memcpy.c:96: Call to builtin memcpy
448a451
449a452
> [eva] tests/builtins/memcpy.c:230: starting to merge loop iterations
diff tests/builtins/oracle/realloc.res.oracle tests/builtins/oracle_gauges/realloc.res.oracle
689a690,1038
......
......@@ -11,7 +11,7 @@ diff tests/builtins/oracle/alloc_weak.res.oracle tests/builtins/oracle_symblocs/
36,37d35
< [eva:alarm] tests/builtins/alloc_weak.c:30: Warning:
< accessing uninitialized left-value. assert \initialized(p);
900c898
908c906
< r ∈ [--..--]
---
> r ∈ {42}
......
......@@ -415,11 +415,11 @@ diff tests/value/oracle/local_slevel.res.oracle tests/value/oracle_apron/local_s
< Frama_C_show_each: {-1}, [0..78],0%2, [0..4294967295]
---
> Frama_C_show_each: {-1}, [0..78],0%2, [0..78]
150c142
152c144
< r ∈ [--..--]
---
> r ∈ [0..2147483647]
391,393c383,385
393,395c385,387
< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {0; 1}
< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {-1}, {0}, {0; 1}
< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {0; 1; 2}
......@@ -427,15 +427,15 @@ diff tests/value/oracle/local_slevel.res.oracle tests/value/oracle_apron/local_s
> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {1}
> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {-1}, {0}, {0}
> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {1}
396c388
398c390
< Frama_C_show_each: {1}, [1..79],1%2, {0; 1; 2; 3}
---
> Frama_C_show_each: {1}, [1..79],1%2, {1; 2; 3}
400c392
402c394
< Frama_C_show_each: {1}, [1..79],1%2, {0; 1; 2; 3; 4}
---
> Frama_C_show_each: {1}, [1..79],1%2, {1; 2; 3; 4}
404,412c396
406,414c398
< Frama_C_show_each: {1}, [1..79],1%2, [0..2147483647]
< [eva] tests/value/local_slevel.i:18:
< Frama_C_show_each: {-1}, [0..78],0%2, [0..2147483647]
......@@ -447,11 +447,11 @@ diff tests/value/oracle/local_slevel.res.oracle tests/value/oracle_apron/local_s
< Frama_C_show_each: {1}, [1..79],1%2, [0..4294967295]
---
> Frama_C_show_each: {1}, [1..79],1%2, [1..79]
414c398
416c400
< Frama_C_show_each: {-1}, [0..78],0%2, [0..4294967295]
---
> Frama_C_show_each: {-1}, [0..78],0%2, [0..78]
528c512
532c516
< r ∈ [--..--]
---
> r ∈ [0..2147483647]
......@@ -618,10 +618,10 @@ diff tests/value/oracle/memexec.res.oracle tests/value/oracle_apron/memexec.res.
> g_f5_1 ∈ [-2147483648..6]
diff tests/value/oracle/modulo.res.oracle tests/value/oracle_apron/modulo.res.oracle
40a41,64
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [1..9], [0..8]
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [-9..-1], [0..8]
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [1..9], [-8..0]
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [-9..-1], [-8..0]
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [1..9], [-8..0]
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [-9..-1], [0..8]
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [1..9], [0..8]
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
......@@ -636,37 +636,37 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_apron/modulo.res.or
> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {-8; -7; -6; -5; -4; -3; -2; -1},
> {1; 2; 3; 4; 5; 6; 7},
> {-6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
50a75,98
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [1..9], [0..8]
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [-9..-1], [0..8]
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [1..9], [-8..0]
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [-9..-1], [-8..0]
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [1..9], [0..8]
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [-9..-1], [0..8]
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> [-9..-1], {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {-8; -7; -6; -5; -4; -3; -2; -1},
> {1; 2; 3; 4; 5; 6; 7},
> {-6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
60a109,110
> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-10..10], [-9..9], [-8..8]
> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-9..9], [-8..8], [-7..7]
......@@ -714,6 +714,10 @@ diff tests/value/oracle/offsetmap.1.res.oracle tests/value/oracle_apron/offsetma
> a ∈ {1; 6}
> b ∈ {0; 1}
> a7 ∈ {1}
diff tests/value/oracle/partitioning-annots.4.res.oracle tests/value/oracle_apron/partitioning-annots.4.res.oracle
14,15d13
< [eva:alarm] tests/value/partitioning-annots.c:134: Warning:
< division by zero. assert j ≢ 0;
diff tests/value/oracle/precise_locations.res.oracle tests/value/oracle_apron/precise_locations.res.oracle
32,35c32,47
< [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
......@@ -972,6 +976,9 @@ diff tests/value/oracle/unroll_simple.res.oracle tests/value/oracle_apron/unroll
< j ∈ [-2147483648..-126]
---
> j ∈ {-250}
diff tests/value/oracle/widen_on_non_monotonic.res.oracle tests/value/oracle_apron/widen_on_non_monotonic.res.oracle
25a26
> [eva] tests/value/widen_on_non_monotonic.i:21: starting to merge loop iterations
diff tests/value/oracle/with_comment.res.oracle tests/value/oracle_apron/with_comment.res.oracle
9,10d8
< [eva:alarm] tests/value/with_comment.i:21: Warning:
......
......@@ -379,10 +379,10 @@ diff tests/value/oracle/long_const.1.res.oracle tests/value/oracle_equalities/lo
> [eva] Done for function LL_ABS
diff tests/value/oracle/modulo.res.oracle tests/value/oracle_equalities/modulo.res.oracle
40a41,119
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [1..9], [0..8]
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [-9..-1], [0..8]
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [1..9], [-8..0]
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [-9..-1], [-8..0]
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [1..9], [-8..0]
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [-9..-1], [0..8]
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [1..9], [0..8]
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
......@@ -397,10 +397,9 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_equalities/modulo.r
> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {1; 2; 3; 4; 5; 6; 7; 8}, {1; 2; 3; 4; 5; 6; 7}, {0; 1; 2; 3; 4; 5; 6}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
> {-8; -7; -6; -5; -4; -3; -2; -1},
> {-7; -6; -5; -4; -3; -2; -1},
> {-6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {-8; -7; -6; -5; -4; -3; -2; -1},
......@@ -408,9 +407,10 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_equalities/modulo.r
> {-6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {-8; -7; -6; -5; -4; -3; -2; -1},
> {-7; -6; -5; -4; -3; -2; -1},
> {-6; -5; -4; -3; -2; -1; 0}
> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {1; 2; 3; 4; 5; 6; 7; 8}, {1; 2; 3; 4; 5; 6; 7}, {0; 1; 2; 3; 4; 5; 6}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {1; 2; 3; 4; 5; 6; 7}, {1; 2; 3; 4; 5; 6}, {0; 1; 2; 3; 4; 5}
......@@ -426,16 +426,16 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_equalities/modulo.r
> {-6; -5; -4; -3; -2; -1},
> {-5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {1; 2; 3; 4; 5; 6}, {1; 2; 3; 4; 5}, {0; 1; 2; 3; 4}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1}, {0; 1; 2; 3; 4}
> {-6; -5; -4; -3; -2; -1}, {-5; -4; -3; -2; -1}, {-4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {-6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5}, {-4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {-6; -5; -4; -3; -2; -1}, {-5; -4; -3; -2; -1}, {-4; -3; -2; -1; 0}
> {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1}, {0; 1; 2; 3; 4}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {1; 2; 3; 4; 5; 6}, {1; 2; 3; 4; 5}, {0; 1; 2; 3; 4}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {1; 2; 3; 4; 5}, {1; 2; 3; 4}, {0; 1; 2; 3}
> [eva] tests/value/modulo.i:41:
......@@ -445,13 +445,13 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_equalities/modulo.r
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {-5; -4; -3; -2; -1}, {-4; -3; -2; -1}, {-3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {1; 2; 3; 4}, {1; 2; 3}, {0; 1; 2}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {1; 2; 3; 4}, {-3; -2; -1}, {0; 1; 2}
> Frama_C_show_each_1: {-4; -3; -2; -1}, {-3; -2; -1}, {-2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {-4; -3; -2; -1}, {1; 2; 3}, {-2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {-4; -3; -2; -1}, {-3; -2; -1}, {-2; -1; 0}
> Frama_C_show_each_1: {1; 2; 3; 4}, {-3; -2; -1}, {0; 1; 2}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {1; 2; 3; 4}, {1; 2; 3}, {0; 1; 2}
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2; 3}, {1; 2}, {0; 1}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {-3; -2; -1}, {1; 2}, {-1; 0}
......@@ -459,28 +459,22 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_equalities/modulo.r
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {-3; -2; -1}, {-2; -1}, {-1; 0}
50a130,208
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [1..9], [0..8]
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [-9..-1], [0..8]
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [1..9], [-8..0]
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [-9..-1], [-8..0]
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [1..9], [0..8]
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [-9..-1], [0..8]
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> [-9..-1], {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {1; 2; 3; 4; 5; 6; 7; 8}, {1; 2; 3; 4; 5; 6; 7}, {0; 1; 2; 3; 4; 5; 6}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {-8; -7; -6; -5; -4; -3; -2; -1},
......@@ -493,23 +487,24 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_equalities/modulo.r
> {-6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {1; 2; 3; 4; 5; 6; 7}, {1; 2; 3; 4; 5; 6}, {0; 1; 2; 3; 4; 5}
> {1; 2; 3; 4; 5; 6; 7; 8}, {1; 2; 3; 4; 5; 6; 7}, {0; 1; 2; 3; 4; 5; 6}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {-7; -6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {1; 2; 3; 4; 5; 6; 7}, {-6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5}
> {1; 2; 3; 4; 5; 6; 7}, {1; 2; 3; 4; 5; 6}, {0; 1; 2; 3; 4; 5}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {-7; -6; -5; -4; -3; -2; -1},
> {-6; -5; -4; -3; -2; -1},
> {-5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {1; 2; 3; 4; 5; 6}, {1; 2; 3; 4; 5}, {0; 1; 2; 3; 4}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1}, {0; 1; 2; 3; 4}
> {1; 2; 3; 4; 5; 6; 7}, {-6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {-6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5}, {-4; -3; -2; -1; 0}
......@@ -517,27 +512,32 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_equalities/modulo.r
> Frama_C_show_each_2:
> {-6; -5; -4; -3; -2; -1}, {-5; -4; -3; -2; -1}, {-4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {1; 2; 3; 4; 5}, {1; 2; 3; 4}, {0; 1; 2; 3}
> Frama_C_show_each_2: {1; 2; 3; 4; 5; 6}, {1; 2; 3; 4; 5}, {0; 1; 2; 3; 4}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1}, {0; 1; 2; 3; 4}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {-5; -4; -3; -2; -1}, {1; 2; 3; 4}, {-3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {1; 2; 3; 4; 5}, {-4; -3; -2; -1}, {0; 1; 2; 3}
> Frama_C_show_each_2: {1; 2; 3; 4; 5}, {1; 2; 3; 4}, {0; 1; 2; 3}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {-5; -4; -3; -2; -1}, {-4; -3; -2; -1}, {-3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {1; 2; 3; 4}, {1; 2; 3}, {0; 1; 2}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {1; 2; 3; 4}, {-3; -2; -1}, {0; 1; 2}
> Frama_C_show_each_2: {1; 2; 3; 4; 5}, {-4; -3; -2; -1}, {0; 1; 2; 3}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {-4; -3; -2; -1}, {1; 2; 3}, {-2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {-4; -3; -2; -1}, {-3; -2; -1}, {-2; -1; 0}
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2; 3}, {1; 2}, {0; 1}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {1; 2; 3; 4}, {1; 2; 3}, {0; 1; 2}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {1; 2; 3; 4}, {-3; -2; -1}, {0; 1; 2}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {-3; -2; -1}, {1; 2}, {-1; 0}
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2; 3}, {-2; -1}, {0; 1}
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2; 3}, {1; 2}, {0; 1}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2: {-3; -2; -1}, {-2; -1}, {-1; 0}
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2; 3}, {-2; -1}, {0; 1}
60a219,231
> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-10..10], [-9..9], [-8..8]
> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-9..9], [-8..8], [-7..7]
......
......@@ -447,11 +447,11 @@ diff tests/value/oracle/local_slevel.res.oracle tests/value/oracle_gauges/local_
< Frama_C_show_each: {-1}, [0..78],0%2, [0..4294967295]
---
> Frama_C_show_each: {-1}, [0..78],0%2, [0..78]
150c142
152c144
< r ∈ [--..--]
---
> r ∈ [0..2147483647]
391,393c383,385
393,395c385,387
< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {0; 1}
< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {-1}, {0}, {0; 1}
< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {0; 1; 2}
......@@ -459,15 +459,15 @@ diff tests/value/oracle/local_slevel.res.oracle tests/value/oracle_gauges/local_
> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {1}
> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {-1}, {0}, {0}
> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {1}
396c388
398c390
< Frama_C_show_each: {1}, [1..79],1%2, {0; 1; 2; 3}
---
> Frama_C_show_each: {1}, [1..79],1%2, {1; 2; 3}
400c392
402c394
< Frama_C_show_each: {1}, [1..79],1%2, {0; 1; 2; 3; 4}
---
> Frama_C_show_each: {1}, [1..79],1%2, {1; 2; 3; 4}
404,412c396
406,414c398
< Frama_C_show_each: {1}, [1..79],1%2, [0..2147483647]
< [eva] tests/value/local_slevel.i:18:
< Frama_C_show_each: {-1}, [0..78],0%2, [0..2147483647]
......@@ -479,11 +479,11 @@ diff tests/value/oracle/local_slevel.res.oracle tests/value/oracle_gauges/local_
< Frama_C_show_each: {1}, [1..79],1%2, [0..4294967295]
---
> Frama_C_show_each: {1}, [1..79],1%2, [1..79]
414c398
416c400
< Frama_C_show_each: {-1}, [0..78],0%2, [0..4294967295]
---
> Frama_C_show_each: {-1}, [0..78],0%2, [0..78]
528c512
532c516
< r ∈ [--..--]
---
> r ∈ [0..2147483647]
......@@ -516,10 +516,10 @@ diff tests/value/oracle/memexec.res.oracle tests/value/oracle_gauges/memexec.res
> [eva] tests/value/memexec.c:98: starting to merge loop iterations
diff tests/value/oracle/modulo.res.oracle tests/value/oracle_gauges/modulo.res.oracle
40a41,123
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [1..9], [0..8]
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [-9..-1], [0..8]
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [1..9], [-8..0]
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [-9..-1], [-8..0]
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [1..9], [-8..0]
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [-9..-1], [0..8]
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [1..9], [0..8]
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
......@@ -534,10 +534,9 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_gauges/modulo.res.o
> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {1; 2; 3; 4; 5; 6; 7; 8}, {1; 2; 3; 4; 5; 6; 7}, {0; 1; 2; 3; 4; 5; 6}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
> {-8; -7; -6; -5; -4; -3; -2; -1},
> {-7; -6; -5; -4; -3; -2; -1},
> {-6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {-8; -7; -6; -5; -4; -3; -2; -1},
......@@ -545,9 +544,10 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_gauges/modulo.res.o
> {-6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {-8; -7; -6; -5; -4; -3; -2; -1},
> {-7; -6; -5; -4; -3; -2; -1},
> {-6; -5; -4; -3; -2; -1; 0}
> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {1; 2; 3; 4; 5; 6; 7; 8}, {1; 2; 3; 4; 5; 6; 7}, {0; 1; 2; 3; 4; 5; 6}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {1; 2; 3; 4; 5; 6; 7}, {1; 2; 3; 4; 5; 6}, {0; 1; 2; 3; 4; 5}
......@@ -563,16 +563,16 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_gauges/modulo.res.o
> {-6; -5; -4; -3; -2; -1},
> {-5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {1; 2; 3; 4; 5; 6}, {1; 2; 3; 4; 5}, {0; 1; 2; 3; 4}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1}, {0; 1; 2; 3; 4}
> {-6; -5; -4; -3; -2; -1}, {-5; -4; -3; -2; -1}, {-4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {-6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5}, {-4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1:
> {-6; -5; -4; -3; -2; -1}, {-5; -4; -3; -2; -1}, {-4; -3; -2; -1; 0}
> {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1}, {0; 1; 2; 3; 4}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {1; 2; 3; 4; 5; 6}, {1; 2; 3; 4; 5}, {0; 1; 2; 3; 4}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {1; 2; 3; 4; 5}, {1; 2; 3; 4}, {0; 1; 2; 3}
> [eva] tests/value/modulo.i:41:
......@@ -582,46 +582,40 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_gauges/modulo.res.o
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {-5; -4; -3; -2; -1}, {-4; -3; -2; -1}, {-3; -2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {1; 2; 3; 4}, {1; 2; 3}, {0; 1; 2}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {1; 2; 3; 4}, {-3; -2; -1}, {0; 1; 2}
> Frama_C_show_each_1: {-4; -3; -2; -1}, {-3; -2; -1}, {-2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {-4; -3; -2; -1}, {1; 2; 3}, {-2; -1; 0}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {-4; -3; -2; -1}, {-3; -2; -1}, {-2; -1; 0}
> Frama_C_show_each_1: {1; 2; 3; 4}, {-3; -2; -1}, {0; 1; 2}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {1; 2; 3; 4}, {1; 2; 3}, {0; 1; 2}
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2; 3}, {1; 2}, {0; 1}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {-3; -2; -1}, {1; 2}, {-1; 0}
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2; 3}, {-2; -1}, {0; 1}
> [eva] tests/value/modulo.i:41:
> Frama_C_show_each_1: {-3; -2; -1}, {-2; -1}, {-1; 0}
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2}, {1}, {0}
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2}, {-1}, {0}
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {-2; -1}, {1}, {0}
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {-2; -1}, {-1}, {0}
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {-2; -1}, {1}, {0}
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2}, {-1}, {0}
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2}, {1}, {0}
50a134,216
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [1..9], [0..8]
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [-9..-1], [0..8]
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [1..9], [-8..0]
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [-9..-1], [-8..0]
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [1..9], [0..8]
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [-9..-1], [0..8]
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> [-9..-1], {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1; 0}
> [eva] tests/value/modulo.i:53:
> Frama_C_show_each_2:
> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
> [eva] tests/value/modulo.i:53: