diff --git a/tests/test_config_gauges b/tests/test_config_gauges
index ee46c34eb9c1a5f4dfb63334ee41a14f19fcfb40..2c04eba2c74acdaa705e8dc6437b577266183d32 100644
--- a/tests/test_config_gauges
+++ b/tests/test_config_gauges
@@ -1,3 +1,7 @@
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains gauges
MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic -machdep x86_32
+
+# Compare the result with the oracle of the default config.
+FILTER: diff --new-file @PTEST_DIR@/oracle/@PTEST_ORACLE@ -
+
OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/value/oracle_gauges/CruiseControl.res.oracle b/tests/value/oracle_gauges/CruiseControl.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/FP5.res.oracle b/tests/value/oracle_gauges/FP5.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/abs.res.oracle b/tests/value/oracle_gauges/abs.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/abs_addr.res.oracle b/tests/value/oracle_gauges/abs_addr.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/absolute_pointer.res.oracle b/tests/value/oracle_gauges/absolute_pointer.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/abstract_struct_1.res.oracle b/tests/value/oracle_gauges/abstract_struct_1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/access_path.res.oracle b/tests/value/oracle_gauges/access_path.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/add_approx.res.oracle b/tests/value/oracle_gauges/add_approx.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/addition.res.oracle b/tests/value/oracle_gauges/addition.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/addr.0.res.oracle b/tests/value/oracle_gauges/addr.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/addr.1.res.oracle b/tests/value/oracle_gauges/addr.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/addr2.res.oracle b/tests/value/oracle_gauges/addr2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/addrofstring.res.oracle b/tests/value/oracle_gauges/addrofstring.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/affect_corrupt.0.res.oracle b/tests/value/oracle_gauges/affect_corrupt.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/affect_corrupt.1.res.oracle b/tests/value/oracle_gauges/affect_corrupt.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/ai_annot.res.oracle b/tests/value/oracle_gauges/ai_annot.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/alias.0.res.oracle b/tests/value/oracle_gauges/alias.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/alias.1.res.oracle b/tests/value/oracle_gauges/alias.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/alias.2.res.oracle b/tests/value/oracle_gauges/alias.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/alias.3.res.oracle b/tests/value/oracle_gauges/alias.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/alias.4.res.oracle b/tests/value/oracle_gauges/alias.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/alias.5.res.oracle b/tests/value/oracle_gauges/alias.5.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3136d5f1ef82f0f21af779e1e32866f2f1cfd502
--- /dev/null
+++ b/tests/value/oracle_gauges/alias.5.res.oracle
@@ -0,0 +1,2 @@
+59a60
+> [eva] tests/value/alias.i:260: starting to merge loop iterations
diff --git a/tests/value/oracle_gauges/alias.6.res.oracle b/tests/value/oracle_gauges/alias.6.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/align.res.oracle b/tests/value/oracle_gauges/align.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/align_char_array.res.oracle b/tests/value/oracle_gauges/align_char_array.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/annot.res.oracle b/tests/value/oracle_gauges/annot.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/annot_valid.res.oracle b/tests/value/oracle_gauges/annot_valid.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/anonymous_field.res.oracle b/tests/value/oracle_gauges/anonymous_field.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/any_int.res.oracle b/tests/value/oracle_gauges/any_int.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/arch.res.oracle b/tests/value/oracle_gauges/arch.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/arg_array.res.oracle b/tests/value/oracle_gauges/arg_array.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/arith_pointer.res.oracle b/tests/value/oracle_gauges/arith_pointer.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/array_access.res.oracle b/tests/value/oracle_gauges/array_access.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/array_array.0.res.oracle b/tests/value/oracle_gauges/array_array.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/array_array.1.res.oracle b/tests/value/oracle_gauges/array_array.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/array_array.2.res.oracle b/tests/value/oracle_gauges/array_array.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/array_bounds.0.res.oracle b/tests/value/oracle_gauges/array_bounds.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/array_bounds.1.res.oracle b/tests/value/oracle_gauges/array_bounds.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/array_degenerating_loop.res.oracle b/tests/value/oracle_gauges/array_degenerating_loop.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/array_initializer.res.oracle b/tests/value/oracle_gauges/array_initializer.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/array_loop.res.oracle b/tests/value/oracle_gauges/array_loop.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/array_overlap.res.oracle b/tests/value/oracle_gauges/array_overlap.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/array_ptr.res.oracle b/tests/value/oracle_gauges/array_ptr.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/array_zero_length.0.res.oracle b/tests/value/oracle_gauges/array_zero_length.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/array_zero_length.1.res.oracle b/tests/value/oracle_gauges/array_zero_length.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/array_zero_length.2.res.oracle b/tests/value/oracle_gauges/array_zero_length.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/asm_contracts.res.oracle b/tests/value/oracle_gauges/asm_contracts.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/assert_ptr.res.oracle b/tests/value/oracle_gauges/assert_ptr.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/assign-leaf-indirect.res.oracle b/tests/value/oracle_gauges/assign-leaf-indirect.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/assigns.res.oracle b/tests/value/oracle_gauges/assigns.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/assigns_from.res.oracle b/tests/value/oracle_gauges/assigns_from.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/assigns_from_direct.res.oracle b/tests/value/oracle_gauges/assigns_from_direct.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/attribute-aligned.res.oracle b/tests/value/oracle_gauges/attribute-aligned.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/audit.res.oracle b/tests/value/oracle_gauges/audit.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..9ff41db248872519df6d5b9ea95483fc420a1ff1
--- /dev/null
+++ b/tests/value/oracle_gauges/audit.res.oracle
@@ -0,0 +1,11 @@
+1,8d0
+< [kernel:audit] Warning:
+< different hashes for tests/value/audit.c: got 08f73691217888d926a0ee15cbe18159, expected 01010101010101010101010101010101
+< [kernel:audit] Warning:
+< different hashes for tests/value/audit_included_but_not_listed.h: got c2cc488143a476f69cf2ed04c3439e6e, expected <none> (not in list)
+< [kernel:audit] Warning:
+< missing files:
+< tests/value/non_existing_file.h
+< [kernel] Audit: sources list written to: tests/value/result/audit-out.json
+34d25
+< [kernel] Wrote: tests/value/result/audit-out.json
diff --git a/tests/value/oracle_gauges/auto_loop_unroll.0.res.oracle b/tests/value/oracle_gauges/auto_loop_unroll.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b53899a72738a7c9f35605d4cba511a0cb611d45
--- /dev/null
+++ b/tests/value/oracle_gauges/auto_loop_unroll.0.res.oracle
@@ -0,0 +1,195 @@
+11,13c11
+< [eva:alarm] tests/value/auto_loop_unroll.c:25: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:27: Frama_C_show_each_auto: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:27: Frama_C_show_each_auto: {100}
+15,18c13
+< [eva:alarm] tests/value/auto_loop_unroll.c:31: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:33:
+< Frama_C_show_each_imprecise: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:33: Frama_C_show_each_imprecise: {1000}
+20,23c15
+< [eva:alarm] tests/value/auto_loop_unroll.c:39: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:41:
+< Frama_C_show_each_imprecise: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:41: Frama_C_show_each_imprecise: {100}
+32,34c24
+< [eva:alarm] tests/value/auto_loop_unroll.c:58: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:59: Frama_C_show_each_64: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:59: Frama_C_show_each_64: {64}
+36,38c26
+< [eva:alarm] tests/value/auto_loop_unroll.c:63: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:64: Frama_C_show_each_40: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:64: Frama_C_show_each_40: {40}
+40,42c28
+< [eva:alarm] tests/value/auto_loop_unroll.c:69: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:72: Frama_C_show_each_80: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:72: Frama_C_show_each_80: {80}
+44,47c30
+< [eva:alarm] tests/value/auto_loop_unroll.c:76: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:82:
+< Frama_C_show_each_32_80: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:82: Frama_C_show_each_32_80: [32..83]
+55,56d37
+< [eva:alarm] tests/value/auto_loop_unroll.c:88: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+58c39
+< Frama_C_show_each_40_50: [0..2147483647]
+---
+> Frama_C_show_each_40_50: [40..1073741861]
+133,136c114
+< [eva:alarm] tests/value/auto_loop_unroll.c:120: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:122:
+< Frama_C_show_each_32_64: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:122: Frama_C_show_each_32_64: [32..65]
+194,197c172
+< [eva:alarm] tests/value/auto_loop_unroll.c:192: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:194:
+< Frama_C_show_each_imprecise: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:194: Frama_C_show_each_imprecise: [1..9]
+199,200d173
+< [eva:alarm] tests/value/auto_loop_unroll.c:200: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+204c177
+< Frama_C_show_each_imprecise: [0..2147483647]
+---
+> Frama_C_show_each_imprecise: [64..2147483647]
+210,212c183
+< [eva:alarm] tests/value/auto_loop_unroll.c:212: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:214: Frama_C_show_each_11: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:214: Frama_C_show_each_11: {11}
+214,216c185
+< [eva:alarm] tests/value/auto_loop_unroll.c:217: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:219: Frama_C_show_each_12: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:219: Frama_C_show_each_12: {12}
+218,219d186
+< [eva:alarm] tests/value/auto_loop_unroll.c:223: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+221a189,190
+> [eva:alarm] tests/value/auto_loop_unroll.c:223: Warning:
+> signed overflow. assert res + 1 ≤ 2147483647;
+225,226d193
+< [eva:alarm] tests/value/auto_loop_unroll.c:228: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+228a196,197
+> [eva:alarm] tests/value/auto_loop_unroll.c:228: Warning:
+> signed overflow. assert res + 1 ≤ 2147483647;
+232,233d200
+< [eva:alarm] tests/value/auto_loop_unroll.c:236: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+237,240c204
+< [eva:alarm] tests/value/auto_loop_unroll.c:241: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:245:
+< Frama_C_show_each_11_111: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:245: Frama_C_show_each_11_111: [11..111]
+242,244c206
+< [eva:alarm] tests/value/auto_loop_unroll.c:251: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:253: Frama_C_show_each_16: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:253: Frama_C_show_each_16: [16..2147483647]
+252,254c214
+< [eva:alarm] tests/value/auto_loop_unroll.c:263: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_20: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:265: Frama_C_show_each_20: [20..2147483646]
+256,257d215
+< [eva:alarm] tests/value/auto_loop_unroll.c:268: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+260c218,220
+< [eva] tests/value/auto_loop_unroll.c:270: Frama_C_show_each_21: [0..2147483647]
+---
+> [eva:alarm] tests/value/auto_loop_unroll.c:268: Warning:
+> signed overflow. assert res + 1 ≤ 2147483647;
+> [eva] tests/value/auto_loop_unroll.c:270: Frama_C_show_each_21: {21}
+264,265d223
+< [eva:alarm] tests/value/auto_loop_unroll.c:272: Warning:
+< signed overflow. assert i + 1 ≤ 2147483647;
+270,271d227
+< [eva:alarm] tests/value/auto_loop_unroll.c:279: Warning:
+< signed overflow. assert i + 1 ≤ 2147483647;
+276,277d231
+< [eva:alarm] tests/value/auto_loop_unroll.c:287: Warning:
+< signed overflow. assert i + 1 ≤ 2147483647;
+284,286c238,239
+< [eva:alarm] tests/value/auto_loop_unroll.c:299: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:303: Frama_C_show_each_30: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:303: Frama_C_show_each_30: {30}
+> [eva] tests/value/auto_loop_unroll.c:307: starting to merge loop iterations
+289d241
+< [eva] tests/value/auto_loop_unroll.c:307: starting to merge loop iterations
+292,294c244
+< [eva:alarm] tests/value/auto_loop_unroll.c:316: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:321: Frama_C_show_each_32: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:321: Frama_C_show_each_32: {32}
+307,310c257
+< [eva:alarm] tests/value/auto_loop_unroll.c:343: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:345:
+< Frama_C_show_each_0_35: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:345: Frama_C_show_each_0_35: [0..35]
+313,314d259
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva:alarm] tests/value/auto_loop_unroll.c:348: Warning:
+316c261,263
+< [eva] tests/value/auto_loop_unroll.c:352: Frama_C_show_each_36: [0..2147483647]
+---
+> [eva:alarm] tests/value/auto_loop_unroll.c:348: Warning:
+> signed overflow. assert res + 1 ≤ 2147483647;
+> [eva] tests/value/auto_loop_unroll.c:352: Frama_C_show_each_36: {36}
+325,327c272
+< [eva:alarm] tests/value/auto_loop_unroll.c:371: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:375: Frama_C_show_each_50: [1..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:375: Frama_C_show_each_50: {50}
+330,331d274
+< [eva:alarm] tests/value/auto_loop_unroll.c:380: Warning:
+< signed overflow. assert -2147483648 ≤ i - 1;
+339,342d281
+< [eva:alarm] tests/value/auto_loop_unroll.c:392: Warning:
+< signed overflow. assert j + 1 ≤ 2147483647;
+< [eva:alarm] tests/value/auto_loop_unroll.c:396: Warning:
+< signed overflow. assert j + 1 ≤ 2147483647;
+344c283
+< [eva] tests/value/auto_loop_unroll.c:398: Frama_C_show_each_30: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:398: Frama_C_show_each_30: {30}
+346,349d284
+< [eva:alarm] tests/value/auto_loop_unroll.c:403: Warning:
+< signed overflow. assert j + 1 ≤ 2147483647;
+< [eva:alarm] tests/value/auto_loop_unroll.c:407: Warning:
+< signed overflow. assert j + 1 ≤ 2147483647;
+351c286
+< [eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:412: Frama_C_show_each_30: [15..45]
diff --git a/tests/value/oracle_gauges/auto_loop_unroll.1.res.oracle b/tests/value/oracle_gauges/auto_loop_unroll.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..69c5d75fdc9b168fb5e84a39b225b0e6a9ac2f9f
--- /dev/null
+++ b/tests/value/oracle_gauges/auto_loop_unroll.1.res.oracle
@@ -0,0 +1,31 @@
+15,18c15
+< [eva:alarm] tests/value/auto_loop_unroll.c:31: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:33:
+< Frama_C_show_each_imprecise: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:33: Frama_C_show_each_imprecise: {1000}
+20,23c17
+< [eva:alarm] tests/value/auto_loop_unroll.c:39: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:41:
+< Frama_C_show_each_imprecise: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:41: Frama_C_show_each_imprecise: {100}
+335,338c329
+< [eva:alarm] tests/value/auto_loop_unroll.c:192: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:194:
+< Frama_C_show_each_imprecise: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:194: Frama_C_show_each_imprecise: [1..9]
+340,341d330
+< [eva:alarm] tests/value/auto_loop_unroll.c:200: Warning:
+< signed overflow. assert res + 1 ≤ 2147483647;
+345c334
+< Frama_C_show_each_imprecise: [0..2147483647]
+---
+> Frama_C_show_each_imprecise: [64..2147483647]
+381,382d369
+< [eva:alarm] tests/value/auto_loop_unroll.c:287: Warning:
+< signed overflow. assert i + 1 ≤ 2147483647;
diff --git a/tests/value/oracle_gauges/automalloc.res.oracle b/tests/value/oracle_gauges/automalloc.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/backward_add_ptr.res.oracle b/tests/value/oracle_gauges/backward_add_ptr.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/backward_arith.res.oracle b/tests/value/oracle_gauges/backward_arith.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bad_loop.res.oracle b/tests/value/oracle_gauges/bad_loop.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0801a0331945b646c64cf36e95d84db91bd5e2ce
--- /dev/null
+++ b/tests/value/oracle_gauges/bad_loop.res.oracle
@@ -0,0 +1,2 @@
+6a7
+> [eva] tests/value/bad_loop.i:12: starting to merge loop iterations
diff --git a/tests/value/oracle_gauges/base_addr_offset_block_length.res.oracle b/tests/value/oracle_gauges/base_addr_offset_block_length.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/behavior_statuses.0.res.oracle b/tests/value/oracle_gauges/behavior_statuses.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/behavior_statuses.1.res.oracle b/tests/value/oracle_gauges/behavior_statuses.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/behaviors1.res.oracle b/tests/value/oracle_gauges/behaviors1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/behaviors2.res.oracle b/tests/value/oracle_gauges/behaviors2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/big_lib_entry.res.oracle b/tests/value/oracle_gauges/big_lib_entry.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bigarray.res.oracle b/tests/value/oracle_gauges/bigarray.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bitfield.res.oracle b/tests/value/oracle_gauges/bitfield.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1ac37a479977ef3745e516936e77bfb7d93dc33c
--- /dev/null
+++ b/tests/value/oracle_gauges/bitfield.res.oracle
@@ -0,0 +1,16 @@
+138a139,153
+> [eva] tests/value/bitfield.i:71:
+> Frama_C_show_each:
+> {{ garbled mix of &{b} (origin: Misaligned {tests/value/bitfield.i:70}) }}
+> [eva] tests/value/bitfield.i:73:
+> Frama_C_show_each:
+> {{ garbled mix of &{b} (origin: Misaligned {tests/value/bitfield.i:70}) }}
+> [eva] computing for function leaf <- imprecise_bts_1671 <- main.
+> Called from tests/value/bitfield.i:70.
+> [eva] Done for function leaf
+> [eva] tests/value/bitfield.i:71:
+> Frama_C_show_each:
+> {{ garbled mix of &{b} (origin: Misaligned {tests/value/bitfield.i:70}) }}
+> [eva] tests/value/bitfield.i:73:
+> Frama_C_show_each:
+> {{ garbled mix of &{b} (origin: Misaligned {tests/value/bitfield.i:70}) }}
diff --git a/tests/value/oracle_gauges/bitfield_assign.res.oracle b/tests/value/oracle_gauges/bitfield_assign.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bitfield_longlong.res.oracle b/tests/value/oracle_gauges/bitfield_longlong.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bitfield_receives_result.res.oracle b/tests/value/oracle_gauges/bitfield_receives_result.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bitwise.res.oracle b/tests/value/oracle_gauges/bitwise.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bitwise_float.res.oracle b/tests/value/oracle_gauges/bitwise_float.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bitwise_pointer.res.oracle b/tests/value/oracle_gauges/bitwise_pointer.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bitwise_reduction.res.oracle b/tests/value/oracle_gauges/bitwise_reduction.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/biz.res.oracle b/tests/value/oracle_gauges/biz.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bool.res.oracle b/tests/value/oracle_gauges/bool.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/branch.res.oracle b/tests/value/oracle_gauges/branch.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/branch2.res.oracle b/tests/value/oracle_gauges/branch2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/broken_loop.res.oracle b/tests/value/oracle_gauges/broken_loop.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bts0506.0.res.oracle b/tests/value/oracle_gauges/bts0506.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bts0506.1.res.oracle b/tests/value/oracle_gauges/bts0506.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bts0775.res.oracle b/tests/value/oracle_gauges/bts0775.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bts0858.res.oracle b/tests/value/oracle_gauges/bts0858.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bts1306.res.oracle b/tests/value/oracle_gauges/bts1306.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/buffer_overflow.0.res.oracle b/tests/value/oracle_gauges/buffer_overflow.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/buffer_overflow.1.res.oracle b/tests/value/oracle_gauges/buffer_overflow.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bug.res.oracle b/tests/value/oracle_gauges/bug.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bug0196.res.oracle b/tests/value/oracle_gauges/bug0196.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bug0223.0.res.oracle b/tests/value/oracle_gauges/bug0223.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bug0223.1.res.oracle b/tests/value/oracle_gauges/bug0223.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bug0245.res.oracle b/tests/value/oracle_gauges/bug0245.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bug_023.res.oracle b/tests/value/oracle_gauges/bug_023.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/bug_0244.res.oracle b/tests/value/oracle_gauges/bug_0244.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/builtins_split.res.oracle b/tests/value/oracle_gauges/builtins_split.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/call.res.oracle b/tests/value/oracle_gauges/call.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/call_2.res.oracle b/tests/value/oracle_gauges/call_2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/call_3.res.oracle b/tests/value/oracle_gauges/call_3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/call_alias.0.res.oracle b/tests/value/oracle_gauges/call_alias.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/call_alias.1.res.oracle b/tests/value/oracle_gauges/call_alias.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/call_alias.2.res.oracle b/tests/value/oracle_gauges/call_alias.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/call_deep.res.oracle b/tests/value/oracle_gauges/call_deep.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/call_multi.res.oracle b/tests/value/oracle_gauges/call_multi.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/call_simple.res.oracle b/tests/value/oracle_gauges/call_simple.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/case_analysis.res.oracle b/tests/value/oracle_gauges/case_analysis.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/cast.res.oracle b/tests/value/oracle_gauges/cast.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/cast1.res.oracle b/tests/value/oracle_gauges/cast1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/cast2.res.oracle b/tests/value/oracle_gauges/cast2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ba548cab66284dc6d1633823aafdae6fae261f51
--- /dev/null
+++ b/tests/value/oracle_gauges/cast2.res.oracle
@@ -0,0 +1,2 @@
+26a27
+> [eva] tests/value/cast2.i:24: starting to merge loop iterations
diff --git a/tests/value/oracle_gauges/cast_axalto.res.oracle b/tests/value/oracle_gauges/cast_axalto.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/cast_fun.res.oracle b/tests/value/oracle_gauges/cast_fun.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/cast_hetero.res.oracle b/tests/value/oracle_gauges/cast_hetero.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/cast_return.0.res.oracle b/tests/value/oracle_gauges/cast_return.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/cast_return.1.res.oracle b/tests/value/oracle_gauges/cast_return.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/cert_exp35_c.res.oracle b/tests/value/oracle_gauges/cert_exp35_c.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/changeret.res.oracle b/tests/value/oracle_gauges/changeret.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/cmp.res.oracle b/tests/value/oracle_gauges/cmp.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/cmp_ptr.0.res.oracle b/tests/value/oracle_gauges/cmp_ptr.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/cmp_ptr.1.res.oracle b/tests/value/oracle_gauges/cmp_ptr.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/cmp_ptr_follow_all_branches.0.res.oracle b/tests/value/oracle_gauges/cmp_ptr_follow_all_branches.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/cmp_ptr_follow_all_branches.1.res.oracle b/tests/value/oracle_gauges/cmp_ptr_follow_all_branches.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/cond.res.oracle b/tests/value/oracle_gauges/cond.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/cond2.0.res.oracle b/tests/value/oracle_gauges/cond2.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/cond2.1.res.oracle b/tests/value/oracle_gauges/cond2.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/cond_integer_cast_of_float.res.oracle b/tests/value/oracle_gauges/cond_integer_cast_of_float.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/conditional_initializer.res.oracle b/tests/value/oracle_gauges/conditional_initializer.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/const.res.oracle b/tests/value/oracle_gauges/const.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/const2.res.oracle b/tests/value/oracle_gauges/const2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/const_syntax.res.oracle b/tests/value/oracle_gauges/const_syntax.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/const_typedef.res.oracle b/tests/value/oracle_gauges/const_typedef.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/constarraystructlibentry.res.oracle b/tests/value/oracle_gauges/constarraystructlibentry.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/context_free.res.oracle b/tests/value/oracle_gauges/context_free.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/context_free_simple.res.oracle b/tests/value/oracle_gauges/context_free_simple.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/context_width.res.oracle b/tests/value/oracle_gauges/context_width.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/control.res.oracle b/tests/value/oracle_gauges/control.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/conversion.res.oracle b/tests/value/oracle_gauges/conversion.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/copy_paste.res.oracle b/tests/value/oracle_gauges/copy_paste.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/copy_paste_hidden_by_dummy_cast.res.oracle b/tests/value/oracle_gauges/copy_paste_hidden_by_dummy_cast.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/copy_stdin.res.oracle b/tests/value/oracle_gauges/copy_stdin.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/dangling.res.oracle b/tests/value/oracle_gauges/dangling.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/dataflow_order.res.oracle b/tests/value/oracle_gauges/dataflow_order.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/dead_code.res.oracle b/tests/value/oracle_gauges/dead_code.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/dead_code2.res.oracle b/tests/value/oracle_gauges/dead_code2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/dead_inout.res.oracle b/tests/value/oracle_gauges/dead_inout.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/dead_statuses.res.oracle b/tests/value/oracle_gauges/dead_statuses.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/deep_conditionals.res.oracle b/tests/value/oracle_gauges/deep_conditionals.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/degeneration2.res.oracle b/tests/value/oracle_gauges/degeneration2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/deps.0.res.oracle b/tests/value/oracle_gauges/deps.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/deps.1.res.oracle b/tests/value/oracle_gauges/deps.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/deps.2.res.oracle b/tests/value/oracle_gauges/deps.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/deps_addr.res.oracle b/tests/value/oracle_gauges/deps_addr.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/deps_compose.res.oracle b/tests/value/oracle_gauges/deps_compose.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/deps_local.res.oracle b/tests/value/oracle_gauges/deps_local.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/deps_mixed.res.oracle b/tests/value/oracle_gauges/deps_mixed.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/deps_unitialized_locals.res.oracle b/tests/value/oracle_gauges/deps_unitialized_locals.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/deref.res.oracle b/tests/value/oracle_gauges/deref.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/descending.res.oracle b/tests/value/oracle_gauges/descending.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/disjoint_status.res.oracle b/tests/value/oracle_gauges/disjoint_status.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/div.0.res.oracle b/tests/value/oracle_gauges/div.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/div.1.res.oracle b/tests/value/oracle_gauges/div.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/div_strange.res.oracle b/tests/value/oracle_gauges/div_strange.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/divneg.res.oracle b/tests/value/oracle_gauges/divneg.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/domains.res.oracle b/tests/value/oracle_gauges/domains.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/domains_function.res.oracle b/tests/value/oracle_gauges/domains_function.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/downcast.0.res.oracle b/tests/value/oracle_gauges/downcast.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/downcast.1.res.oracle b/tests/value/oracle_gauges/downcast.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/downcast.2.res.oracle b/tests/value/oracle_gauges/downcast.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/downcast.3.res.oracle b/tests/value/oracle_gauges/downcast.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/downcast.4.res.oracle b/tests/value/oracle_gauges/downcast.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/dur.res.oracle b/tests/value/oracle_gauges/dur.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/empty_base.0.res.oracle b/tests/value/oracle_gauges/empty_base.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/empty_base.1.res.oracle b/tests/value/oracle_gauges/empty_base.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/empty_struct.0.res.oracle b/tests/value/oracle_gauges/empty_struct.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/empty_struct.1.res.oracle b/tests/value/oracle_gauges/empty_struct.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/empty_struct.2.res.oracle b/tests/value/oracle_gauges/empty_struct.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/empty_struct.3.res.oracle b/tests/value/oracle_gauges/empty_struct.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/empty_struct.4.res.oracle b/tests/value/oracle_gauges/empty_struct.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/empty_struct.5.res.oracle b/tests/value/oracle_gauges/empty_struct.5.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/empty_struct.6.res.oracle b/tests/value/oracle_gauges/empty_struct.6.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/empty_struct2.res.oracle b/tests/value/oracle_gauges/empty_struct2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/empty_union.res.oracle b/tests/value/oracle_gauges/empty_union.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/endian.0.res.oracle b/tests/value/oracle_gauges/endian.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/endian.1.res.oracle b/tests/value/oracle_gauges/endian.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/enum.res.oracle b/tests/value/oracle_gauges/enum.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/enum2.res.oracle b/tests/value/oracle_gauges/enum2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/equality.res.oracle b/tests/value/oracle_gauges/equality.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/eval_separated.res.oracle b/tests/value/oracle_gauges/eval_separated.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/exit_paths.res.oracle b/tests/value/oracle_gauges/exit_paths.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/extern.res.oracle b/tests/value/oracle_gauges/extern.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/f1.res.oracle b/tests/value/oracle_gauges/f1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/f2.res.oracle b/tests/value/oracle_gauges/f2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/false.res.oracle b/tests/value/oracle_gauges/false.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/fam_sizeof.res.oracle b/tests/value/oracle_gauges/fam_sizeof.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/find_ivaltop.res.oracle b/tests/value/oracle_gauges/find_ivaltop.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/folding.res.oracle b/tests/value/oracle_gauges/folding.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/for_loops.0.res.oracle b/tests/value/oracle_gauges/for_loops.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/for_loops.1.res.oracle b/tests/value/oracle_gauges/for_loops.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a688cad743d26765cdaf73e9a3eaace9e54b19d3
--- /dev/null
+++ b/tests/value/oracle_gauges/for_loops.1.res.oracle
@@ -0,0 +1,6 @@
+39,41c39
+< [eva:alarm] tests/value/for_loops.c:16: Warning:
+< signed overflow. assert w + 1 ≤ 2147483647;
+< [eva] tests/value/for_loops.c:17: Frama_C_show_each_F: [0..2147483647]
+---
+> [eva] tests/value/for_loops.c:17: Frama_C_show_each_F: [0..100]
diff --git a/tests/value/oracle_gauges/for_loops.2.res.oracle b/tests/value/oracle_gauges/for_loops.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..07bdb32470ea74358c823be33bb122db954e445b
--- /dev/null
+++ b/tests/value/oracle_gauges/for_loops.2.res.oracle
@@ -0,0 +1,6 @@
+37,39c37
+< [eva:alarm] tests/value/for_loops.c:42: Warning:
+< signed overflow. assert w + T[j] ≤ 2147483647;
+< [eva] tests/value/for_loops.c:43: Frama_C_show_each: [0..2147483647]
+---
+> [eva] tests/value/for_loops.c:43: Frama_C_show_each: [0..1000]
diff --git a/tests/value/oracle_gauges/for_loops.3.res.oracle b/tests/value/oracle_gauges/for_loops.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/forall.res.oracle b/tests/value/oracle_gauges/forall.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/fptr.0.res.oracle b/tests/value/oracle_gauges/fptr.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/fptr.1.res.oracle b/tests/value/oracle_gauges/fptr.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/from1.res.oracle b/tests/value/oracle_gauges/from1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/from_call.0.res.oracle b/tests/value/oracle_gauges/from_call.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/from_call.1.res.oracle b/tests/value/oracle_gauges/from_call.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/from_global.res.oracle b/tests/value/oracle_gauges/from_global.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/from_ind.res.oracle b/tests/value/oracle_gauges/from_ind.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/from_pb.0.res.oracle b/tests/value/oracle_gauges/from_pb.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/from_pb.1.res.oracle b/tests/value/oracle_gauges/from_pb.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/from_pb.2.res.oracle b/tests/value/oracle_gauges/from_pb.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/from_pb.3.res.oracle b/tests/value/oracle_gauges/from_pb.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/from_pb.4.res.oracle b/tests/value/oracle_gauges/from_pb.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/from_pb.5.res.oracle b/tests/value/oracle_gauges/from_pb.5.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/from_pb.6.res.oracle b/tests/value/oracle_gauges/from_pb.6.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/from_pb.7.res.oracle b/tests/value/oracle_gauges/from_pb.7.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/from_ptr.0.res.oracle b/tests/value/oracle_gauges/from_ptr.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/from_ptr.1.res.oracle b/tests/value/oracle_gauges/from_ptr.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/from_ptr2.res.oracle b/tests/value/oracle_gauges/from_ptr2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/from_res_2.res.oracle b/tests/value/oracle_gauges/from_res_2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/from_termin.res.oracle b/tests/value/oracle_gauges/from_termin.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a29f1796862a617621451045df13187bf62b6a6d
--- /dev/null
+++ b/tests/value/oracle_gauges/from_termin.res.oracle
@@ -0,0 +1,2 @@
+9a10
+> [eva] tests/value/from_termin.i:8: starting to merge loop iterations
diff --git a/tests/value/oracle_gauges/fun_ptr.0.res.oracle b/tests/value/oracle_gauges/fun_ptr.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/fun_ptr.1.res.oracle b/tests/value/oracle_gauges/fun_ptr.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/function_return_serial_casts.res.oracle b/tests/value/oracle_gauges/function_return_serial_casts.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/g1.res.oracle b/tests/value/oracle_gauges/g1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/garbled_init.res.oracle b/tests/value/oracle_gauges/garbled_init.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/gauges.res.oracle b/tests/value/oracle_gauges/gauges.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a34023e43fe99cbd16db6f50c76ba68a7996f94f
--- /dev/null
+++ b/tests/value/oracle_gauges/gauges.res.oracle
@@ -0,0 +1,348 @@
+25,26d24
+< [eva:alarm] tests/value/gauges.c:23: Warning:
+< signed overflow. assert -2147483648 ≤ j - 4;
+38,39d35
+< [eva:alarm] tests/value/gauges.c:26: Warning:
+< signed overflow. assert l + 1 ≤ 2147483647;
+57,58d52
+< [eva:alarm] tests/value/gauges.c:45: Warning:
+< signed overflow. assert -2147483648 ≤ j - 4;
+61a56,57
+> [eva:alarm] tests/value/gauges.c:45: Warning:
+> signed overflow. assert -2147483648 ≤ j - 4;
+70,71d65
+< [eva:alarm] tests/value/gauges.c:48: Warning:
+< signed overflow. assert l + 1 ≤ 2147483647;
+83,84d76
+< [eva:alarm] tests/value/gauges.c:58: Warning:
+< accessing out of bounds index. assert j < 38;
+97,101d88
+< [eva:alarm] tests/value/gauges.c:71: Warning:
+< out of bounds write. assert \valid(tmp);
+< (tmp from p++)
+< [eva] tests/value/gauges.c:72: Frama_C_show_each:
+< [eva] tests/value/gauges.c:72: Frama_C_show_each:
+113,114d99
+< [eva:alarm] tests/value/gauges.c:81: Warning:
+< signed overflow. assert k + 1 ≤ 2147483647;
+116,117d100
+< [eva:alarm] tests/value/gauges.c:84: Warning:
+< signed overflow. assert k + 1 ≤ 2147483647;
+125c108
+< [eva] tests/value/gauges.c:86: Frama_C_show_each: [0..2147483647]
+---
+> [eva] tests/value/gauges.c:86: Frama_C_show_each: {390}
+139,140d121
+< [eva:alarm] tests/value/gauges.c:99: Warning:
+< signed overflow. assert c + 1 ≤ 2147483647;
+178,181c159,162
+< [eva] tests/value/gauges.c:129: Frama_C_show_each: {{ &y + [4..36],0%4 }}
+< [eva] tests/value/gauges.c:129: Frama_C_show_each: {{ &y + [4..40],0%4 }}
+< [eva:alarm] tests/value/gauges.c:130: Warning:
+< out of bounds write. assert \valid(p);
+---
+> [eva] tests/value/gauges.c:129:
+> Frama_C_show_each: {{ &y + {4; 8; 12; 16; 20; 24} }}
+> [eva] tests/value/gauges.c:129:
+> Frama_C_show_each: {{ &y + {4; 8; 12; 16; 20; 24} }}
+187,188d167
+< [eva:alarm] tests/value/gauges.c:140: Warning:
+< signed overflow. assert j + 1 ≤ 2147483647;
+206,208d184
+< [eva:alarm] tests/value/gauges.c:158: Warning:
+< out of bounds write. assert \valid(tmp);
+< (tmp from p--)
+227,231c203,205
+< [eva] tests/value/gauges.c:172: Frama_C_show_each: [2147483646..4294967294]
+< [eva] tests/value/gauges.c:172: Frama_C_show_each: [1..4294967294]
+< [eva] tests/value/gauges.c:172: Frama_C_show_each: [1..4294967294]
+< [eva] tests/value/gauges.c:172: Frama_C_show_each: [1..4294967294]
+< [eva] tests/value/gauges.c:172: Frama_C_show_each: [1..4294967294]
+---
+> [eva] tests/value/gauges.c:172: Frama_C_show_each: [2147483647..4294967294]
+> [eva] tests/value/gauges.c:172: Frama_C_show_each: [2147483647..4294967294]
+> [eva] tests/value/gauges.c:172: Frama_C_show_each: [2147483647..4294967294]
+235c209,210
+< [eva] tests/value/gauges.c:172: Frama_C_show_each: [1..4294967294]
+---
+> [eva] tests/value/gauges.c:172: Frama_C_show_each: [2147483647..4294967294]
+> [eva] tests/value/gauges.c:172: Frama_C_show_each: [2147483647..4294967294]
+259,262d233
+< [eva:alarm] tests/value/gauges.c:192: Warning:
+< out of bounds write. assert \valid(p);
+< [eva:alarm] tests/value/gauges.c:193: Warning:
+< out of bounds write. assert \valid(q);
+270,275d240
+< [eva:alarm] tests/value/gauges.c:202: Warning:
+< out of bounds read. assert \valid_read(tmp);
+< (tmp from A++)
+< [eva:alarm] tests/value/gauges.c:202: Warning:
+< out of bounds read. assert \valid_read(tmp_0);
+< (tmp_0 from B++)
+303,304d267
+< [eva:alarm] tests/value/gauges.c:220: Warning:
+< signed overflow. assert -2147483648 ≤ n - 1;
+319,322c282
+< [eva:alarm] tests/value/gauges.c:240: Warning:
+< signed overflow. assert j + 1 ≤ 2147483647;
+< [eva] tests/value/gauges.c:242:
+< Frama_C_show_each: {45; 46; 47; 48; 49; 50; 51}, [0..2147483647]
+---
+> [eva] tests/value/gauges.c:242: Frama_C_show_each: {47; 48}, {6}
+328,329d287
+< [eva:alarm] tests/value/gauges.c:251: Warning:
+< signed overflow. assert j + 1 ≤ 2147483647;
+331c289
+< Frama_C_show_each: {48; 49; 50; 51; 52; 53; 54}, [0..2147483647]
+---
+> Frama_C_show_each: {48; 49; 50; 51; 52; 53; 54}, {6; 7}
+337,340c295
+< [eva:alarm] tests/value/gauges.c:263: Warning:
+< signed overflow. assert j + 1 ≤ 2147483647;
+< [eva] tests/value/gauges.c:265:
+< Frama_C_show_each: {-59; -58; -57; -56; -55; -54; -53}, [0..2147483647]
+---
+> [eva] tests/value/gauges.c:265: Frama_C_show_each: {-58; -57}, {9}
+346,347d300
+< [eva:alarm] tests/value/gauges.c:274: Warning:
+< signed overflow. assert j + 1 ≤ 2147483647;
+349c302
+< Frama_C_show_each: {-64; -63; -62; -61; -60; -59; -58}, [0..2147483647]
+---
+> Frama_C_show_each: {-64; -63; -62; -61; -60; -59; -58}, {9; 10}
+357,358d309
+< [eva:alarm] tests/value/gauges.c:293: Warning:
+< signed overflow. assert j + 1 ≤ 2147483647;
+360c311
+< Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..2147483647]
+---
+> Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [99..119]
+422a374,377
+> # Gauges domain:
+> V: [{[ p -> {{ &x }}
+> i -> {1} ]}]
+> s398: λ(0)
+482a438,441
+> # Gauges domain:
+> V: [{[ i -> {1} ]}]
+> s398: λ([0 .. 1])
+> {[ i -> {1} ]}
+541a501,504
+> # Gauges domain:
+> V: [{[ i -> {1} ]}]
+> s398: λ([0 .. 2])
+> {[ i -> {1} ]}
+600a564,567
+> # Gauges domain:
+> V: [{[ i -> {1} ]}]
+> s398: λ([0 .. 10])
+> {[ i -> {1} ]}
+665a633,637
+> # Gauges domain:
+> V: [{[ p -> {{ &a }}
+> i -> {2} ]}]
+> s412: λ(0)
+> s411: λ(0)
+726a699,703
+> # Gauges domain:
+> V: [{[ i -> {2} ]}]
+> s412: λ(0)
+> s411: λ([0 .. 1])
+> {[ i -> {0} ]}
+728a706,833
+> [eva] tests/value/gauges.c:325:
+> Frama_C_dump_each:
+> # Cvalue domain:
+> __fc_heap_status ∈ [--..--]
+> __fc_random_counter ∈ [--..--]
+> __fc_rand_max ∈ {32767}
+> __fc_random48_init ∈ {0}
+> __fc_random48_counter[0..2] ∈ [--..--]
+> __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
+> __fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
+> [1] ∈ {{ NULL ; &S_1___fc_env[0] }}
+> [2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
+> __fc_mblen_state ∈ [--..--]
+> __fc_mbtowc_state ∈ [--..--]
+> __fc_wctomb_state ∈ [--..--]
+> v ∈ [--..--]
+> t[0..4] ∈ {0}
+> [5] ∈ [0..48],0%3
+> [6] ∈ {0}
+> [7] ∈ [0..48],0%3
+> [8] ∈ {0}
+> [9] ∈ [0..48],0%3
+> [10] ∈ {0}
+> [11] ∈ [0..48],0%3
+> [12] ∈ {0}
+> [13] ∈ [0..48],0%3
+> [14] ∈ {0}
+> [15] ∈ [0..48],0%3
+> [16] ∈ {0}
+> [17] ∈ [0..48],0%3
+> [18] ∈ {0}
+> [19] ∈ [0..48],0%3
+> [20] ∈ {0}
+> [21] ∈ [0..48],0%3
+> [22] ∈ {0}
+> [23] ∈ [0..48],0%3
+> [24] ∈ {0}
+> [25] ∈ [0..48],0%3
+> [26] ∈ {0}
+> [27] ∈ [0..48],0%3
+> [28] ∈ {0}
+> [29] ∈ [0..48],0%3
+> [30] ∈ {0}
+> [31] ∈ [0..48],0%3
+> [32] ∈ {0}
+> [33] ∈ [0..48],0%3
+> [34] ∈ {0}
+> [35] ∈ [0..48],0%3
+> [36] ∈ {0}
+> [37] ∈ [0..48],0%3
+> u[0..99] ∈ [0..100]
+> T[0..99] ∈ [--..--]
+> a ∈ {1}
+> b ∈ {0}
+> p ∈ {{ &a ; &b }}
+> i ∈ {2}
+> S_0___fc_env[0..1] ∈ [--..--]
+> S_1___fc_env[0..1] ∈ [--..--]
+> # Gauges domain:
+> V: [{[ i -> {2} ]}]
+> s412: λ(0)
+> s411: λ([0 .. 2])
+> {[ i -> {0} ]}
+> ==END OF DUMP==
+> [eva] tests/value/gauges.c:325:
+> Frama_C_dump_each:
+> # Cvalue domain:
+> __fc_heap_status ∈ [--..--]
+> __fc_random_counter ∈ [--..--]
+> __fc_rand_max ∈ {32767}
+> __fc_random48_init ∈ {0}
+> __fc_random48_counter[0..2] ∈ [--..--]
+> __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
+> __fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
+> [1] ∈ {{ NULL ; &S_1___fc_env[0] }}
+> [2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
+> __fc_mblen_state ∈ [--..--]
+> __fc_mbtowc_state ∈ [--..--]
+> __fc_wctomb_state ∈ [--..--]
+> v ∈ [--..--]
+> t[0..4] ∈ {0}
+> [5] ∈ [0..48],0%3
+> [6] ∈ {0}
+> [7] ∈ [0..48],0%3
+> [8] ∈ {0}
+> [9] ∈ [0..48],0%3
+> [10] ∈ {0}
+> [11] ∈ [0..48],0%3
+> [12] ∈ {0}
+> [13] ∈ [0..48],0%3
+> [14] ∈ {0}
+> [15] ∈ [0..48],0%3
+> [16] ∈ {0}
+> [17] ∈ [0..48],0%3
+> [18] ∈ {0}
+> [19] ∈ [0..48],0%3
+> [20] ∈ {0}
+> [21] ∈ [0..48],0%3
+> [22] ∈ {0}
+> [23] ∈ [0..48],0%3
+> [24] ∈ {0}
+> [25] ∈ [0..48],0%3
+> [26] ∈ {0}
+> [27] ∈ [0..48],0%3
+> [28] ∈ {0}
+> [29] ∈ [0..48],0%3
+> [30] ∈ {0}
+> [31] ∈ [0..48],0%3
+> [32] ∈ {0}
+> [33] ∈ [0..48],0%3
+> [34] ∈ {0}
+> [35] ∈ [0..48],0%3
+> [36] ∈ {0}
+> [37] ∈ [0..48],0%3
+> u[0..99] ∈ [0..100]
+> T[0..99] ∈ [--..--]
+> a ∈ {1}
+> b ∈ {0}
+> p ∈ {{ &a ; &b }}
+> i ∈ {2}
+> S_0___fc_env[0..1] ∈ [--..--]
+> S_1___fc_env[0..1] ∈ [--..--]
+> # Gauges domain:
+> V: [{[ i -> {2} ]}]
+> s412: λ(0)
+> s411: λ([0 .. +oo])
+> {[ i -> {0} ]}
+> ==END OF DUMP==
+736a842,843
+> [eva] tests/value/gauges.c:343: Call to builtin malloc
+> [eva] tests/value/gauges.c:343: Call to builtin malloc
+789,790c896,897
+< A ∈ {{ &A + [0..--],0%4 }}
+< B ∈ {{ &B + [0..--],0%4 }}
+---
+> A ∈ {{ &A + [0..36],0%4 }}
+> B ∈ {{ &B + [0..36],0%4 }}
+802c909
+< n ∈ [-2147483648..99]
+---
+> n ∈ [-2147483547..99]
+808c915
+< i ∈ {45; 46; 47; 48; 49; 50; 51}
+---
+> i ∈ {45; 46; 47; 48}
+814c921
+< i ∈ {-59; -58; -57; -56; -55; -54; -53}
+---
+> i ∈ {-58; -57; -56; -55; -54; -53}
+834c941
+< p ∈ {{ &u + [0..--],0%4 }}
+---
+> p ∈ {{ &u + [0..400],0%4 }}
+836c943
+< k ∈ [0..2147483647]
+---
+> k ∈ [0..390]
+841c948
+< i ∈ [0..2147483647]
+---
+> i ∈ [0..21]
+852,853c959,961
+< [1..9] ∈ {4; 5; 6; 7; 8; 9} or UNINITIALIZED
+< p ∈ {{ &y + [4..40],0%4 }}
+---
+> [1..6] ∈ {4; 5; 6; 7; 8; 9} or UNINITIALIZED
+> [7..9] ∈ UNINITIALIZED
+> p ∈ {{ &y[7] }}
+864c972
+< p ∈ {{ &T + [--..396],0%4 }}
+---
+> p ∈ {{ &T + [-4..396],0%4 }}
+869,873c977
+< n ∈ {0}
+< arr[0] ∈ {0}
+< [1] ∈ {-1}
+< [2..65535] ∈ [--..--] or UNINITIALIZED
+< p ∈ {{ &arr + [12..--],0%4 }}
+---
+> NON TERMINATING FUNCTION
+976a1081
+> [from] Non-terminating function main8_aux (no dependencies)
+999,1000c1104,1105
+< p FROM p; A; B; n; p; A[0..9]; B[0..9] (and SELF)
+< \result FROM p; A; B; n; p; A[0..9]; B[0..9]
+---
+> p FROM p; A; B; n; p; A[0..8]; B[0..8] (and SELF)
+> \result FROM p; A; B; n; p; A[0..8]; B[0..8]
+1044c1149
+< NO EFFECTS
+---
+> NON TERMINATING - NO EFFECTS
+1078c1183
+< p; A[0..9]; B[0..9]
+---
+> p; A[0..8]; B[0..8]
diff --git a/tests/value/oracle_gauges/ghost.res.oracle b/tests/value/oracle_gauges/ghost.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/global_bug.res.oracle b/tests/value/oracle_gauges/global_bug.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/goto.res.oracle b/tests/value/oracle_gauges/goto.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/hierarchical_convergence.res.oracle b/tests/value/oracle_gauges/hierarchical_convergence.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..dfe4a55a8d5655bd3e9b1c913be588bdf10ac87c
--- /dev/null
+++ b/tests/value/oracle_gauges/hierarchical_convergence.res.oracle
@@ -0,0 +1,2 @@
+15a16
+> [eva] tests/value/hierarchical_convergence.c:10: Frama_C_show_each: {1}, {0}
diff --git a/tests/value/oracle_gauges/if.0.res.oracle b/tests/value/oracle_gauges/if.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/if.1.res.oracle b/tests/value/oracle_gauges/if.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/if2.res.oracle b/tests/value/oracle_gauges/if2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/ilevel.res.oracle b/tests/value/oracle_gauges/ilevel.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/implies.res.oracle b/tests/value/oracle_gauges/implies.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/imprecise_invalid_write.res.oracle b/tests/value/oracle_gauges/imprecise_invalid_write.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/incompatible_states.res.oracle b/tests/value/oracle_gauges/incompatible_states.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/incorrect_reduce_expr.res.oracle b/tests/value/oracle_gauges/incorrect_reduce_expr.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/ineq.res.oracle b/tests/value/oracle_gauges/ineq.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/infinite.res.oracle b/tests/value/oracle_gauges/infinite.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..4acec0b99e24e8dc0e6f48456b2475191ac9831a
--- /dev/null
+++ b/tests/value/oracle_gauges/infinite.res.oracle
@@ -0,0 +1,11 @@
+12a13,22
+> [eva] tests/value/infinite.i:6: starting to merge loop iterations
+> [eva] computing for function pause <- main.
+> Called from tests/value/infinite.i:9.
+> [eva] Done for function pause
+> [eva] computing for function pause <- main.
+> Called from tests/value/infinite.i:9.
+> [eva] Done for function pause
+> [eva] computing for function pause <- main.
+> Called from tests/value/infinite.i:9.
+> [eva] Done for function pause
diff --git a/tests/value/oracle_gauges/init.0.res.oracle b/tests/value/oracle_gauges/init.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/init.1.res.oracle b/tests/value/oracle_gauges/init.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/init_const_guard.res.oracle b/tests/value/oracle_gauges/init_const_guard.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/initialized.res.oracle b/tests/value/oracle_gauges/initialized.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/initialized_copy.0.res.oracle b/tests/value/oracle_gauges/initialized_copy.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/initialized_copy.1.res.oracle b/tests/value/oracle_gauges/initialized_copy.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/inout.0.res.oracle b/tests/value/oracle_gauges/inout.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/inout.1.res.oracle b/tests/value/oracle_gauges/inout.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/inout.2.res.oracle b/tests/value/oracle_gauges/inout.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..fdad47271b2c2f0231b62d27778cea169de9e3c2
--- /dev/null
+++ b/tests/value/oracle_gauges/inout.2.res.oracle
@@ -0,0 +1,2 @@
+22a23
+> [eva] tests/value/inout.i:50: starting to merge loop iterations
diff --git a/tests/value/oracle_gauges/inout.3.res.oracle b/tests/value/oracle_gauges/inout.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c2d0b9893381f3f084603b0a50cc3c73e4f9c840
--- /dev/null
+++ b/tests/value/oracle_gauges/inout.3.res.oracle
@@ -0,0 +1,2 @@
+22a23
+> [eva] tests/value/inout.i:60: starting to merge loop iterations
diff --git a/tests/value/oracle_gauges/inout.4.res.oracle b/tests/value/oracle_gauges/inout.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3b6b4fc2ae125a92e0abfe0e3b7bb65dd7e6d523
--- /dev/null
+++ b/tests/value/oracle_gauges/inout.4.res.oracle
@@ -0,0 +1,2 @@
+24a25
+> [eva] tests/value/inout.i:60: starting to merge loop iterations
diff --git a/tests/value/oracle_gauges/inout_diff.res.oracle b/tests/value/oracle_gauges/inout_diff.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/inout_formals.res.oracle b/tests/value/oracle_gauges/inout_formals.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/inout_on_alarms.res.oracle b/tests/value/oracle_gauges/inout_on_alarms.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/inout_proto.res.oracle b/tests/value/oracle_gauges/inout_proto.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/input.res.oracle b/tests/value/oracle_gauges/input.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/integers.res.oracle b/tests/value/oracle_gauges/integers.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/interpol.res.oracle b/tests/value/oracle_gauges/interpol.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/interpreter-mode-syracuse.res.oracle b/tests/value/oracle_gauges/interpreter-mode-syracuse.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/invalid_loc_return.res.oracle b/tests/value/oracle_gauges/invalid_loc_return.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/invalid_lval_arg.res.oracle b/tests/value/oracle_gauges/invalid_lval_arg.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/invalid_pointer.0.res.oracle b/tests/value/oracle_gauges/invalid_pointer.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/invalid_pointer.1.res.oracle b/tests/value/oracle_gauges/invalid_pointer.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/inversion.res.oracle b/tests/value/oracle_gauges/inversion.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/inversion2.res.oracle b/tests/value/oracle_gauges/inversion2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/jacques.res.oracle b/tests/value/oracle_gauges/jacques.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/join_misaligned.res.oracle b/tests/value/oracle_gauges/join_misaligned.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/label.res.oracle b/tests/value/oracle_gauges/label.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/lazy.0.res.oracle b/tests/value/oracle_gauges/lazy.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/lazy.1.res.oracle b/tests/value/oracle_gauges/lazy.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/leaf.res.oracle b/tests/value/oracle_gauges/leaf.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/leaf2.res.oracle b/tests/value/oracle_gauges/leaf2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/leaf_spec.0.res.oracle b/tests/value/oracle_gauges/leaf_spec.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/leaf_spec.1.res.oracle b/tests/value/oracle_gauges/leaf_spec.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/library.res.oracle b/tests/value/oracle_gauges/library.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/library_precond.res.oracle b/tests/value/oracle_gauges/library_precond.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/limits.res.oracle b/tests/value/oracle_gauges/limits.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/local.res.oracle b/tests/value/oracle_gauges/local.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/local_cleanup.res.oracle b/tests/value/oracle_gauges/local_cleanup.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/local_slevel.res.oracle b/tests/value/oracle_gauges/local_slevel.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3329f131e3c9ff467f4c369b90394fcfd7cca6e9
--- /dev/null
+++ b/tests/value/oracle_gauges/local_slevel.res.oracle
@@ -0,0 +1,72 @@
+13,15c13,15
+< [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}
+---
+> [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}
+18c18
+< 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}
+22c22
+< 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}
+26,34c26
+< 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]
+< [eva] tests/value/local_slevel.i:18:
+< Frama_C_show_each: {1}, [1..79],1%2, [0..2147483648]
+< [eva] tests/value/local_slevel.i:18:
+< Frama_C_show_each: {-1}, [0..78],0%2, [0..2147483648]
+< [eva] tests/value/local_slevel.i:18:
+< Frama_C_show_each: {1}, [1..79],1%2, [0..4294967295]
+---
+> Frama_C_show_each: {1}, [1..79],1%2, [1..79]
+36c28
+< Frama_C_show_each: {-1}, [0..78],0%2, [0..4294967295]
+---
+> Frama_C_show_each: {-1}, [0..78],0%2, [0..78]
+152c144
+< r ∈ [--..--]
+---
+> r ∈ [0..2147483647]
+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}
+---
+> [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}
+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}
+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}
+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]
+< [eva] tests/value/local_slevel.i:18:
+< Frama_C_show_each: {1}, [1..79],1%2, [0..2147483648]
+< [eva] tests/value/local_slevel.i:18:
+< Frama_C_show_each: {-1}, [0..78],0%2, [0..2147483648]
+< [eva] tests/value/local_slevel.i:18:
+< Frama_C_show_each: {1}, [1..79],1%2, [0..4294967295]
+---
+> Frama_C_show_each: {1}, [1..79],1%2, [1..79]
+416c400
+< Frama_C_show_each: {-1}, [0..78],0%2, [0..4294967295]
+---
+> Frama_C_show_each: {-1}, [0..78],0%2, [0..78]
+532c516
+< r ∈ [--..--]
+---
+> r ∈ [0..2147483647]
diff --git a/tests/value/oracle_gauges/local_variables.res.oracle b/tests/value/oracle_gauges/local_variables.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/lock.res.oracle b/tests/value/oracle_gauges/lock.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/logic.res.oracle b/tests/value/oracle_gauges/logic.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/logic_ptr_cast.res.oracle b/tests/value/oracle_gauges/logic_ptr_cast.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/logicdeps.res.oracle b/tests/value/oracle_gauges/logicdeps.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/long.res.oracle b/tests/value/oracle_gauges/long.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/long_const.0.res.oracle b/tests/value/oracle_gauges/long_const.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/long_const.1.res.oracle b/tests/value/oracle_gauges/long_const.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/loop.res.oracle b/tests/value/oracle_gauges/loop.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/loop1.res.oracle b/tests/value/oracle_gauges/loop1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/loop2.res.oracle b/tests/value/oracle_gauges/loop2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/loop3.res.oracle b/tests/value/oracle_gauges/loop3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/loop_array.res.oracle b/tests/value/oracle_gauges/loop_array.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/loop_join.res.oracle b/tests/value/oracle_gauges/loop_join.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/loop_long.res.oracle b/tests/value/oracle_gauges/loop_long.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/loop_no_var.res.oracle b/tests/value/oracle_gauges/loop_no_var.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..13d459a97d0afd893e1fcc8004d26061c0c3374e
--- /dev/null
+++ b/tests/value/oracle_gauges/loop_no_var.res.oracle
@@ -0,0 +1,2 @@
+6a7
+> [eva] tests/value/loop_no_var.i:3: starting to merge loop iterations
diff --git a/tests/value/oracle_gauges/loop_simple.res.oracle b/tests/value/oracle_gauges/loop_simple.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/loop_test.0.res.oracle b/tests/value/oracle_gauges/loop_test.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/loop_test.1.res.oracle b/tests/value/oracle_gauges/loop_test.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/loop_wvar.0.res.oracle b/tests/value/oracle_gauges/loop_wvar.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/loop_wvar.1.res.oracle b/tests/value/oracle_gauges/loop_wvar.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3cbd56d943b6f61678b7adcf19d622740d6de48c
--- /dev/null
+++ b/tests/value/oracle_gauges/loop_wvar.1.res.oracle
@@ -0,0 +1,11 @@
+27,28c27
+< [eva] tests/value/loop_wvar.i:71: Frama_C_show_each: [0..9], [0..17], [0..11]
+< [eva] tests/value/loop_wvar.i:71: Frama_C_show_each: [0..9], [0..18], [0..12]
+---
+> [eva] tests/value/loop_wvar.i:71: Frama_C_show_each: [0..9], [0..9], [0..9]
+37,38c36,37
+< j ∈ [0..18]
+< k ∈ [0..12]
+---
+> j ∈ [0..17]
+> k ∈ [0..11]
diff --git a/tests/value/oracle_gauges/loop_wvar.2.res.oracle b/tests/value/oracle_gauges/loop_wvar.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/loop_wvar.3.res.oracle b/tests/value/oracle_gauges/loop_wvar.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/loopfun.0.res.oracle b/tests/value/oracle_gauges/loopfun.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/loopfun.1.res.oracle b/tests/value/oracle_gauges/loopfun.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..4096faa0f9f092b7604436dd52ab6fd629a1d229
--- /dev/null
+++ b/tests/value/oracle_gauges/loopfun.1.res.oracle
@@ -0,0 +1,8 @@
+9a10,12
+> [eva] tests/value/loopfun.i:23: starting to merge loop iterations
+> [eva:loop-unroll] tests/value/loopfun.i:25: loop not completely unrolled
+> [eva] tests/value/loopfun.i:25: starting to merge loop iterations
+11a15
+> [eva] tests/value/loopfun.i:26: starting to merge loop iterations
+13a18
+> [eva] tests/value/loopfun.i:27: starting to merge loop iterations
diff --git a/tests/value/oracle_gauges/loopinv.res.oracle b/tests/value/oracle_gauges/loopinv.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e109e23df9c3fac971ea0f2322245e6f87748f00
--- /dev/null
+++ b/tests/value/oracle_gauges/loopinv.res.oracle
@@ -0,0 +1,21 @@
+72,74c72
+< [eva:alarm] tests/value/loopinv.c:69: Warning:
+< loop invariant got status unknown.
+< [eva] tests/value/loopinv.c:71: Frama_C_show_each: {0; 2; 4; 6; 8}, [1..107]
+---
+> [eva] tests/value/loopinv.c:71: Frama_C_show_each: {0; 2; 4; 6; 8}, [1..106]
+79,80c77,78
+< [eva:alarm] tests/value/loopinv.c:73: Warning:
+< signed overflow. assert i + 1 ≤ 2147483647;
+---
+> [eva:alarm] tests/value/loopinv.c:69: Warning:
+> loop invariant got status unknown.
+175,176d172
+< [ - ] Assertion 'Eva,signed_overflow' (file tests/value/loopinv.c, line 73)
+< tried with Eva.
+182,183c178,179
+< 7 To be validated
+< 16 Total
+---
+> 6 To be validated
+> 15 Total
diff --git a/tests/value/oracle_gauges/machdep.res.oracle b/tests/value/oracle_gauges/machdep.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/max_pointed.res.oracle b/tests/value/oracle_gauges/max_pointed.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/memexec.res.oracle b/tests/value/oracle_gauges/memexec.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b06de9e7bb50aba248ba8582c53d7fa6804d6e6a
--- /dev/null
+++ b/tests/value/oracle_gauges/memexec.res.oracle
@@ -0,0 +1,2 @@
+101a102
+> [eva] tests/value/memexec.c:98: starting to merge loop iterations
diff --git a/tests/value/oracle_gauges/merge_bits.res.oracle b/tests/value/oracle_gauges/merge_bits.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/mini_pointrer.res.oracle b/tests/value/oracle_gauges/mini_pointrer.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/misaligned_tabs.res.oracle b/tests/value/oracle_gauges/misaligned_tabs.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/mixed_val.res.oracle b/tests/value/oracle_gauges/mixed_val.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/modifies.res.oracle b/tests/value/oracle_gauges/modifies.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/modulo.res.oracle b/tests/value/oracle_gauges/modulo.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..385e0e184c17b3aec284e3d184fed36779f83a92
--- /dev/null
+++ b/tests/value/oracle_gauges/modulo.res.oracle
@@ -0,0 +1,186 @@
+40a41,123
+> [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}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> [-9..-1], {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1; 0}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> [-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:
+> {-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},
+> {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}
+> [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}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> {-7; -6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5; 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}, {-6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1:
+> {-7; -6; -5; -4; -3; -2; -1},
+> {-6; -5; -4; -3; -2; -1},
+> {-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}
+> [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:
+> {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:
+> Frama_C_show_each_1: {-5; -4; -3; -2; -1}, {1; 2; 3; 4}, {-3; -2; -1; 0}
+> [eva] tests/value/modulo.i:41:
+> Frama_C_show_each_1: {1; 2; 3; 4; 5}, {-4; -3; -2; -1}, {0; 1; 2; 3}
+> [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: {-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: {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: {-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: [-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..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], {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..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:
+> {-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: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}
+> [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}, {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; 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}
+> [eva] tests/value/modulo.i:53:
+> 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; 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}, {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; 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; 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}, {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}
+> [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]
+> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-8..8], [-7..7], [-6..6]
+> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-7..7], [-6..6], [-5..5]
+> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-6..6], [-5..5], [-4..4]
+> [eva] tests/value/modulo.i:64:
+> Frama_C_show_each_3:
+> [-5..5], {-4; -3; -2; -1; 1; 2; 3; 4}, {-3; -2; -1; 0; 1; 2; 3}
+> [eva] tests/value/modulo.i:64:
+> Frama_C_show_each_3:
+> {-4; -3; -2; -1; 1; 2; 3; 4}, {-3; -2; -1; 1; 2; 3}, {-2; -1; 0; 1; 2}
+> [eva] tests/value/modulo.i:64:
+> Frama_C_show_each_3: {-3; -2; -1; 1; 2; 3}, {-2; -1; 1; 2}, {-1; 0; 1}
+> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: {-2; -1; 1; 2}, {-1; 1}, {0}
+81a262,263
+> [eva] tests/value/modulo.i:95: starting to merge loop iterations
+> [eva] tests/value/modulo.i:82: starting to merge loop iterations
diff --git a/tests/value/oracle_gauges/multi_access.res.oracle b/tests/value/oracle_gauges/multi_access.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/narrow_behaviors.res.oracle b/tests/value/oracle_gauges/narrow_behaviors.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/nested_struct_init.res.oracle b/tests/value/oracle_gauges/nested_struct_init.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/no_results.res.oracle b/tests/value/oracle_gauges/no_results.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/non_iso_initializer.res.oracle b/tests/value/oracle_gauges/non_iso_initializer.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/non_natural.res.oracle b/tests/value/oracle_gauges/non_natural.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..bc1e48d293fd33ea035d51d8740f9d028f0eee40
--- /dev/null
+++ b/tests/value/oracle_gauges/non_natural.res.oracle
@@ -0,0 +1,178 @@
+60,63c60
+< Frama_C_show_each: {{ &p2 + [0..400000],0%32 }}
+< [eva:alarm] tests/value/non_natural.i:23: Warning:
+< out of bounds write. assert \valid(tmp);
+< (tmp from to++)
+---
+> Frama_C_show_each: {{ &p2 + [0..399968],0%32 }}
+66,68d62
+< [eva:alarm] tests/value/non_natural.i:24: Warning:
+< out of bounds write. assert \valid(tmp_1);
+< (tmp_1 from to++)
+71,76d64
+< [eva:alarm] tests/value/non_natural.i:25: Warning:
+< out of bounds write. assert \valid(tmp_3);
+< (tmp_3 from to++)
+< [eva:alarm] tests/value/non_natural.i:25: Warning:
+< out of bounds read. assert \valid_read(tmp_4);
+< (tmp_4 from from++)
+79,84d66
+< [eva:alarm] tests/value/non_natural.i:26: Warning:
+< out of bounds write. assert \valid(tmp_5);
+< (tmp_5 from to++)
+< [eva:alarm] tests/value/non_natural.i:26: Warning:
+< out of bounds read. assert \valid_read(tmp_6);
+< (tmp_6 from from++)
+87,92d68
+< [eva:alarm] tests/value/non_natural.i:27: Warning:
+< out of bounds write. assert \valid(tmp_7);
+< (tmp_7 from to++)
+< [eva:alarm] tests/value/non_natural.i:27: Warning:
+< out of bounds read. assert \valid_read(tmp_8);
+< (tmp_8 from from++)
+95,100d70
+< [eva:alarm] tests/value/non_natural.i:28: Warning:
+< out of bounds write. assert \valid(tmp_9);
+< (tmp_9 from to++)
+< [eva:alarm] tests/value/non_natural.i:28: Warning:
+< out of bounds read. assert \valid_read(tmp_10);
+< (tmp_10 from from++)
+103,108d72
+< [eva:alarm] tests/value/non_natural.i:29: Warning:
+< out of bounds write. assert \valid(tmp_11);
+< (tmp_11 from to++)
+< [eva:alarm] tests/value/non_natural.i:29: Warning:
+< out of bounds read. assert \valid_read(tmp_12);
+< (tmp_12 from from++)
+111,125d74
+< [eva:alarm] tests/value/non_natural.i:30: Warning:
+< out of bounds write. assert \valid(tmp_13);
+< (tmp_13 from to++)
+< [eva:alarm] tests/value/non_natural.i:30: Warning:
+< out of bounds read. assert \valid_read(tmp_14);
+< (tmp_14 from from++)
+< [eva] tests/value/non_natural.i:22:
+< Frama_C_show_each: {{ &p2 + [0..400032],0%32 }}
+< [eva:alarm] tests/value/non_natural.i:23: Warning:
+< out of bounds read. assert \valid_read(tmp_0);
+< (tmp_0 from from++)
+< [eva:alarm] tests/value/non_natural.i:24: Warning:
+< out of bounds read. assert \valid_read(tmp_2);
+< (tmp_2 from from++)
+< [eva] tests/value/non_natural.i:22: Frama_C_show_each: {{ &p2 + [0..--],0%32 }}
+128,129d76
+< more than 200(12501) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:23:
+132,133d78
+< more than 200(12501) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:24:
+194,197c139
+< Frama_C_show_each: {{ &p2 + [0..400000],0%32 }}
+< [eva:alarm] tests/value/non_natural.i:39: Warning:
+< out of bounds write. assert \valid(tmp);
+< (tmp from to++)
+---
+> Frama_C_show_each: {{ &p2 + [0..399968],0%32 }}
+200,202d141
+< [eva:alarm] tests/value/non_natural.i:40: Warning:
+< out of bounds write. assert \valid(tmp_1);
+< (tmp_1 from to++)
+205,210d143
+< [eva:alarm] tests/value/non_natural.i:41: Warning:
+< out of bounds write. assert \valid(tmp_3);
+< (tmp_3 from to++)
+< [eva:alarm] tests/value/non_natural.i:41: Warning:
+< out of bounds read. assert \valid_read(tmp_4);
+< (tmp_4 from from++)
+213,218d145
+< [eva:alarm] tests/value/non_natural.i:42: Warning:
+< out of bounds write. assert \valid(tmp_5);
+< (tmp_5 from to++)
+< [eva:alarm] tests/value/non_natural.i:42: Warning:
+< out of bounds read. assert \valid_read(tmp_6);
+< (tmp_6 from from++)
+221,226d147
+< [eva:alarm] tests/value/non_natural.i:43: Warning:
+< out of bounds write. assert \valid(tmp_7);
+< (tmp_7 from to++)
+< [eva:alarm] tests/value/non_natural.i:43: Warning:
+< out of bounds read. assert \valid_read(tmp_8);
+< (tmp_8 from from++)
+229,234d149
+< [eva:alarm] tests/value/non_natural.i:44: Warning:
+< out of bounds write. assert \valid(tmp_9);
+< (tmp_9 from to++)
+< [eva:alarm] tests/value/non_natural.i:44: Warning:
+< out of bounds read. assert \valid_read(tmp_10);
+< (tmp_10 from from++)
+237,242d151
+< [eva:alarm] tests/value/non_natural.i:45: Warning:
+< out of bounds write. assert \valid(tmp_11);
+< (tmp_11 from to++)
+< [eva:alarm] tests/value/non_natural.i:45: Warning:
+< out of bounds read. assert \valid_read(tmp_12);
+< (tmp_12 from from++)
+245,259d153
+< [eva:alarm] tests/value/non_natural.i:46: Warning:
+< out of bounds write. assert \valid(tmp_13);
+< (tmp_13 from to++)
+< [eva:alarm] tests/value/non_natural.i:46: Warning:
+< out of bounds read. assert \valid_read(tmp_14);
+< (tmp_14 from from++)
+< [eva] tests/value/non_natural.i:38:
+< Frama_C_show_each: {{ &p2 + [0..400032],0%32 }}
+< [eva:alarm] tests/value/non_natural.i:39: Warning:
+< out of bounds read. assert \valid_read(tmp_0);
+< (tmp_0 from from++)
+< [eva:alarm] tests/value/non_natural.i:40: Warning:
+< out of bounds read. assert \valid_read(tmp_2);
+< (tmp_2 from from++)
+< [eva] tests/value/non_natural.i:38: Frama_C_show_each: {{ &p2 + [0..--],0%32 }}
+268,269c162,163
+< to ∈ {{ &p2 + [32..--],0%32 }}
+< from ∈ {{ &p1 + [32..--],0%32 }}
+---
+> to ∈ {{ &p2 + [32..400000],0%32 }}
+> from ∈ {{ &p1 + [32..400000],0%32 }}
+273,274c167,168
+< to ∈ {{ &p2 + [32..--],0%32 }}
+< from ∈ {{ &p1 + [32..--],0%32 }}
+---
+> to ∈ {{ &p2 + [32..400000],0%32 }}
+> from ∈ {{ &p1 + [32..400000],0%32 }}
+330,332c224,232
+< p2[0] FROM to; from; count; p1[0..100000] (and SELF)
+< [1..99992] FROM to; from; count; p1[0..100001] (and SELF)
+< [99993] FROM to; from; count; p1[1..100001] (and SELF)
+---
+> p2[0] FROM to; from; count; p1[0..99992] (and SELF)
+> [1] FROM to; from; count; p1[0..99993] (and SELF)
+> [2] FROM to; from; count; p1[0..99994] (and SELF)
+> [3] FROM to; from; count; p1[0..99995] (and SELF)
+> [4] FROM to; from; count; p1[0..99996] (and SELF)
+> [5] FROM to; from; count; p1[0..99997] (and SELF)
+> [6] FROM to; from; count; p1[0..99998] (and SELF)
+> [7..99992] FROM to; from; count; p1[0..99999] (and SELF)
+> [99993] FROM to; from; count; p1[1..99999] (and SELF)
+340,342c240,248
+< p2[0] FROM to; from; count; p1[0..100000] (and SELF)
+< [1..99992] FROM to; from; count; p1[0..100001] (and SELF)
+< [99993] FROM to; from; count; p1[1..100001] (and SELF)
+---
+> p2[0] FROM to; from; count; p1[0..99992] (and SELF)
+> [1] FROM to; from; count; p1[0..99993] (and SELF)
+> [2] FROM to; from; count; p1[0..99994] (and SELF)
+> [3] FROM to; from; count; p1[0..99995] (and SELF)
+> [4] FROM to; from; count; p1[0..99996] (and SELF)
+> [5] FROM to; from; count; p1[0..99997] (and SELF)
+> [6] FROM to; from; count; p1[0..99998] (and SELF)
+> [7..99992] FROM to; from; count; p1[0..99999] (and SELF)
+> [99993] FROM to; from; count; p1[1..99999] (and SELF)
+360c266
+< p1[0..100001]
+---
+> p1[0..99999]
+365c271
+< p1[0..100001]
+---
+> p1[0..99999]
diff --git a/tests/value/oracle_gauges/nonlin.res.oracle b/tests/value/oracle_gauges/nonlin.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/noreturn.res.oracle b/tests/value/oracle_gauges/noreturn.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..2f5c57570724a6b5ec84cc978235676a03e61149
--- /dev/null
+++ b/tests/value/oracle_gauges/noreturn.res.oracle
@@ -0,0 +1,8 @@
+8a9
+> [eva] tests/value/noreturn.i:20: starting to merge loop iterations
+16a18
+> [eva] tests/value/noreturn.i:16: starting to merge loop iterations
+32a35
+> [eva] tests/value/noreturn.i:7: starting to merge loop iterations
+36a40
+> [eva] tests/value/noreturn.i:13: starting to merge loop iterations
diff --git a/tests/value/oracle_gauges/not.res.oracle b/tests/value/oracle_gauges/not.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/not_ct_array_arg.res.oracle b/tests/value/oracle_gauges/not_ct_array_arg.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/null_lt_valid.res.oracle b/tests/value/oracle_gauges/null_lt_valid.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/octagons.res.oracle b/tests/value/oracle_gauges/octagons.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..49fefa1dc489947ad79cb8b973f9804fbb184331
--- /dev/null
+++ b/tests/value/oracle_gauges/octagons.res.oracle
@@ -0,0 +1,27 @@
+121,128d120
+< [eva:alarm] tests/value/octagons.c:107: Warning:
+< signed overflow. assert a + 2 ≤ 2147483647;
+< [eva:alarm] tests/value/octagons.c:108: Warning:
+< signed overflow. assert b + 2 ≤ 2147483647;
+< [eva:alarm] tests/value/octagons.c:110: Warning:
+< signed overflow. assert a + k ≤ 2147483647;
+< [eva:alarm] tests/value/octagons.c:113: Warning:
+< signed overflow. assert -2147483648 ≤ c - a;
+130c122
+< [eva] tests/value/octagons.c:116: Frama_C_show_each_imprecise: [-2147483648..1]
+---
+> [eva] tests/value/octagons.c:116: Frama_C_show_each_imprecise: [-2468..1]
+284,287c276,279
+< a ∈ [-1024..2147483647]
+< b ∈ [-1023..2147483647]
+< c ∈ [-1023..2147483647]
+< d ∈ [-1032..2147483647]
+---
+> a ∈ [-182..1866]
+> b ∈ [-181..1867]
+> c ∈ [-602..1446]
+> d ∈ [-190..1874]
+289c281
+< d2 ∈ [-2147483648..1]
+---
+> d2 ∈ [-2468..1]
diff --git a/tests/value/oracle_gauges/offset_misaligned.res.oracle b/tests/value/oracle_gauges/offset_misaligned.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/offset_neg.res.oracle b/tests/value/oracle_gauges/offset_neg.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/offset_top.res.oracle b/tests/value/oracle_gauges/offset_top.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/offsetmap.0.res.oracle b/tests/value/oracle_gauges/offsetmap.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/offsetmap.1.res.oracle b/tests/value/oracle_gauges/offsetmap.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/origin.0.res.oracle b/tests/value/oracle_gauges/origin.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/origin.1.res.oracle b/tests/value/oracle_gauges/origin.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/output_leafs.res.oracle b/tests/value/oracle_gauges/output_leafs.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/overflow.0.res.oracle b/tests/value/oracle_gauges/overflow.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/overflow.1.res.oracle b/tests/value/oracle_gauges/overflow.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/overflow_cast_float_int.res.oracle b/tests/value/oracle_gauges/overflow_cast_float_int.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/packed.res.oracle b/tests/value/oracle_gauges/packed.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/partitioning-annots.0.res.oracle b/tests/value/oracle_gauges/partitioning-annots.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/partitioning-annots.1.res.oracle b/tests/value/oracle_gauges/partitioning-annots.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/partitioning-annots.2.res.oracle b/tests/value/oracle_gauges/partitioning-annots.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/partitioning-annots.3.res.oracle b/tests/value/oracle_gauges/partitioning-annots.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/partitioning-annots.4.res.oracle b/tests/value/oracle_gauges/partitioning-annots.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/partitioning-annots.5.res.oracle b/tests/value/oracle_gauges/partitioning-annots.5.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/partitioning-annots.6.res.oracle b/tests/value/oracle_gauges/partitioning-annots.6.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/pb.res.oracle b/tests/value/oracle_gauges/pb.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/period.res.oracle b/tests/value/oracle_gauges/period.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/plevel.res.oracle b/tests/value/oracle_gauges/plevel.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/pointer.res.oracle b/tests/value/oracle_gauges/pointer.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/pointer2.0.res.oracle b/tests/value/oracle_gauges/pointer2.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/pointer2.1.res.oracle b/tests/value/oracle_gauges/pointer2.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/pointer3.res.oracle b/tests/value/oracle_gauges/pointer3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/pointer4.res.oracle b/tests/value/oracle_gauges/pointer4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/pointer_arg.res.oracle b/tests/value/oracle_gauges/pointer_arg.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/pointer_comp.res.oracle b/tests/value/oracle_gauges/pointer_comp.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/pointer_comparison.0.res.oracle b/tests/value/oracle_gauges/pointer_comparison.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/pointer_comparison.1.res.oracle b/tests/value/oracle_gauges/pointer_comparison.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/pointer_int_cast.res.oracle b/tests/value/oracle_gauges/pointer_int_cast.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/pointer_loop.res.oracle b/tests/value/oracle_gauges/pointer_loop.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/postcond_leaf.res.oracle b/tests/value/oracle_gauges/postcond_leaf.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/postcondition.res.oracle b/tests/value/oracle_gauges/postcondition.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/pragma.res.oracle b/tests/value/oracle_gauges/pragma.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/precise_locations.res.oracle b/tests/value/oracle_gauges/precise_locations.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/precond.res.oracle b/tests/value/oracle_gauges/precond.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/precond2.0.res.oracle b/tests/value/oracle_gauges/precond2.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/precond2.1.res.oracle b/tests/value/oracle_gauges/precond2.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/propagate_bottom.res.oracle b/tests/value/oracle_gauges/propagate_bottom.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/protomain.res.oracle b/tests/value/oracle_gauges/protomain.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/ptr_call_object.res.oracle b/tests/value/oracle_gauges/ptr_call_object.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/ptr_relation.0.res.oracle b/tests/value/oracle_gauges/ptr_relation.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/ptr_relation.1.res.oracle b/tests/value/oracle_gauges/ptr_relation.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/ptr_relation.2.res.oracle b/tests/value/oracle_gauges/ptr_relation.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/pure_exp.res.oracle b/tests/value/oracle_gauges/pure_exp.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/qualified_arrays.res.oracle b/tests/value/oracle_gauges/qualified_arrays.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/raz.res.oracle b/tests/value/oracle_gauges/raz.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/reading_null.res.oracle b/tests/value/oracle_gauges/reading_null.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/rec.res.oracle b/tests/value/oracle_gauges/rec.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/recol.0.res.oracle b/tests/value/oracle_gauges/recol.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/recol.1.res.oracle b/tests/value/oracle_gauges/recol.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/recursion.0.res.oracle b/tests/value/oracle_gauges/recursion.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/recursion.1.res.oracle b/tests/value/oracle_gauges/recursion.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/recursion2.res.oracle b/tests/value/oracle_gauges/recursion2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/reduce_by_valid.res.oracle b/tests/value/oracle_gauges/reduce_by_valid.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/reduce_formals.res.oracle b/tests/value/oracle_gauges/reduce_formals.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..5d51c9b163e4132a3b20e36f9f4086a1d28e95bc
--- /dev/null
+++ b/tests/value/oracle_gauges/reduce_formals.res.oracle
@@ -0,0 +1,2 @@
+10a11
+> [eva] tests/value/reduce_formals.i:5: starting to merge loop iterations
diff --git a/tests/value/oracle_gauges/reduce_index.res.oracle b/tests/value/oracle_gauges/reduce_index.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/reduce_valid.res.oracle b/tests/value/oracle_gauges/reduce_valid.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/redundant_alarms.res.oracle b/tests/value/oracle_gauges/redundant_alarms.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6fb7421de9d4f5ed067d020701cefc81b86b6bb6
--- /dev/null
+++ b/tests/value/oracle_gauges/redundant_alarms.res.oracle
@@ -0,0 +1,2 @@
+47a48
+> [eva] tests/value/redundant_alarms.c:39: starting to merge loop iterations
diff --git a/tests/value/oracle_gauges/reevaluate_alarms.res.oracle b/tests/value/oracle_gauges/reevaluate_alarms.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..5ba638098acab6f3f08565ae63fb433b1e37acd8
--- /dev/null
+++ b/tests/value/oracle_gauges/reevaluate_alarms.res.oracle
@@ -0,0 +1,29 @@
+14,16d13
+< [eva:alarm] tests/value/reevaluate_alarms.i:14: Warning:
+< out of bounds write. assert \valid(tmp);
+< (tmp from p++)
+59c56
+< p ∈ {{ &T + [0..--],0%4 }}
+---
+> p ∈ {{ &T{[0], [1], [2], [3], [4], [5]} }}
+124,125d120
+< [ - ] Assertion 'Eva,mem_access' (file tests/value/reevaluate_alarms.i, line 14)
+< tried with Eva.
+144,145c139,140
+< 4 To be validated
+< 4 Total
+---
+> 3 To be validated
+> 3 Total
+182,183d176
+< [eva] tests/value/reevaluate_alarms.i:14:
+< assertion 'Eva,mem_access' got final status valid.
+274,275d266
+< [ Valid ] Assertion 'Eva,mem_access' (file tests/value/reevaluate_alarms.i, line 14)
+< by Eva (v2).
+294,295c285,286
+< 4 Completely validated
+< 4 Total
+---
+> 3 Completely validated
+> 3 Total
diff --git a/tests/value/oracle_gauges/relation_reduction.res.oracle b/tests/value/oracle_gauges/relation_reduction.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/relation_shift.res.oracle b/tests/value/oracle_gauges/relation_shift.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/relations.res.oracle b/tests/value/oracle_gauges/relations.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/relations2.res.oracle b/tests/value/oracle_gauges/relations2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/relations_difficult.res.oracle b/tests/value/oracle_gauges/relations_difficult.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/replace_by_show_each.res.oracle b/tests/value/oracle_gauges/replace_by_show_each.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/resolve.res.oracle b/tests/value/oracle_gauges/resolve.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/return.res.oracle b/tests/value/oracle_gauges/return.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/semaphore.res.oracle b/tests/value/oracle_gauges/semaphore.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3e2b1b2c86f6b84c4ccd64937b28643eadd26672
--- /dev/null
+++ b/tests/value/oracle_gauges/semaphore.res.oracle
@@ -0,0 +1,10 @@
+24a25,33
+> [eva] computing for function V <- g.
+> Called from tests/value/semaphore.i:31.
+> [eva] Done for function V
+> [eva] computing for function V <- g.
+> Called from tests/value/semaphore.i:31.
+> [eva] Done for function V
+> [eva] computing for function V <- g.
+> Called from tests/value/semaphore.i:31.
+> [eva] Done for function V
diff --git a/tests/value/oracle_gauges/separated.res.oracle b/tests/value/oracle_gauges/separated.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/shift.0.res.oracle b/tests/value/oracle_gauges/shift.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/shift.1.res.oracle b/tests/value/oracle_gauges/shift.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/shift_big.res.oracle b/tests/value/oracle_gauges/shift_big.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/shift_neg.0.res.oracle b/tests/value/oracle_gauges/shift_neg.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/shift_neg.1.res.oracle b/tests/value/oracle_gauges/shift_neg.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/sign_of_bitfiled_int.0.res.oracle b/tests/value/oracle_gauges/sign_of_bitfiled_int.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/sign_of_bitfiled_int.1.res.oracle b/tests/value/oracle_gauges/sign_of_bitfiled_int.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/simple_packed.res.oracle b/tests/value/oracle_gauges/simple_packed.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/simple_path.res.oracle b/tests/value/oracle_gauges/simple_path.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/simplify_cfg.0.res.oracle b/tests/value/oracle_gauges/simplify_cfg.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/simplify_cfg.1.res.oracle b/tests/value/oracle_gauges/simplify_cfg.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/sizeof.res.oracle b/tests/value/oracle_gauges/sizeof.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/slevel_return.res.oracle b/tests/value/oracle_gauges/slevel_return.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/slevelex.res.oracle b/tests/value/oracle_gauges/slevelex.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/small_conditionals.res.oracle b/tests/value/oracle_gauges/small_conditionals.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/sort4.0.res.oracle b/tests/value/oracle_gauges/sort4.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/sort4.1.res.oracle b/tests/value/oracle_gauges/sort4.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/sort4.2.res.oracle b/tests/value/oracle_gauges/sort4.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/split_return.0.res.oracle b/tests/value/oracle_gauges/split_return.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/split_return.1.res.oracle b/tests/value/oracle_gauges/split_return.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/split_return.2.res.oracle b/tests/value/oracle_gauges/split_return.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/split_return.3.res.oracle b/tests/value/oracle_gauges/split_return.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/split_return.4.res.oracle b/tests/value/oracle_gauges/split_return.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/statement_contract.res.oracle b/tests/value/oracle_gauges/statement_contract.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/static.res.oracle b/tests/value/oracle_gauges/static.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/strange.res.oracle b/tests/value/oracle_gauges/strange.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/strings.res.oracle b/tests/value/oracle_gauges/strings.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/strings_cond.res.oracle b/tests/value/oracle_gauges/strings_cond.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/struct.res.oracle b/tests/value/oracle_gauges/struct.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/struct2.res.oracle b/tests/value/oracle_gauges/struct2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/struct3.res.oracle b/tests/value/oracle_gauges/struct3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/struct_array.res.oracle b/tests/value/oracle_gauges/struct_array.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/struct_call.0.res.oracle b/tests/value/oracle_gauges/struct_call.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/struct_call.1.res.oracle b/tests/value/oracle_gauges/struct_call.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/struct_deps.res.oracle b/tests/value/oracle_gauges/struct_deps.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/struct_incl.res.oracle b/tests/value/oracle_gauges/struct_incl.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/struct_p_call.res.oracle b/tests/value/oracle_gauges/struct_p_call.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/strucval.res.oracle b/tests/value/oracle_gauges/strucval.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/subset.res.oracle b/tests/value/oracle_gauges/subset.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/summary.0.res.oracle b/tests/value/oracle_gauges/summary.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/summary.1.res.oracle b/tests/value/oracle_gauges/summary.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/summary.2.res.oracle b/tests/value/oracle_gauges/summary.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/summary.3.res.oracle b/tests/value/oracle_gauges/summary.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/summary.4.res.oracle b/tests/value/oracle_gauges/summary.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/switch.0.res.oracle b/tests/value/oracle_gauges/switch.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/switch.1.res.oracle b/tests/value/oracle_gauges/switch.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/switch2.res.oracle b/tests/value/oracle_gauges/switch2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/switch_cast.res.oracle b/tests/value/oracle_gauges/switch_cast.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/symbolic_locs.res.oracle b/tests/value/oracle_gauges/symbolic_locs.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7f734f6794dabb1fc73daf16cccb1bcb7381e1dc
--- /dev/null
+++ b/tests/value/oracle_gauges/symbolic_locs.res.oracle
@@ -0,0 +1,2 @@
+135a136
+> [eva] tests/value/symbolic_locs.i:93: starting to merge loop iterations
diff --git a/tests/value/oracle_gauges/tab.res.oracle b/tests/value/oracle_gauges/tab.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/tab1.res.oracle b/tests/value/oracle_gauges/tab1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/termination.res.oracle b/tests/value/oracle_gauges/termination.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/test.0.res.oracle b/tests/value/oracle_gauges/test.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/test.1.res.oracle b/tests/value/oracle_gauges/test.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/test_arith.res.oracle b/tests/value/oracle_gauges/test_arith.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/threat_array.res.oracle b/tests/value/oracle_gauges/threat_array.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/threat_if.res.oracle b/tests/value/oracle_gauges/threat_if.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/threat_redundant.res.oracle b/tests/value/oracle_gauges/threat_redundant.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/tricky_logic.res.oracle b/tests/value/oracle_gauges/tricky_logic.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/typedef_function.res.oracle b/tests/value/oracle_gauges/typedef_function.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/typeof.res.oracle b/tests/value/oracle_gauges/typeof.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/ulongvslonglong.0.res.oracle b/tests/value/oracle_gauges/ulongvslonglong.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/ulongvslonglong.1.res.oracle b/tests/value/oracle_gauges/ulongvslonglong.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/undef_behavior_bts1059.res.oracle b/tests/value/oracle_gauges/undef_behavior_bts1059.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/undef_fct.res.oracle b/tests/value/oracle_gauges/undef_fct.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/undefined_sequence.0.res.oracle b/tests/value/oracle_gauges/undefined_sequence.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e8f776c30713951ab4bd75cb835f4ed1b39e20c5
--- /dev/null
+++ b/tests/value/oracle_gauges/undefined_sequence.0.res.oracle
@@ -0,0 +1,4 @@
+97a98
+> [eva] tests/value/undefined_sequence.i:43: starting to merge loop iterations
+101a103
+> [eva] tests/value/undefined_sequence.i:49: starting to merge loop iterations
diff --git a/tests/value/oracle_gauges/undefined_sequence.1.res.oracle b/tests/value/oracle_gauges/undefined_sequence.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/undefined_sequence2.res.oracle b/tests/value/oracle_gauges/undefined_sequence2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/uninit.res.oracle b/tests/value/oracle_gauges/uninit.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/uninit_callstack.res.oracle b/tests/value/oracle_gauges/uninit_callstack.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/uninitialized_gnubody.res.oracle b/tests/value/oracle_gauges/uninitialized_gnubody.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/unknown_sizeof.0.res.oracle b/tests/value/oracle_gauges/unknown_sizeof.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/unknown_sizeof.1.res.oracle b/tests/value/oracle_gauges/unknown_sizeof.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/unop.res.oracle b/tests/value/oracle_gauges/unop.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/unroll.res.oracle b/tests/value/oracle_gauges/unroll.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..81a921960fb00c34b0d1f0636d2361c61db51ca0
--- /dev/null
+++ b/tests/value/oracle_gauges/unroll.res.oracle
@@ -0,0 +1,9 @@
+13,14d12
+< [eva:alarm] tests/value/unroll.i:34: Warning:
+< signed overflow. assert -2147483648 ≤ j - 1;
+16a15
+> [eva] tests/value/unroll.i:39: starting to merge loop iterations
+26c25
+< j ∈ [-2147483648..-123]
+---
+> j ∈ {-238}
diff --git a/tests/value/oracle_gauges/unroll_simple.res.oracle b/tests/value/oracle_gauges/unroll_simple.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d9b0a864fe0371b8a883a85446d84ef7b97c7ad4
--- /dev/null
+++ b/tests/value/oracle_gauges/unroll_simple.res.oracle
@@ -0,0 +1,9 @@
+8,9d7
+< [eva:alarm] tests/value/unroll_simple.i:11: Warning:
+< signed overflow. assert -2147483648 ≤ j - 1;
+11a10
+> [eva] tests/value/unroll_simple.i:16: starting to merge loop iterations
+21c20
+< j ∈ [-2147483648..-126]
+---
+> j ∈ {-250}
diff --git a/tests/value/oracle_gauges/unsigned_overflow.res.oracle b/tests/value/oracle_gauges/unsigned_overflow.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/use_spec.0.res.oracle b/tests/value/oracle_gauges/use_spec.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/use_spec.1.res.oracle b/tests/value/oracle_gauges/use_spec.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/user_assertion_uninit_var.res.oracle b/tests/value/oracle_gauges/user_assertion_uninit_var.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/usp.res.oracle b/tests/value/oracle_gauges/usp.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/va_list.0.res.oracle b/tests/value/oracle_gauges/va_list.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/va_list.1.res.oracle b/tests/value/oracle_gauges/va_list.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/va_list2.0.res.oracle b/tests/value/oracle_gauges/va_list2.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..8149f19c0d3eb1c14afbece52086636c015c3f3d
--- /dev/null
+++ b/tests/value/oracle_gauges/va_list2.0.res.oracle
@@ -0,0 +1,13 @@
+50a51,62
+> [eva] tests/value/va_list2.c:16:
+> Frama_C_show_each_i:
+> {{ garbled mix of &{S_0_S___va_params; S_1_S___va_params} (origin: Well) }}
+> [eva] tests/value/va_list2.c:21:
+> Frama_C_show_each_f:
+> {{ garbled mix of &{S_0_S___va_params; S_1_S___va_params} (origin: Well) }}
+> [eva] tests/value/va_list2.c:16:
+> Frama_C_show_each_i:
+> {{ garbled mix of &{S_0_S___va_params; S_1_S___va_params} (origin: Well) }}
+> [eva] tests/value/va_list2.c:21:
+> Frama_C_show_each_f:
+> {{ garbled mix of &{S_0_S___va_params; S_1_S___va_params} (origin: Well) }}
diff --git a/tests/value/oracle_gauges/va_list2.1.res.oracle b/tests/value/oracle_gauges/va_list2.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6af1df391437f951baaad48f4a545991f74459f3
--- /dev/null
+++ b/tests/value/oracle_gauges/va_list2.1.res.oracle
@@ -0,0 +1,13 @@
+40a41,52
+> [eva] computing for function __builtin_va_arg <- main.
+> Called from tests/value/va_list2.c:15.
+> [eva] Done for function __builtin_va_arg
+> [eva] computing for function __builtin_va_arg <- main.
+> Called from tests/value/va_list2.c:20.
+> [eva] Done for function __builtin_va_arg
+> [eva] computing for function __builtin_va_arg <- main.
+> Called from tests/value/va_list2.c:15.
+> [eva] Done for function __builtin_va_arg
+> [eva] computing for function __builtin_va_arg <- main.
+> Called from tests/value/va_list2.c:20.
+> [eva] Done for function __builtin_va_arg
diff --git a/tests/value/oracle_gauges/val6.0.res.oracle b/tests/value/oracle_gauges/val6.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/val6.1.res.oracle b/tests/value/oracle_gauges/val6.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/val_if.0.res.oracle b/tests/value/oracle_gauges/val_if.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/val_if.1.res.oracle b/tests/value/oracle_gauges/val_if.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/val_if.2.res.oracle b/tests/value/oracle_gauges/val_if.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/val_ptr.0.res.oracle b/tests/value/oracle_gauges/val_ptr.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/val_ptr.1.res.oracle b/tests/value/oracle_gauges/val_ptr.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/val_ptr.2.res.oracle b/tests/value/oracle_gauges/val_ptr.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/val_ptr.3.res.oracle b/tests/value/oracle_gauges/val_ptr.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/video_detect.res.oracle b/tests/value/oracle_gauges/video_detect.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/volatile.res.oracle b/tests/value/oracle_gauges/volatile.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/volatile2.res.oracle b/tests/value/oracle_gauges/volatile2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/volatilestruct.res.oracle b/tests/value/oracle_gauges/volatilestruct.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/wide_string.res.oracle b/tests/value/oracle_gauges/wide_string.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/widen_non_constant.res.oracle b/tests/value/oracle_gauges/widen_non_constant.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/widen_on_non_monotonic.res.oracle b/tests/value/oracle_gauges/widen_on_non_monotonic.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..8d1b8fdc0935530652c731a1e86b7bc40e4884c3
--- /dev/null
+++ b/tests/value/oracle_gauges/widen_on_non_monotonic.res.oracle
@@ -0,0 +1,3 @@
+25a26,27
+> [eva] tests/value/widen_on_non_monotonic.i:21: starting to merge loop iterations
+> [eva] tests/value/widen_on_non_monotonic.i:18: starting to merge loop iterations
diff --git a/tests/value/oracle_gauges/widen_overflow.res.oracle b/tests/value/oracle_gauges/widen_overflow.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3007b00b6bebdd84917aba46654bb185b25a99af
--- /dev/null
+++ b/tests/value/oracle_gauges/widen_overflow.res.oracle
@@ -0,0 +1,4 @@
+31a32,34
+> [eva] computing for function u <- main.
+> Called from tests/value/widen_overflow.i:9.
+> [eva] Done for function u
diff --git a/tests/value/oracle_gauges/widening_thresholds.res.oracle b/tests/value/oracle_gauges/widening_thresholds.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/with_comment.res.oracle b/tests/value/oracle_gauges/with_comment.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/value/oracle_gauges/zerolengtharrays.res.oracle b/tests/value/oracle_gauges/zerolengtharrays.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391