diff --git a/tests/builtins/diff_apron b/tests/builtins/diff_apron
index dcf5e4255bdb8dd1aaa4eadbfa4ce2936022f01c..138fb410e262c773d22565a154e37ee6eab65e31 100644
--- a/tests/builtins/diff_apron
+++ b/tests/builtins/diff_apron
@@ -1,5 +1,5 @@
diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_apron/Longinit_sequencer.res.oracle
-62,65c62,81
+59,62c59,78
< [eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze
< [eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze
< [eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze
@@ -25,7 +25,7 @@ diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_a
> Called from tests/builtins/long_init.c:29.
> [eva] Recording results for subanalyze
> [eva] Done for function subanalyze
-153,154c169,216
+148,149c164,211
< [eva] tests/builtins/long_init.c:93: Reusing old results for call to analyze
< [eva] tests/builtins/long_init.c:94: Reusing old results for call to analyze
---
@@ -77,11 +77,11 @@ diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_a
> [eva] Done for function subanalyze
> [eva] Recording results for analyze
> [eva] Done for function analyze
-327c389
+320c382
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_apron/Longinit_sequencer.sav
-421,424c483,498
+411,414c473,488
< [eva] tests/builtins/long_init2.c:29: Reusing old results for call to subanalyze
< [eva] tests/builtins/long_init2.c:29: Reusing old results for call to subanalyze
< [eva] tests/builtins/long_init2.c:29: Reusing old results for call to subanalyze
@@ -103,11 +103,11 @@ diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_a
> Called from tests/builtins/long_init2.c:29.
> [eva] Recording results for subanalyze
> [eva] Done for function subanalyze
-568c642
+556c630
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_apron/Longinit_sequencer.sav
-658,661c732,747
+643,646c717,732
< [eva] tests/builtins/long_init3.c:29: Reusing old results for call to subanalyze
< [eva] tests/builtins/long_init3.c:29: Reusing old results for call to subanalyze
< [eva] tests/builtins/long_init3.c:29: Reusing old results for call to subanalyze
diff --git a/tests/builtins/diff_bitwise b/tests/builtins/diff_bitwise
index 3fcbca6757345103c83d94f888ffb987b29a2bd7..e2e2efc04cf4b7157d7d1d23eed26b1e58c1983f 100644
--- a/tests/builtins/diff_bitwise
+++ b/tests/builtins/diff_bitwise
@@ -1,9 +1,9 @@
diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_bitwise/Longinit_sequencer.res.oracle
-327c327
+320c320
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_bitwise/Longinit_sequencer.sav
-568c568
+556c556
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_bitwise/Longinit_sequencer.sav
@@ -13,56 +13,47 @@ diff tests/builtins/oracle/allocated.0.res.oracle tests/builtins/oracle_bitwise/
> [eva:malloc] tests/builtins/allocated.c:127:
> resizing variable `__malloc_main_l127' (0..31/319) to fit 0..63/319
diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/allocated.1.res.oracle
-191a192,194
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+171a172,173
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_7
-208a212,214
+188a191,193
> strong free on bases: {__malloc_main_l82_7}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
-223a230,232
+203a209,211
> strong free on bases: {__malloc_main_l82_7}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
-238a248,250
+218a227,229
> strong free on bases: {__malloc_main_l82_7}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
-252,254c264,266
-< [eva] tests/builtins/allocated.c:82:
-< Call to builtin Frama_C_malloc_fresh for function malloc
+232,233c243,245
+< [eva] tests/builtins/allocated.c:82: Call to builtin malloc
< [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_7
---
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_7}
-323a336,356
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+279a292,305
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_31
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_32
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_33
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_34
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_35
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_36
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_37
-329,330d361
+285,286d310
< Trace partitioning superposing up to 300 states
< [eva] tests/builtins/allocated.c:84:
-333a365,385
+289a314,334
> strong free on bases: {__malloc_main_l82_37}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
@@ -84,7 +75,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/
> strong free on bases: {__malloc_main_l82_31}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
-403c455,473
+359c404,422
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -106,7 +97,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-475c545,563
+431c494,512
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -128,7 +119,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-547c635,653
+503c584,602
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -150,7 +141,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-619c725,743
+575c674,692
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -172,7 +163,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-691c815,833
+647c764,782
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -194,7 +185,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-763c905,923
+719c854,872
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -216,7 +207,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-835c995,1013
+791c944,962
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -238,21 +229,21 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-905,907c1083,1084
+861,863c1032,1033
< [eva] tests/builtins/allocated.c:87: Call to builtin free
< [eva:malloc] tests/builtins/allocated.c:87:
< strong free on bases: {__malloc_main_l82_7}
---
> [eva] tests/builtins/allocated.c:81:
> Trace partitioning superposing up to 500 states
-1069,1071c1246,1247
+1001,1003c1171,1172
< __malloc_main_l82_7[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
---
> __malloc_main_l82_7[0] ∈ {14} or UNINITIALIZED
> [1] ∈ {17} or UNINITIALIZED
-1140a1317,1337
+1072a1242,1262
> __malloc_main_l82_31[0] ∈ {21} or UNINITIALIZED
> [1] ∈ {24} or UNINITIALIZED
> [2] ∈ {27} or UNINITIALIZED
@@ -274,11 +265,11 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/
> __malloc_main_l82_37[0] ∈ {21} or UNINITIALIZED
> [1] ∈ {24} or UNINITIALIZED
> [2] ∈ {27} or UNINITIALIZED
-1184c1381
+1116c1306
< __malloc_main_l82_7[0..2] FROM __fc_heap_status; nondet (and SELF)
---
> __malloc_main_l82_7[0..1] FROM __fc_heap_status; nondet (and SELF)
-1207a1405,1411
+1139a1330,1336
> __malloc_main_l82_31[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_32[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_33[0..2] FROM __fc_heap_status; nondet (and SELF)
@@ -286,11 +277,11 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_bitwise/
> __malloc_main_l82_35[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_36[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_37[0..2] FROM __fc_heap_status; nondet (and SELF)
-1231c1435
+1163c1360
< __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..2];
---
> __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..1];
-1243,1244c1447,1452
+1175,1176c1372,1377
< __malloc_main_l82_30[0..2]; __malloc_main_l97[0]; __malloc_main_l114[0..3];
< __malloc_main_l127; __malloc_main_l127_0[0..1]; __malloc_main_l127_1[0..2];
---
diff --git a/tests/builtins/diff_equalities b/tests/builtins/diff_equalities
index 3eceeaa016d96deff8eb5bd8b3c5049b104e7c3b..3956b94f2499324860cf5298288352ab3e415043 100644
--- a/tests/builtins/diff_equalities
+++ b/tests/builtins/diff_equalities
@@ -1,9 +1,9 @@
diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_equalities/Longinit_sequencer.res.oracle
-327c327
+320c320
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_equalities/Longinit_sequencer.sav
-568c568
+556c556
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_equalities/Longinit_sequencer.sav
@@ -11,61 +11,52 @@ diff tests/builtins/oracle/alloc_weak.res.oracle tests/builtins/oracle_equalitie
36,37d35
< [eva:alarm] tests/builtins/alloc_weak.c:30: Warning:
< accessing uninitialized left-value. assert \initialized(p);
-908c906
+912c910
< r ∈ [--..--]
---
> r ∈ {42}
diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equalities/allocated.1.res.oracle
-191a192,194
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+171a172,173
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_7
-208a212,214
+188a191,193
> strong free on bases: {__malloc_main_l82_7}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
-223a230,232
+203a209,211
> strong free on bases: {__malloc_main_l82_7}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
-238a248,250
+218a227,229
> strong free on bases: {__malloc_main_l82_7}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
-252,254c264,266
-< [eva] tests/builtins/allocated.c:82:
-< Call to builtin Frama_C_malloc_fresh for function malloc
+232,233c243,245
+< [eva] tests/builtins/allocated.c:82: Call to builtin malloc
< [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_7
---
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_7}
-323a336,356
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+279a292,305
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_31
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_32
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_33
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_34
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_35
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_36
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_37
-329,330d361
+285,286d310
< Trace partitioning superposing up to 300 states
< [eva] tests/builtins/allocated.c:84:
-333a365,385
+289a314,334
> strong free on bases: {__malloc_main_l82_37}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
@@ -87,7 +78,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> strong free on bases: {__malloc_main_l82_31}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
-403c455,473
+359c404,422
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -109,7 +100,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-475c545,563
+431c494,512
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -131,7 +122,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-547c635,653
+503c584,602
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -153,7 +144,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-619c725,743
+575c674,692
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -175,7 +166,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-691c815,833
+647c764,782
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -197,7 +188,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-763c905,923
+719c854,872
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -219,7 +210,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-835c995,1013
+791c944,962
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -241,21 +232,21 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-905,907c1083,1084
+861,863c1032,1033
< [eva] tests/builtins/allocated.c:87: Call to builtin free
< [eva:malloc] tests/builtins/allocated.c:87:
< strong free on bases: {__malloc_main_l82_7}
---
> [eva] tests/builtins/allocated.c:81:
> Trace partitioning superposing up to 500 states
-1069,1071c1246,1247
+1001,1003c1171,1172
< __malloc_main_l82_7[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
---
> __malloc_main_l82_7[0] ∈ {14} or UNINITIALIZED
> [1] ∈ {17} or UNINITIALIZED
-1140a1317,1337
+1072a1242,1262
> __malloc_main_l82_31[0] ∈ {21} or UNINITIALIZED
> [1] ∈ {24} or UNINITIALIZED
> [2] ∈ {27} or UNINITIALIZED
@@ -277,11 +268,11 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> __malloc_main_l82_37[0] ∈ {21} or UNINITIALIZED
> [1] ∈ {24} or UNINITIALIZED
> [2] ∈ {27} or UNINITIALIZED
-1184c1381
+1116c1306
< __malloc_main_l82_7[0..2] FROM __fc_heap_status; nondet (and SELF)
---
> __malloc_main_l82_7[0..1] FROM __fc_heap_status; nondet (and SELF)
-1207a1405,1411
+1139a1330,1336
> __malloc_main_l82_31[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_32[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_33[0..2] FROM __fc_heap_status; nondet (and SELF)
@@ -289,11 +280,11 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> __malloc_main_l82_35[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_36[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_37[0..2] FROM __fc_heap_status; nondet (and SELF)
-1231c1435
+1163c1360
< __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..2];
---
> __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..1];
-1243,1244c1447,1452
+1175,1176c1372,1377
< __malloc_main_l82_30[0..2]; __malloc_main_l97[0]; __malloc_main_l114[0..3];
< __malloc_main_l127; __malloc_main_l127_0[0..1]; __malloc_main_l127_1[0..2];
---
@@ -304,16 +295,16 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> __malloc_main_l97[0]; __malloc_main_l114[0..3]; __malloc_main_l127;
> __malloc_main_l127_0[0..1]; __malloc_main_l127_1[0..2];
diff tests/builtins/oracle/imprecise.res.oracle tests/builtins/oracle_equalities/imprecise.res.oracle
-100a101,102
+104a105,106
> [kernel] tests/builtins/imprecise.c:51:
> imprecise size for variable v3 (abstract type 'struct u')
-224a227,228
+229a232,233
> [kernel] tests/builtins/imprecise.c:111:
> more than 200(300) elements to enumerate. Approximating.
-233a238,239
+238a243,244
> [kernel] tests/builtins/imprecise.c:114:
> more than 200(300) elements to enumerate. Approximating.
-237,240d242
+242,245d247
< [kernel] tests/builtins/imprecise.c:111:
< more than 200(300) elements to enumerate. Approximating.
< [kernel] tests/builtins/imprecise.c:114:
diff --git a/tests/builtins/diff_gauges b/tests/builtins/diff_gauges
index 6d0296afea2fcbc809f18fae19d5d1b535fb2142..ca4a1580fa4e366cd777744846c0120ddd2509ba 100644
--- a/tests/builtins/diff_gauges
+++ b/tests/builtins/diff_gauges
@@ -1,9 +1,9 @@
diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_gauges/Longinit_sequencer.res.oracle
-327c327
+320c320
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_gauges/Longinit_sequencer.sav
-568c568
+556c556
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_gauges/Longinit_sequencer.sav
@@ -36,13 +36,13 @@ diff tests/builtins/oracle/malloc-size-zero.1.res.oracle tests/builtins/oracle_g
> [eva] Recording results for my_calloc
> [eva] Done for function my_calloc
diff tests/builtins/oracle/memcpy.res.oracle tests/builtins/oracle_gauges/memcpy.res.oracle
-168a169,170
+176a177,178
> [eva] tests/builtins/memcpy.c:96: Call to builtin memcpy
> [eva] tests/builtins/memcpy.c:96: Call to builtin memcpy
-449a452
+457a460
> [eva] tests/builtins/memcpy.c:230: starting to merge loop iterations
diff tests/builtins/oracle/realloc.res.oracle tests/builtins/oracle_gauges/realloc.res.oracle
-689a690,1038
+677a678,1026
> [eva] tests/builtins/realloc.c:152: Call to builtin realloc
> [eva:malloc] bases_to_realloc: {__realloc_w_main10_l152}
> [eva:malloc] tests/builtins/realloc.c:152:
diff --git a/tests/builtins/diff_octagons b/tests/builtins/diff_octagons
index d189dffda23b163cb80c265740715e1c91c72f17..c2b18889ac58a637ec38f7f04c918867bbe336b8 100644
--- a/tests/builtins/diff_octagons
+++ b/tests/builtins/diff_octagons
@@ -1,9 +1,9 @@
diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_octagons/Longinit_sequencer.res.oracle
-327c327
+320c320
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_octagons/Longinit_sequencer.sav
-568c568
+556c556
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_octagons/Longinit_sequencer.sav
@@ -13,56 +13,47 @@ diff tests/builtins/oracle/allocated.0.res.oracle tests/builtins/oracle_octagons
---
> j ∈ {10}
diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_octagons/allocated.1.res.oracle
-191a192,194
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+171a172,173
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_7
-208a212,214
+188a191,193
> strong free on bases: {__malloc_main_l82_7}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
-223a230,232
+203a209,211
> strong free on bases: {__malloc_main_l82_7}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
-238a248,250
+218a227,229
> strong free on bases: {__malloc_main_l82_7}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
-252,254c264,266
-< [eva] tests/builtins/allocated.c:82:
-< Call to builtin Frama_C_malloc_fresh for function malloc
+232,233c243,245
+< [eva] tests/builtins/allocated.c:82: Call to builtin malloc
< [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_7
---
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_7}
-323a336,356
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+279a292,305
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_31
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_32
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_33
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_34
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_35
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_36
-> [eva] tests/builtins/allocated.c:82:
-> Call to builtin Frama_C_malloc_fresh for function malloc
+> [eva] tests/builtins/allocated.c:82: Call to builtin malloc
> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_37
-329,330d361
+285,286d310
< Trace partitioning superposing up to 300 states
< [eva] tests/builtins/allocated.c:84:
-333a365,385
+289a314,334
> strong free on bases: {__malloc_main_l82_37}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
@@ -84,7 +75,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_octagons
> strong free on bases: {__malloc_main_l82_31}
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
-403c455,473
+359c404,422
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -106,7 +97,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_octagons
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-475c545,563
+431c494,512
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -128,7 +119,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_octagons
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-547c635,653
+503c584,602
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -150,7 +141,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_octagons
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-619c725,743
+575c674,692
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -172,7 +163,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_octagons
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-691c815,833
+647c764,782
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -194,7 +185,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_octagons
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-763c905,923
+719c854,872
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -216,7 +207,7 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_octagons
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-835c995,1013
+791c944,962
< strong free on bases: {__malloc_main_l82_7}
---
> strong free on bases: {__malloc_main_l82_37}
@@ -238,21 +229,21 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_octagons
> [eva] tests/builtins/allocated.c:87: Call to builtin free
> [eva:malloc] tests/builtins/allocated.c:87:
> strong free on bases: {__malloc_main_l82_31}
-905,907c1083,1084
+861,863c1032,1033
< [eva] tests/builtins/allocated.c:87: Call to builtin free
< [eva:malloc] tests/builtins/allocated.c:87:
< strong free on bases: {__malloc_main_l82_7}
---
> [eva] tests/builtins/allocated.c:81:
> Trace partitioning superposing up to 500 states
-1069,1071c1246,1247
+1001,1003c1171,1172
< __malloc_main_l82_7[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
---
> __malloc_main_l82_7[0] ∈ {14} or UNINITIALIZED
> [1] ∈ {17} or UNINITIALIZED
-1140a1317,1337
+1072a1242,1262
> __malloc_main_l82_31[0] ∈ {21} or UNINITIALIZED
> [1] ∈ {24} or UNINITIALIZED
> [2] ∈ {27} or UNINITIALIZED
@@ -274,11 +265,11 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_octagons
> __malloc_main_l82_37[0] ∈ {21} or UNINITIALIZED
> [1] ∈ {24} or UNINITIALIZED
> [2] ∈ {27} or UNINITIALIZED
-1184c1381
+1116c1306
< __malloc_main_l82_7[0..2] FROM __fc_heap_status; nondet (and SELF)
---
> __malloc_main_l82_7[0..1] FROM __fc_heap_status; nondet (and SELF)
-1207a1405,1411
+1139a1330,1336
> __malloc_main_l82_31[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_32[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_33[0..2] FROM __fc_heap_status; nondet (and SELF)
@@ -286,11 +277,11 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_octagons
> __malloc_main_l82_35[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_36[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_37[0..2] FROM __fc_heap_status; nondet (and SELF)
-1231c1435
+1163c1360
< __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..2];
---
> __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..1];
-1243,1244c1447,1452
+1175,1176c1372,1377
< __malloc_main_l82_30[0..2]; __malloc_main_l97[0]; __malloc_main_l114[0..3];
< __malloc_main_l127; __malloc_main_l127_0[0..1]; __malloc_main_l127_1[0..2];
---
@@ -301,13 +292,13 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_octagons
> __malloc_main_l97[0]; __malloc_main_l114[0..3]; __malloc_main_l127;
> __malloc_main_l127_0[0..1]; __malloc_main_l127_1[0..2];
diff tests/builtins/oracle/imprecise.res.oracle tests/builtins/oracle_octagons/imprecise.res.oracle
-224a225,226
+229a230,231
> [kernel] tests/builtins/imprecise.c:111:
> more than 200(300) elements to enumerate. Approximating.
-233a236,237
+238a241,242
> [kernel] tests/builtins/imprecise.c:114:
> more than 200(300) elements to enumerate. Approximating.
-237,240d240
+242,245d245
< [kernel] tests/builtins/imprecise.c:111:
< more than 200(300) elements to enumerate. Approximating.
< [kernel] tests/builtins/imprecise.c:114:
diff --git a/tests/builtins/diff_symblocs b/tests/builtins/diff_symblocs
index 985f1aa7459c12885973d39126f6c3d930ec7a52..f640a0f73229eb6388e8c2b9526126abe4f4eeaa 100644
--- a/tests/builtins/diff_symblocs
+++ b/tests/builtins/diff_symblocs
@@ -1,9 +1,9 @@
diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_symblocs/Longinit_sequencer.res.oracle
-327c327
+320c320
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_symblocs/Longinit_sequencer.sav
-568c568
+556c556
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_symblocs/Longinit_sequencer.sav
@@ -11,18 +11,18 @@ diff tests/builtins/oracle/alloc_weak.res.oracle tests/builtins/oracle_symblocs/
36,37d35
< [eva:alarm] tests/builtins/alloc_weak.c:30: Warning:
< accessing uninitialized left-value. assert \initialized(p);
-908c906
+912c910
< r ∈ [--..--]
---
> r ∈ {42}
diff tests/builtins/oracle/imprecise.res.oracle tests/builtins/oracle_symblocs/imprecise.res.oracle
-224a225,226
+229a230,231
> [kernel] tests/builtins/imprecise.c:111:
> more than 200(300) elements to enumerate. Approximating.
-233a236,237
+238a241,242
> [kernel] tests/builtins/imprecise.c:114:
> more than 200(300) elements to enumerate. Approximating.
-237,240d240
+242,245d245
< [kernel] tests/builtins/imprecise.c:111:
< more than 200(300) elements to enumerate. Approximating.
< [kernel] tests/builtins/imprecise.c:114:
diff --git a/tests/float/diff_equalities b/tests/float/diff_equalities
index 2b65e74c9227a91b9a0bbb7b0ab5e13dc4861fca..bf39814c4b96d859cb091c9b348f53ca943cf92b 100644
--- a/tests/float/diff_equalities
+++ b/tests/float/diff_equalities
@@ -4,7 +4,7 @@ Only in tests/float/oracle: absorb_sav.res
Only in tests/float/oracle: absorb_sav2.err
Only in tests/float/oracle: absorb_sav2.res
diff tests/float/oracle/alarms.0.res.oracle tests/float/oracle_equalities/alarms.0.res.oracle
-137,139c137,138
+141,143c141,142
< u1{.l[bits 0 to 31]; .f; .d[bits 0 to 31]} ∈
< [-3.40282346639e+38 .. 3.40282346639e+38]
< {.l[bits 32 to 63]; .f[bits 32 to 63]; .d[bits 32 to 63]} ∈ [--..--]
@@ -39,6 +39,6 @@ diff tests/float/oracle/nonlin.5.res.oracle tests/float/oracle_equalities/nonlin
61a62
> [eva:nonlin] tests/float/nonlin.c:44: subdividing on a
diff tests/float/oracle/parse.res.oracle tests/float/oracle_equalities/parse.res.oracle
-21a22,23
+22a23,24
> [eva] tests/float/parse.i:37: Warning:
> cannot parse floating-point constant, returning imprecise result
diff --git a/tests/float/diff_octagons b/tests/float/diff_octagons
index 532ecb44df5be4239c1bb13a6996f93fe0487731..c37678723890d07cf9737efd397500e8c12efee2 100644
--- a/tests/float/diff_octagons
+++ b/tests/float/diff_octagons
@@ -5,26 +5,26 @@ Only in tests/float/oracle: absorb_sav2.err
Only in tests/float/oracle: absorb_sav2.res
Only in tests/float/oracle: fval_test.res.oracle
diff tests/float/oracle/nonlin.1.res.oracle tests/float/oracle_octagons/nonlin.1.res.oracle
-279a280,281
+283a284,285
> [eva:nonlin] tests/float/nonlin.c:113: non-linear 'f + f', lv 'f'
> [eva:nonlin] tests/float/nonlin.c:113: subdividing on f
-283d284
+287d288
< [eva:nonlin] tests/float/nonlin.c:113: subdividing on f
diff tests/float/oracle/nonlin.2.res.oracle tests/float/oracle_octagons/nonlin.2.res.oracle
-259a260,261
+263a264,265
> [eva:nonlin] tests/float/nonlin.c:113: non-linear 'f + f', lv 'f'
> [eva:nonlin] tests/float/nonlin.c:113: subdividing on f
-263d264
+267d268
< [eva:nonlin] tests/float/nonlin.c:113: subdividing on f
diff tests/float/oracle/nonlin.4.res.oracle tests/float/oracle_octagons/nonlin.4.res.oracle
-279a280,281
+283a284,285
> [eva:nonlin] tests/float/nonlin.c:113: non-linear 'f + f', lv 'f'
> [eva:nonlin] tests/float/nonlin.c:113: subdividing on f
-283d284
+287d288
< [eva:nonlin] tests/float/nonlin.c:113: subdividing on f
diff tests/float/oracle/nonlin.5.res.oracle tests/float/oracle_octagons/nonlin.5.res.oracle
-259a260,261
+263a264,265
> [eva:nonlin] tests/float/nonlin.c:113: non-linear 'f + f', lv 'f'
> [eva:nonlin] tests/float/nonlin.c:113: subdividing on f
-263d264
+267d268
< [eva:nonlin] tests/float/nonlin.c:113: subdividing on f
diff --git a/tests/value/diff_apron b/tests/value/diff_apron
index acd1edcccf94742f47764a074ccbf93bc71fce24..2ba17244e29404e5b12a718153ff2bc88c017c05 100644
--- a/tests/value/diff_apron
+++ b/tests/value/diff_apron
@@ -501,7 +501,15 @@ diff tests/value/oracle/divneg.res.oracle tests/value/oracle_apron/divneg.res.or
< vic ∈ {4294967295}
---
> vic ∈ {-1}
-diff tests/value/oracle/downcast.res.oracle tests/value/oracle_apron/downcast.res.oracle
+diff tests/value/oracle/domains_function.res.oracle tests/value/oracle_apron/domains_function.res.oracle
+107c107,110
+< [eva] tests/value/domains_function.c:63: Reusing old results for call to use
+---
+> [eva] computing for function use <- test_propagation <- main.
+> Called from tests/value/domains_function.c:63.
+> [eva] Recording results for use
+> [eva] Done for function use
+diff tests/value/oracle/downcast.1.res.oracle tests/value/oracle_apron/downcast.1.res.oracle
61c61
< [100000..2147483647], [100145..2147483647], [100145..2147483647]
---
@@ -615,7 +623,7 @@ diff tests/value/oracle/fptr.1.res.oracle tests/value/oracle_apron/fptr.1.res.or
> [eva] Recording results for f
> [eva] Done for function f
diff tests/value/oracle/from_call.0.res.oracle tests/value/oracle_apron/from_call.0.res.oracle
-64c64,69
+68c68,73
< [eva] tests/value/from_call.i:20: Reusing old results for call to g
---
> [eva] computing for function g <- f <- main.
@@ -624,7 +632,7 @@ diff tests/value/oracle/from_call.0.res.oracle tests/value/oracle_apron/from_cal
> [from] Computing for function g
> [from] Done for function g
> [eva] Done for function g
-74c79,84
+78c83,88
< [eva] tests/value/from_call.i:20: Reusing old results for call to g
---
> [eva] computing for function g <- f <- main.
@@ -633,7 +641,7 @@ diff tests/value/oracle/from_call.0.res.oracle tests/value/oracle_apron/from_cal
> [from] Computing for function g
> [from] Done for function g
> [eva] Done for function g
-145,146c155,166
+149,150c159,170
< [eva] tests/value/from_call.i:44: Reusing old results for call to return_A1
< [eva] tests/value/from_call.i:44: Reusing old results for call to return_A2
---
@@ -650,21 +658,21 @@ diff tests/value/oracle/from_call.0.res.oracle tests/value/oracle_apron/from_cal
> [from] Done for function return_A2
> [eva] Done for function return_A2
diff tests/value/oracle/from_call.1.res.oracle tests/value/oracle_apron/from_call.1.res.oracle
-60c60,63
+64c64,67
< [eva] tests/value/from_call.i:20: Reusing old results for call to g
---
> [eva] computing for function g <- f <- main.
> Called from tests/value/from_call.i:20.
> [eva] Recording results for g
> [eva] Done for function g
-68c71,74
+72c75,78
< [eva] tests/value/from_call.i:20: Reusing old results for call to g
---
> [eva] computing for function g <- f <- main.
> Called from tests/value/from_call.i:20.
> [eva] Recording results for g
> [eva] Done for function g
-119,120c125,132
+123,124c129,136
< [eva] tests/value/from_call.i:44: Reusing old results for call to return_A1
< [eva] tests/value/from_call.i:44: Reusing old results for call to return_A2
---
@@ -685,7 +693,7 @@ diff tests/value/oracle/fun_ptr.0.res.oracle tests/value/oracle_apron/fun_ptr.0.
> [eva] Recording results for f
> [eva] Done for function f
diff tests/value/oracle/fun_ptr.1.res.oracle tests/value/oracle_apron/fun_ptr.1.res.oracle
-39c39,42
+43c43,46
< [eva] tests/value/fun_ptr.i:33: Reusing old results for call to f
---
> [eva] computing for function f <- test2 <- main.
@@ -720,53 +728,53 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_apron/gauges.res.or
187,188d180
< [eva:alarm] tests/value/gauges.c:140: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
-299,300d290
+303,304d294
< [eva:alarm] tests/value/gauges.c:220: Warning:
< signed overflow. assert -2147483648 ≤ n - 1;
-315,316d304
+319,320d308
< [eva:alarm] tests/value/gauges.c:240: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
-318c306
+322c310
< Frama_C_show_each: {45; 46; 47; 48; 49; 50; 51}, [0..2147483647]
---
> Frama_C_show_each: {45; 46; 47; 48; 49; 50; 51}, [0..46]
-324,325d311
+328,329d315
< [eva:alarm] tests/value/gauges.c:251: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
-327c313
+331c317
< Frama_C_show_each: {48; 49; 50; 51; 52; 53; 54}, [0..2147483647]
---
> Frama_C_show_each: {48; 49; 50; 51; 52; 53; 54}, [0..49]
-333,334d318
+337,338d322
< [eva:alarm] tests/value/gauges.c:263: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
-336c320
+340c324
< Frama_C_show_each: {-59; -58; -57; -56; -55; -54; -53}, [0..2147483647]
---
> Frama_C_show_each: {-59; -58; -57; -56; -55; -54; -53}, [0..65]
-342,343d325
+346,347d329
< [eva:alarm] tests/value/gauges.c:274: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
-345c327
+349c331
< Frama_C_show_each: {-64; -63; -62; -61; -60; -59; -58}, [0..2147483647]
---
> Frama_C_show_each: {-64; -63; -62; -61; -60; -59; -58}, [0..70]
-353,354d334
+357,358d338
< [eva:alarm] tests/value/gauges.c:293: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
-356c336
+360c340
< Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..2147483647]
---
> Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..598]
-798c778
+802c782
< n ∈ [-2147483648..99]
---
> n ∈ [-2147483547..99]
-801c781
+805c785
< i ∈ [0..2147483647]
---
> i ∈ [10..2147483647]
-837c817
+841c821
< i ∈ [0..2147483647]
---
> i ∈ [0..21]
@@ -978,7 +986,7 @@ diff tests/value/oracle/loopinv.res.oracle tests/value/oracle_apron/loopinv.res.
> 3 To be validated
> 12 Total
diff tests/value/oracle/memexec.res.oracle tests/value/oracle_apron/memexec.res.oracle
-25,30c25,48
+27,32c27,50
< [eva] tests/value/memexec.c:13: Reusing old results for call to f11
< [eva] tests/value/memexec.c:14: Reusing old results for call to f11
< [eva] tests/value/memexec.c:16: Reusing old results for call to f11
@@ -1010,40 +1018,27 @@ diff tests/value/oracle/memexec.res.oracle tests/value/oracle_apron/memexec.res.
> Called from tests/value/memexec.c:21.
> [eva] Recording results for f11
> [eva] Done for function f11
-104c122,125
+106c124,127
< [eva] tests/value/memexec.c:113: Reusing old results for call to f5_aux
---
> [eva] computing for function f5_aux <- f5 <- main.
> Called from tests/value/memexec.c:113.
> [eva] Recording results for f5_aux
> [eva] Done for function f5_aux
-106,107c127
-< Frama_C_show_each_f5:
-< [9..2147483647], [-2147483648..2147483647], [-2147483648..7]
----
-> Frama_C_show_each_f5: [9..2147483647], [-2147483648..6], [-2147483648..7]
-128c148,151
+129c150,153
< [eva] tests/value/memexec.c:137: Reusing old results for call to f7_1
---
> [eva] computing for function f7_1 <- f7 <- main.
> Called from tests/value/memexec.c:137.
> [eva] Recording results for f7_1
> [eva] Done for function f7_1
-143c166,169
+144c168,171
< [eva] tests/value/memexec.c:150: Reusing old results for call to f8_1
---
> [eva] computing for function f8_1 <- f8 <- main.
> Called from tests/value/memexec.c:150.
> [eva] Recording results for f8_1
> [eva] Done for function f8_1
-195c221
-< g_f5_1 ∈ [--..--]
----
-> g_f5_1 ∈ [-2147483648..6]
-231c257
-< g_f5_1 ∈ [--..--]
----
-> g_f5_1 ∈ [-2147483648..6]
diff tests/value/oracle/modulo.res.oracle tests/value/oracle_apron/modulo.res.oracle
40a41,64
> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [-9..-1], [-8..0]
@@ -1110,28 +1105,28 @@ diff tests/value/oracle/octagons.res.oracle tests/value/oracle_apron/octagons.re
> c ∈ [-602..1446]
> d ∈ [-611..2147483647]
diff tests/value/oracle/offsetmap.0.res.oracle tests/value/oracle_apron/offsetmap.0.res.oracle
-62,63c62
+64,65c64
< a[bits 0 to 7] ∈ {1; 6}
< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
---
> a ∈ {1; 6}
-65,66c64
+67,68c66
< a7[bits 0 to 7] ∈ {1}
< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
---
> a7 ∈ {1}
-106,107c104
+108,109c106
< a[bits 0 to 7] ∈ {1; 6}
< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
---
> a ∈ {1; 6}
-109,110c106
+111,112c108
< a7[bits 0 to 7] ∈ {1}
< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
---
> a7 ∈ {1}
diff tests/value/oracle/offsetmap.1.res.oracle tests/value/oracle_apron/offsetmap.1.res.oracle
-62,67c62,64
+64,69c64,66
< a[bits 0 to 7] ∈ {1; 6}
< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
< b[bits 0 to 7] ∈ {0; 1}
@@ -1142,7 +1137,7 @@ diff tests/value/oracle/offsetmap.1.res.oracle tests/value/oracle_apron/offsetma
> a ∈ {1; 6}
> b ∈ {0; 1}
> a7 ∈ {1}
-107,112c104,106
+109,114c106,108
< a[bits 0 to 7] ∈ {1; 6}
< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
< b[bits 0 to 7] ∈ {0; 1}
diff --git a/tests/value/diff_bitwise b/tests/value/diff_bitwise
index fbafb12ebb855166d7107c5ac57b6101ed41c0c4..f3d9227dd921eafcae4091aea38d785407838400 100644
--- a/tests/value/diff_bitwise
+++ b/tests/value/diff_bitwise
@@ -1,23 +1,23 @@
diff tests/value/oracle/addition.res.oracle tests/value/oracle_bitwise/addition.res.oracle
-90,92c90
+121,123c121
< [eva] tests/value/addition.i:52:
< Assigning imprecise value to p10.
< The imprecision originates from Arithmetic {tests/value/addition.i:52}
---
> [eva] tests/value/addition.i:52: Assigning imprecise value to p10.
-128a127
+163a162
> {{ garbled mix of &{p1} (origin: Misaligned {tests/value/addition.i:52}) }}
-130a130
+165a165
> {{ garbled mix of &{p2} (origin: Misaligned {tests/value/addition.i:56}) }}
-166,168c166
+201,203c201
< p10 ∈
< {{ garbled mix of &{p1}
< (origin: Arithmetic {tests/value/addition.i:52}) }}
---
> p10 ∈ {{ garbled mix of &{p1} }}
-358a357
+428a427
> {{ garbled mix of &{p1} (origin: Misaligned {tests/value/addition.i:52}) }}
-397,399c396
+467,469c466
< p10 ∈
< {{ garbled mix of &{p1}
< (origin: Arithmetic {tests/value/addition.i:52}) }}
@@ -32,13 +32,13 @@ diff tests/value/oracle/bitwise.res.oracle tests/value/oracle_bitwise/bitwise.re
> led to bottom without alarms:
> at this point the product of states has no possible concretization.
diff tests/value/oracle/bitwise_pointer.res.oracle tests/value/oracle_bitwise/bitwise_pointer.res.oracle
-32,34c32
+34,36c34
< [eva] tests/value/bitwise_pointer.i:18:
< Assigning imprecise value to p.
< The imprecision originates from Arithmetic {tests/value/bitwise_pointer.i:18}
---
> [eva] tests/value/bitwise_pointer.i:18: Assigning imprecise value to p.
-37,39c35
+41,43c39
< [eva] tests/value/bitwise_pointer.i:22:
< Assigning imprecise value to p1.
< The imprecision originates from Arithmetic {tests/value/bitwise_pointer.i:22}
diff --git a/tests/value/diff_equalities b/tests/value/diff_equalities
index ef78d5ee70dc62c1a02d250080350083376ad7a3..4ebaf82ffdec6a7011177a7b539a9e0fb8113c45 100644
--- a/tests/value/diff_equalities
+++ b/tests/value/diff_equalities
@@ -1,24 +1,24 @@
diff tests/value/oracle/CruiseControl.res.oracle tests/value/oracle_equalities/CruiseControl.res.oracle
-978c978
+980c980
< [0]._C4_ThrottleCmd._I0_Regul_ON ∈ {0; 1}
---
> [0]._C4_ThrottleCmd._I0_Regul_ON ∈ {1}
-1016c1016
+1018c1018
< [0]._C4_ThrottleCmd._C0_ThrottleRegulation._C0_SaturateThrottle{._I0_ThrottleIn; ._O0_ThrottleOut} ∈
---
> [0]._C4_ThrottleCmd._C0_ThrottleRegulation._C0_SaturateThrottle._I0_ThrottleIn ∈
-1017a1018,1019
+1019a1020,1021
> [0]._C4_ThrottleCmd._C0_ThrottleRegulation._C0_SaturateThrottle._O0_ThrottleOut ∈
> [-0.0000000000000000 .. 1.9999998807907104*2^127]
-1031c1033
+1033c1035
< [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
---
> [-0.0000000000000000 .. 1.9999998807907104*2^127]
-1216c1218
+1218c1220
< [0]._C4_ThrottleCmd._I0_Regul_ON ∈ {0; 1}
---
> [0]._C4_ThrottleCmd._I0_Regul_ON ∈ {1}
-1228c1230,1234
+1230c1232,1236
< [0]._C4_ThrottleCmd._C0_ThrottleRegulation{._I1_CruiseSpeed; ._I2_VehiculeSpeed; ._O0_Throttle; ._L1_CruiseControl; ._L2_CruiseControl; ._L3_CruiseControl} ∈
---
> [0]._C4_ThrottleCmd._C0_ThrottleRegulation{._I1_CruiseSpeed; ._I2_VehiculeSpeed} ∈
@@ -26,39 +26,43 @@ diff tests/value/oracle/CruiseControl.res.oracle tests/value/oracle_equalities/C
> [0]._C4_ThrottleCmd._C0_ThrottleRegulation._O0_Throttle ∈
> [-0.0000000000000000 .. 1.9999998807907104*2^127]
> [0]._C4_ThrottleCmd._C0_ThrottleRegulation{._L1_CruiseControl; ._L2_CruiseControl; ._L3_CruiseControl} ∈
-1246c1252
+1248c1254
< [0]._C4_ThrottleCmd._C0_ThrottleRegulation{._L4_CruiseControl; ._L13_CruiseControl} ∈
---
> [0]._C4_ThrottleCmd._C0_ThrottleRegulation._L4_CruiseControl ∈
-1247a1254,1255
+1249a1256,1257
> [0]._C4_ThrottleCmd._C0_ThrottleRegulation._L13_CruiseControl ∈
> [-0.0000000000000000 .. 1.9999998807907104*2^127]
-1254c1262
+1256c1264
< [0]._C4_ThrottleCmd._C0_ThrottleRegulation._C0_SaturateThrottle{._I0_ThrottleIn; ._O0_ThrottleOut} ∈
---
> [0]._C4_ThrottleCmd._C0_ThrottleRegulation._C0_SaturateThrottle._I0_ThrottleIn ∈
-1255a1264,1265
+1257a1266,1267
> [0]._C4_ThrottleCmd._C0_ThrottleRegulation._C0_SaturateThrottle._O0_ThrottleOut ∈
> [-0.0000000000000000 .. 1.9999998807907104*2^127]
-1269c1279
+1271c1281
< [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
---
> [-0.0000000000000000 .. 1.9999998807907104*2^127]
diff tests/value/oracle/addition.res.oracle tests/value/oracle_equalities/addition.res.oracle
-103,106d102
+138,141d137
< [eva:alarm] tests/value/addition.i:61: Warning:
< signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
< [eva:alarm] tests/value/addition.i:61: Warning:
< signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
-133d128
-< [scope:rm_asserts] removing 2 assertion(s)
-337,340d331
+168c164
+< [scope:rm_asserts] removing 9 assertion(s)
+---
+> [scope:rm_asserts] removing 7 assertion(s)
+407,410d402
< [eva:alarm] tests/value/addition.i:61: Warning:
< signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
< [eva:alarm] tests/value/addition.i:61: Warning:
< signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
-363d353
-< [scope:rm_asserts] removing 2 assertion(s)
+433c425
+< [scope:rm_asserts] removing 9 assertion(s)
+---
+> [scope:rm_asserts] removing 7 assertion(s)
diff tests/value/oracle/alias.0.res.oracle tests/value/oracle_equalities/alias.0.res.oracle
103,104c103,104
< t ∈ {1; 2; 4}
@@ -249,16 +253,16 @@ diff tests/value/oracle/backward_add_ptr.res.oracle tests/value/oracle_equalitie
> {{ garbled mix of &{b; c}
> (origin: Arithmetic {tests/value/backward_add_ptr.c:178}) }}
diff tests/value/oracle/bitfield.res.oracle tests/value/oracle_equalities/bitfield.res.oracle
-132a133,135
+138a139,141
> [eva] tests/value/bitfield.i:71:
> Frama_C_show_each:
> {{ garbled mix of &{b} (origin: Misaligned {tests/value/bitfield.i:70}) }}
diff tests/value/oracle/bitwise_pointer.res.oracle tests/value/oracle_equalities/bitwise_pointer.res.oracle
-58c58
+62c62
< x ∈ [0..9]
---
> x ∈ {5}
-71c71
+75c75
< x1 ∈ [0..9]
---
> x1 ∈ {5}
@@ -282,12 +286,74 @@ diff tests/value/oracle/descending.res.oracle tests/value/oracle_equalities/desc
< i ∈ {31; 32}
---
> i ∈ {31}
-diff tests/value/oracle/downcast.res.oracle tests/value/oracle_equalities/downcast.res.oracle
-735c735
+diff tests/value/oracle/domains_function.res.oracle tests/value/oracle_equalities/domains_function.res.oracle
+19,20c19
+< [eva] tests/value/domains_function.c:92:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:92: Frama_C_show_each_top: {3}
+28,29c27
+< [eva] tests/value/domains_function.c:77:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:77: Frama_C_show_each_top: {1}
+32,33c30
+< [eva] tests/value/domains_function.c:96:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:96: Frama_C_show_each_top: {1}
+36,37c33
+< [eva] tests/value/domains_function.c:84:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:84: Frama_C_show_each_top: {2}
+40,41c36
+< [eva] tests/value/domains_function.c:98:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:98: Frama_C_show_each_top: {2}
+60,61c55
+< [eva] tests/value/domains_function.c:84:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:84: Frama_C_show_each_top: {2}
+64,65c58
+< [eva] tests/value/domains_function.c:113:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:113: Frama_C_show_each_top: {2}
+78,79c71
+< [eva] tests/value/domains_function.c:55:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:55: Frama_C_show_each_top: {42}
+108,109c100
+< [eva] tests/value/domains_function.c:64:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:64: Frama_C_show_each_top: {42}
+116c107
+< result ∈ [--..--]
+---
+> result ∈ {2}
+130c121
+< result ∈ [--..--]
+---
+> result ∈ {1}
+135c126
+< result ∈ [--..--]
+---
+> result ∈ {2}
+138c129
+< result ∈ [--..--]
+---
+> result ∈ {2}
+diff tests/value/oracle/downcast.2.res.oracle tests/value/oracle_equalities/downcast.2.res.oracle
+114c114
< ux ∈ [--..--]
---
> ux ∈ [0..65535]
-778c778
+157c157
< ux ∈ [--..--]
---
> ux ∈ [0..65535]
@@ -301,7 +367,7 @@ diff tests/value/oracle/fptr.1.res.oracle tests/value/oracle_equalities/fptr.1.r
---
> n ∈ {0; 1}
diff tests/value/oracle/from_call.0.res.oracle tests/value/oracle_equalities/from_call.0.res.oracle
-64c64,69
+68c68,73
< [eva] tests/value/from_call.i:20: Reusing old results for call to g
---
> [eva] computing for function g <- f <- main.
@@ -310,7 +376,7 @@ diff tests/value/oracle/from_call.0.res.oracle tests/value/oracle_equalities/fro
> [from] Computing for function g
> [from] Done for function g
> [eva] Done for function g
-74c79,84
+78c83,88
< [eva] tests/value/from_call.i:20: Reusing old results for call to g
---
> [eva] computing for function g <- f <- main.
@@ -320,14 +386,14 @@ diff tests/value/oracle/from_call.0.res.oracle tests/value/oracle_equalities/fro
> [from] Done for function g
> [eva] Done for function g
diff tests/value/oracle/from_call.1.res.oracle tests/value/oracle_equalities/from_call.1.res.oracle
-60c60,63
+64c64,67
< [eva] tests/value/from_call.i:20: Reusing old results for call to g
---
> [eva] computing for function g <- f <- main.
> Called from tests/value/from_call.i:20.
> [eva] Recording results for g
> [eva] Done for function g
-68c71,74
+72c75,78
< [eva] tests/value/from_call.i:20: Reusing old results for call to g
---
> [eva] computing for function g <- f <- main.
@@ -338,7 +404,7 @@ diff tests/value/oracle/from_termin.res.oracle tests/value/oracle_equalities/fro
9a10
> [eva] tests/value/from_termin.i:8: starting to merge loop iterations
diff tests/value/oracle/imprecise_invalid_write.res.oracle tests/value/oracle_equalities/imprecise_invalid_write.res.oracle
-27a28,29
+29a30,31
> [kernel] tests/value/imprecise_invalid_write.i:9:
> imprecise size for variable main1 (Undefined sizeof on a function.)
diff tests/value/oracle/incompatible_states.res.oracle tests/value/oracle_equalities/incompatible_states.res.oracle
@@ -347,26 +413,27 @@ diff tests/value/oracle/incompatible_states.res.oracle tests/value/oracle_equali
> The evaluation of the expression x * x
> led to bottom without alarms:
> at this point the product of states has no possible concretization.
-26,27c30,33
+27,29c31,34
< [eva:alarm] tests/value/incompatible_states.c:41: Warning:
-< accessing uninitialized left-value. assert \initialized(&t[(2 * i) / 2]);
+< accessing uninitialized left-value.
+< assert \initialized(&t[(int)((int)(2 * i) / 2)]);
---
> [eva] tests/value/incompatible_states.c:41:
> The evaluation of the expression t[(2 * i) / 2]
> led to bottom without alarms:
> at this point the product of states has no possible concretization.
-39,40d44
+41,42d45
< [eva:alarm] tests/value/incompatible_states.c:53: Warning:
< division by zero. assert t[i] ≢ 0;
-45,47d48
+47,49d49
< [eva] tests/value/incompatible_states.c:41:
< assertion 'Eva,initialization' got final status invalid.
< [scope:rm_asserts] removing 2 assertion(s)
-53c54
+55c55
< z ∈ [-3..100]
---
> z ∈ {-3; -2}
-56c57
+58c58
< t[0] ∈ {0; 1}
---
> t[0] ∈ {0}
@@ -375,7 +442,7 @@ diff tests/value/oracle/library.res.oracle tests/value/oracle_equalities/library
< [eva:alarm] tests/value/library.i:44: Warning:
< non-finite float value. assert \is_finite(*pf);
< [eva:alarm] tests/value/library.i:44: Warning:
-< non-finite float value. assert \is_finite((float)(*pf + *pf));
+< non-finite float value. assert \is_finite(\add_float(*pf, *pf));
diff tests/value/oracle/long_const.0.res.oracle tests/value/oracle_equalities/long_const.0.res.oracle
19c19,22
< [eva] tests/value/long_const.i:25: Reusing old results for call to LL_ABS
@@ -621,7 +688,7 @@ diff tests/value/oracle/non_natural.res.oracle tests/value/oracle_equalities/non
> [kernel] tests/value/non_natural.i:39:
> more than 200(12500) elements to enumerate. Approximating.
diff tests/value/oracle/nonlin.res.oracle tests/value/oracle_equalities/nonlin.res.oracle
-186c186
+188c188
< q ∈ {{ &x + [-400..400],0%4 }}
---
> q ∈ {{ &x }}
@@ -635,33 +702,37 @@ diff tests/value/oracle/octagons.res.oracle tests/value/oracle_equalities/octago
---
> t ∈ [6..4294967295] or UNINITIALIZED
diff tests/value/oracle/offsetmap.0.res.oracle tests/value/oracle_equalities/offsetmap.0.res.oracle
-38d37
+40d39
< [eva] Recording results for g
-40a40
+42a42
> [eva] Recording results for g
diff tests/value/oracle/offsetmap.1.res.oracle tests/value/oracle_equalities/offsetmap.1.res.oracle
-38d37
+40d39
< [eva] Recording results for g
-40a40
+42a42
> [eva] Recording results for g
diff tests/value/oracle/origin.0.res.oracle tests/value/oracle_equalities/origin.0.res.oracle
-226,227c226
+249,250c249
< pm2[bits 0 to 15]# ∈ {{ (? *)&a }}%32, bits 16 to 31
< [bits 16 to 31]# ∈ {{ (? *)&b }}%32, bits 0 to 15
---
> pm2 ∈ {{ &a + {-4} ; &b + {-4} }}
-266,267c265
+289,290c288
< pm2[bits 0 to 15]# ∈ {{ (? *)&a }}%32, bits 16 to 31
< [bits 16 to 31]# ∈ {{ (? *)&b }}%32, bits 0 to 15
---
> pm2 ∈ {{ &a + {-4} ; &b + {-4} }}
diff tests/value/oracle/period.res.oracle tests/value/oracle_equalities/period.res.oracle
-86,90d85
+88,94d87
+< [eva:alarm] tests/value/period.c:53: Warning:
+< pointer downcast. assert (unsigned int)(&g) ≤ 2147483647;
< [eva] tests/value/period.c:53:
< Assigning imprecise value to p.
< The imprecision originates from Arithmetic {tests/value/period.c:53}
< [eva:alarm] tests/value/period.c:54: Warning:
< out of bounds read. assert \valid_read(p);
+99d91
+< [scope:rm_asserts] removing 1 assertion(s)
diff tests/value/oracle/plevel.res.oracle tests/value/oracle_equalities/plevel.res.oracle
12d11
< [eva] Recording results for main
diff --git a/tests/value/diff_gauges b/tests/value/diff_gauges
index d6b0bc223014191dde0e3be2f4c34e02cd5021d2..55a5986c6614e0f6ee962fda6b7aa5413b05a8fc 100644
--- a/tests/value/diff_gauges
+++ b/tests/value/diff_gauges
@@ -80,7 +80,7 @@ diff tests/value/oracle/bad_loop.res.oracle tests/value/oracle_gauges/bad_loop.r
6a7
> [eva] tests/value/bad_loop.i:12: starting to merge loop iterations
diff tests/value/oracle/bitfield.res.oracle tests/value/oracle_gauges/bitfield.res.oracle
-132a133,147
+138a139,153
> [eva] tests/value/bitfield.i:71:
> Frama_C_show_each:
> {{ garbled mix of &{b} (origin: Misaligned {tests/value/bitfield.i:70}) }}
@@ -186,89 +186,89 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.o
---
> [eva] tests/value/gauges.c:172: Frama_C_show_each: [2147483647..4294967294]
> [eva] tests/value/gauges.c:172: Frama_C_show_each: [2147483647..4294967294]
-255,258d229
+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);
-266,271d236
+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++)
-299,300d263
+303,304d267
< [eva:alarm] tests/value/gauges.c:220: Warning:
< signed overflow. assert -2147483648 ≤ n - 1;
-315,318c278
+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}
-324,325d283
+328,329d287
< [eva:alarm] tests/value/gauges.c:251: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
-327c285
+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}
-333,336c291
+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}
-342,343d296
+346,347d300
< [eva:alarm] tests/value/gauges.c:274: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
-345c298
+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}
-353,354d305
+357,358d309
< [eva:alarm] tests/value/gauges.c:293: Warning:
< signed overflow. assert j + 1 ≤ 2147483647;
-356c307
+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]
-418a370,373
+422a374,377
> # Gauges domain:
> V: [{[ p -> {{ &x }}
> i -> {1} ]}]
> s398: λ(0)
-478a434,437
+482a438,441
> # Gauges domain:
> V: [{[ i -> {1} ]}]
> s398: λ([0 .. 1])
> {[ i -> {1} ]}
-537a497,500
+541a501,504
> # Gauges domain:
> V: [{[ i -> {1} ]}]
> s398: λ([0 .. 2])
> {[ i -> {1} ]}
-596a560,563
+600a564,567
> # Gauges domain:
> V: [{[ i -> {1} ]}]
> s398: λ([0 .. 10])
> {[ i -> {1} ]}
-661a629,633
+665a633,637
> # Gauges domain:
> V: [{[ p -> {{ &a }}
> i -> {2} ]}]
> s412: λ(0)
> s411: λ(0)
-722a695,699
+726a699,703
> # Gauges domain:
> V: [{[ i -> {2} ]}]
> s412: λ(0)
> s411: λ([0 .. 1])
> {[ i -> {0} ]}
-724a702,829
+728a706,833
> [eva] tests/value/gauges.c:325:
> Frama_C_dump_each:
> # Cvalue domain:
@@ -397,51 +397,51 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.o
> s411: λ([0 .. +oo])
> {[ i -> {0} ]}
> ==END OF DUMP==
-732a838,839
+736a842,843
> [eva] tests/value/gauges.c:343: Call to builtin malloc
> [eva] tests/value/gauges.c:343: Call to builtin malloc
-785,786c892,893
+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 }}
-798c905
+802c909
< n ∈ [-2147483648..99]
---
> n ∈ [-2147483547..99]
-804c911
+808c915
< i ∈ {45; 46; 47; 48; 49; 50; 51}
---
> i ∈ {45; 46; 47; 48}
-810c917
+814c921
< i ∈ {-59; -58; -57; -56; -55; -54; -53}
---
> i ∈ {-58; -57; -56; -55; -54; -53}
-830c937
+834c941
< p ∈ {{ &u + [0..--],0%4 }}
---
> p ∈ {{ &u + [0..400],0%4 }}
-832c939
+836c943
< k ∈ [0..2147483647]
---
> k ∈ [0..390]
-837c944
+841c948
< i ∈ [0..2147483647]
---
> i ∈ [0..21]
-848,849c955,957
+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] }}
-860c968
+864c972
< p ∈ {{ &T + [--..396],0%4 }}
---
> p ∈ {{ &T + [-4..396],0%4 }}
-865,869c973
+869,873c977
< n ∈ {0}
< arr[0] ∈ {0}
< [1] ∈ {-1}
@@ -449,19 +449,19 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.o
< p ∈ {{ &arr + [12..--],0%4 }}
---
> NON TERMINATING FUNCTION
-972a1077
+976a1081
> [from] Non-terminating function main8_aux (no dependencies)
-995,996c1100,1101
+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]
-1040c1145
+1044c1149
< NO EFFECTS
---
> NON TERMINATING - NO EFFECTS
-1074c1179
+1078c1183
< p; A[0..9]; B[0..9]
---
> p; A[0..8]; B[0..8]
@@ -587,7 +587,7 @@ diff tests/value/oracle/loopfun.1.res.oracle tests/value/oracle_gauges/loopfun.1
13a18
> [eva] tests/value/loopfun.i:27: starting to merge loop iterations
diff tests/value/oracle/memexec.res.oracle tests/value/oracle_gauges/memexec.res.oracle
-99a100
+101a102
> [eva] tests/value/memexec.c:98: starting to merge loop iterations
diff tests/value/oracle/modulo.res.oracle tests/value/oracle_gauges/modulo.res.oracle
40a41,123
@@ -1040,7 +1040,7 @@ diff tests/value/oracle/semaphore.res.oracle tests/value/oracle_gauges/semaphore
> Called from tests/value/semaphore.i:31.
> [eva] Done for function V
diff tests/value/oracle/symbolic_locs.res.oracle tests/value/oracle_gauges/symbolic_locs.res.oracle
-133a134
+135a136
> [eva] tests/value/symbolic_locs.i:93: starting to merge loop iterations
diff tests/value/oracle/undefined_sequence.0.res.oracle tests/value/oracle_gauges/undefined_sequence.0.res.oracle
97a98
diff --git a/tests/value/diff_octagons b/tests/value/diff_octagons
index a24807228bd0cf01a3b21383e795ebe3bff77c5b..8786bf632829b31384a2e29cf003d97301b6a853 100644
--- a/tests/value/diff_octagons
+++ b/tests/value/diff_octagons
@@ -34,7 +34,7 @@ diff tests/value/oracle/alias.6.res.oracle tests/value/oracle_octagons/alias.6.r
> tz2 ∈ {1}
> tz3 ∈ {1}
diff tests/value/oracle/bitfield.res.oracle tests/value/oracle_octagons/bitfield.res.oracle
-132a133,135
+138a139,141
> [eva] tests/value/bitfield.i:71:
> Frama_C_show_each:
> {{ garbled mix of &{b} (origin: Misaligned {tests/value/bitfield.i:70}) }}
@@ -79,12 +79,12 @@ diff tests/value/oracle/descending.res.oracle tests/value/oracle_octagons/descen
< i ∈ {31; 32}
---
> i ∈ {31}
-diff tests/value/oracle/downcast.res.oracle tests/value/oracle_octagons/downcast.res.oracle
+diff tests/value/oracle/downcast.1.res.oracle tests/value/oracle_octagons/downcast.1.res.oracle
61c61
< [100000..2147483647], [100145..2147483647], [100145..2147483647]
---
> [100000..2147483502], [100145..2147483647], [100145..2147483647]
-167c167
+166c166
< x_0 ∈ [100000..2147483647]
---
> x_0 ∈ [100000..2147483502]
@@ -119,24 +119,24 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_octagons/gauges.res
209,210d208
< [eva:alarm] tests/value/gauges.c:156: Warning:
< signed overflow. assert -2147483648 ≤ toCopy - 1;
-272,273d269
+276,277d273
< [eva:alarm] tests/value/gauges.c:201: Warning:
< signed overflow. assert -2147483648 ≤ numNonZero - 1;
-296,300d291
+300,304d295
< [eva] tests/value/gauges.c:218: Frama_C_show_each:
< [eva] tests/value/gauges.c:218: Frama_C_show_each:
< [eva] tests/value/gauges.c:218: Frama_C_show_each:
< [eva:alarm] tests/value/gauges.c:220: Warning:
< signed overflow. assert -2147483648 ≤ n - 1;
-787c778
+791c782
< numNonZero ∈ [-2147483648..8]
---
> numNonZero ∈ {-1}
-798c789
+802c793
< n ∈ [-2147483648..99]
---
> n ∈ {-1}
-859c850
+863c854
< toCopy ∈ [-2147483648..99]
---
> toCopy ∈ {-1}
@@ -238,22 +238,22 @@ diff tests/value/oracle/non_natural.res.oracle tests/value/oracle_octagons/non_n
> [kernel] tests/value/non_natural.i:39:
> more than 200(12500) elements to enumerate. Approximating.
diff tests/value/oracle/nonlin.res.oracle tests/value/oracle_octagons/nonlin.res.oracle
-105a106,107
+107a108,109
> [eva:nonlin] tests/value/nonlin.c:65: non-linear 'x * x', lv 'x'
> [eva:nonlin] tests/value/nonlin.c:65: subdividing on x
-108a111,113
+110a113,115
> [eva:nonlin] tests/value/nonlin.c:66: subdividing on x
> [eva:nonlin] tests/value/nonlin.c:66: non-linear 'y * y', lv 'y'
> [eva:nonlin] tests/value/nonlin.c:66: subdividing on y
-111a117,118
+113a119,120
> [eva:nonlin] tests/value/nonlin.c:68: non-linear 'z * x + x * y', lv 'x'
> [eva:nonlin] tests/value/nonlin.c:68: subdividing on x
-149a157,158
+151a159,160
> [eva:nonlin] tests/value/nonlin.c:112: non-linear 'x * x', lv 'x'
> [eva:nonlin] tests/value/nonlin.c:112: subdividing on x
-152a162
+154a164
> [eva:nonlin] tests/value/nonlin.c:113: subdividing on x
-153a164
+155a166
> [eva:nonlin] tests/value/nonlin.c:115: subdividing on x
diff tests/value/oracle/plevel.res.oracle tests/value/oracle_octagons/plevel.res.oracle
12d11
diff --git a/tests/value/diff_symblocs b/tests/value/diff_symblocs
index fdad91d414bade1b59b31b4515da631d2e84385e..a2095316e27d0cc8c465e64167fb860f90af592c 100644
--- a/tests/value/diff_symblocs
+++ b/tests/value/diff_symblocs
@@ -25,11 +25,11 @@ diff tests/value/oracle/alias.6.res.oracle tests/value/oracle_symblocs/alias.6.r
---
> x ∈ {33}
diff tests/value/oracle/bitwise_pointer.res.oracle tests/value/oracle_symblocs/bitwise_pointer.res.oracle
-58c58
+62c62
< x ∈ [0..9]
---
> x ∈ {5}
-71c71
+75c75
< x1 ∈ [0..9]
---
> x1 ∈ {5}
@@ -50,11 +50,50 @@ diff tests/value/oracle/bitwise_reduction.res.oracle tests/value/oracle_symblocs
< {0; 1}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
---
> {0; 1}, {0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
+diff tests/value/oracle/domains_function.res.oracle tests/value/oracle_symblocs/domains_function.res.oracle
+19,20c19
+< [eva] tests/value/domains_function.c:92:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:92: Frama_C_show_each_top: {3}
+28,29c27
+< [eva] tests/value/domains_function.c:77:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:77: Frama_C_show_each_top: {1}
+32,33c30
+< [eva] tests/value/domains_function.c:96:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+---
+> [eva] tests/value/domains_function.c:96: Frama_C_show_each_top: {1}
+52,56c49,50
+< [eva] computing for function not_enabled <- recursively_enabled <- main.
+< Called from tests/value/domains_function.c:110.
+< [eva] tests/value/domains_function.c:77: Frama_C_show_each_top: {1}
+< [eva] Recording results for not_enabled
+< [eva] Done for function not_enabled
+---
+> [eva] tests/value/domains_function.c:110:
+> Reusing old results for call to not_enabled
+58,63c52,53
+< [eva] computing for function disabled <- recursively_enabled <- main.
+< Called from tests/value/domains_function.c:112.
+< [eva] tests/value/domains_function.c:84:
+< Frama_C_show_each_top: [-2147483648..2147483647]
+< [eva] Recording results for disabled
+< [eva] Done for function disabled
+---
+> [eva] tests/value/domains_function.c:112:
+> Reusing old results for call to disabled
+130c120
+< result ∈ [--..--]
+---
+> result ∈ {1}
diff tests/value/oracle/incompatible_states.res.oracle tests/value/oracle_symblocs/incompatible_states.res.oracle
-39,40d38
+41,42d40
< [eva:alarm] tests/value/incompatible_states.c:53: Warning:
< division by zero. assert t[i] ≢ 0;
-47c45
+49c47
< [scope:rm_asserts] removing 2 assertion(s)
---
> [scope:rm_asserts] removing 1 assertion(s)
@@ -63,7 +102,7 @@ diff tests/value/oracle/library.res.oracle tests/value/oracle_symblocs/library.r
< [eva:alarm] tests/value/library.i:44: Warning:
< non-finite float value. assert \is_finite(*pf);
< [eva:alarm] tests/value/library.i:44: Warning:
-< non-finite float value. assert \is_finite((float)(*pf + *pf));
+< non-finite float value. assert \is_finite(\add_float(*pf, *pf));
diff tests/value/oracle/non_natural.res.oracle tests/value/oracle_symblocs/non_natural.res.oracle
58a59,60
> [kernel] tests/value/non_natural.i:30:
@@ -118,14 +157,14 @@ diff tests/value/oracle/non_natural.res.oracle tests/value/oracle_symblocs/non_n
> [kernel] tests/value/non_natural.i:39:
> more than 200(12500) elements to enumerate. Approximating.
diff tests/value/oracle/offsetmap.0.res.oracle tests/value/oracle_symblocs/offsetmap.0.res.oracle
-38d37
+40d39
< [eva] Recording results for g
-40a40
+42a42
> [eva] Recording results for g
diff tests/value/oracle/offsetmap.1.res.oracle tests/value/oracle_symblocs/offsetmap.1.res.oracle
-38d37
+40d39
< [eva] Recording results for g
-40a40
+42a42
> [eva] Recording results for g
diff tests/value/oracle/plevel.res.oracle tests/value/oracle_symblocs/plevel.res.oracle
12d11
@@ -237,7 +276,7 @@ diff tests/value/oracle/symbolic_locs.res.oracle tests/value/oracle_symblocs/sym
> Z: {[ ]}
> I: {[ ]}
> S: {[ ]}
-77a100,106
+79a102,108
> # Symbolic locations domain:
> V: {[ t[i] -> {{ &x }} ]}
> Z: {[ t[i] -> t[0..8]; i ]}
@@ -245,38 +284,38 @@ diff tests/value/oracle/symbolic_locs.res.oracle tests/value/oracle_symblocs/sym
> i -> {t[i]} ]}
> S: {[ i -> {t[i]}
> x -> {t[i]} ]}
-90a120,124
+92a122,126
> # Symbolic locations domain:
> V: {[ ]}
> Z: {[ ]}
> I: {[ ]}
> S: {[ ]}
-106a141,146
+108a143,148
> # Symbolic locations domain:
> V: {[ t[i] -> {1} ]}
> Z: {[ t[i] -> t[0..8]; i ]}
> I: {[ t -> {t[i]}
> i -> {t[i]} ]}
> S: {[ i -> {t[i]} ]}
-115a156,160
+117a158,162
> # Symbolic locations domain:
> V: {[ ]}
> Z: {[ ]}
> I: {[ ]}
> S: {[ ]}
-132a178,182
+134a180,184
> # Symbolic locations domain:
> V: {[ ]}
> Z: {[ ]}
> I: {[ ]}
> S: {[ ]}
-139,141c189
+141,143c191
< [eva:alarm] tests/value/symbolic_locs.i:111: Warning:
< signed overflow. assert *p + 1 ≤ 2147483647;
< [eva] tests/value/symbolic_locs.i:113: Frama_C_show_each: [0..2147483647]
---
> [eva] tests/value/symbolic_locs.i:113: Frama_C_show_each: [10001..2147483647]
-150a199,203
+152a201,205
> # Symbolic locations domain:
> V: {[ ]}
> Z: {[ ]}