From aefb889a9611e8dfe114da5cdab7344e83a545d9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 18 Apr 2019 10:45:23 +0200
Subject: [PATCH] [Eva] Updates alternative test oracles.
---
tests/builtins/diff_equalities | 59 ++++++++++---------
tests/builtins/diff_gauges | 4 +-
tests/builtins/diff_symblocs | 2 +-
tests/value/diff_apron | 47 ++++++++-------
tests/value/diff_equalities | 80 ++++++++++++-------------
tests/value/diff_gauges | 104 ++++++++++++++++-----------------
tests/value/diff_symblocs | 80 -------------------------
7 files changed, 153 insertions(+), 223 deletions(-)
diff --git a/tests/builtins/diff_equalities b/tests/builtins/diff_equalities
index bb058d3aba7..653e7459b35 100644
--- a/tests/builtins/diff_equalities
+++ b/tests/builtins/diff_equalities
@@ -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];
---
diff --git a/tests/builtins/diff_gauges b/tests/builtins/diff_gauges
index 5a276d3cf19..41ef15b15d1 100644
--- a/tests/builtins/diff_gauges
+++ b/tests/builtins/diff_gauges
@@ -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
diff --git a/tests/builtins/diff_symblocs b/tests/builtins/diff_symblocs
index f82ea2c45a6..9989eea8b41 100644
--- a/tests/builtins/diff_symblocs
+++ b/tests/builtins/diff_symblocs
@@ -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}
diff --git a/tests/value/diff_apron b/tests/value/diff_apron
index 7b830e4e3d3..2ead3a445bb 100644
--- a/tests/value/diff_apron
+++ b/tests/value/diff_apron
@@ -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:
diff --git a/tests/value/diff_equalities b/tests/value/diff_equalities
index dff0951199d..821b7e3c2fc 100644
--- a/tests/value/diff_equalities
+++ b/tests/value/diff_equalities
@@ -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]
diff --git a/tests/value/diff_gauges b/tests/value/diff_gauges
index 26c5b6d4c45..e0312fea2b9 100644
--- a/tests/value/diff_gauges
+++ b/tests/value/diff_gauges
@@ -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:
> 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},
@@ -634,23 +628,24 @@ 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: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}
@@ -658,31 +653,36 @@ diff tests/value/oracle/modulo.res.oracle tests/value/oracle_gauges/modulo.res.o
> 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}, {1}, {0}
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {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: {-2; -1}, {1}, {0}
> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {-2; -1}, {-1}, {0}
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2}, {1}, {0}
+> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2}, {-1}, {0}
60a227,240
> [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]
diff --git a/tests/value/diff_symblocs b/tests/value/diff_symblocs
index 66cf8a0b6bf..fdad91d414b 100644
--- a/tests/value/diff_symblocs
+++ b/tests/value/diff_symblocs
@@ -50,86 +50,6 @@ diff tests/value/oracle/bitwise_reduction.res.oracle tests/value/oracle_symblocs
< {0; 1}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
---
> {0; 1}, {0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
-diff tests/value/oracle/builtins_split.res.oracle tests/value/oracle_symblocs/builtins_split.res.oracle
-68a69,70
-> [eva] tests/value/builtins_split.c:96: Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:96: Call to builtin Frama_C_builtin_split_all
-98a101,144
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-133a180,209
-> [eva] tests/value/builtins_split.c:112:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:112:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:112:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:112:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:112:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:112:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:112:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:112:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:114:
-> Frama_C_show_each_s_5:
-> {{ &s6 + {4} }}, {{ &s4 + {4} }}, {{ &s2 }}, [-2147483648..2147483647]
-> [eva] tests/value/builtins_split.c:114:
-> Frama_C_show_each_s_5: {{ &s6 + {4} }}, {{ &s4 + {4} }}, {{ &s0 }}, {0}
-> [eva] tests/value/builtins_split.c:114:
-> Frama_C_show_each_s_5: {{ &s5 + {4} }}, {{ &s3 + {4} }}, {{ &s1 }}, {-1}
-> [eva] tests/value/builtins_split.c:114:
-> Frama_C_show_each_s_5: {{ &s5 + {4} }}, {{ &s3 + {4} }}, {{ &s0 }}, {0}
-> [eva] tests/value/builtins_split.c:114:
-> Frama_C_show_each_s_5:
-> {{ &s5 + {4} }}, {{ &s4 + {4} }}, {{ &s2 }}, [-2147483648..2147483647]
-> [eva] tests/value/builtins_split.c:114:
-> Frama_C_show_each_s_5: {{ &s5 + {4} }}, {{ &s4 + {4} }}, {{ &s0 }}, {0}
diff tests/value/oracle/incompatible_states.res.oracle tests/value/oracle_symblocs/incompatible_states.res.oracle
39,40d38
< [eva:alarm] tests/value/incompatible_states.c:53: Warning:
--
GitLab