diff --git a/src/plugins/value/utests b/src/plugins/value/utests
index bce097c3b1cfcea2ffac3282c750f757bd950bae..0b2cfea613cd1024532c5bbff89cae377bc921b5 100755
--- a/src/plugins/value/utests
+++ b/src/plugins/value/utests
@@ -12,7 +12,7 @@ if [ $res -ne 0 ]; then
fi
TESTS=(float value idct builtins)
-CONFIGS=(apron equalities bitwise symblocs gauges)
+CONFIGS=(apron equalities bitwise symblocs gauges octagons)
for C in ${CONFIGS[@]}
do
diff --git a/src/plugins/value/vtests b/src/plugins/value/vtests
index f03eac0072fb247668a1005922ae6f62319a7af6..2962dae8d845919d715d58362f08e97b0fd984d0 100755
--- a/src/plugins/value/vtests
+++ b/src/plugins/value/vtests
@@ -1,7 +1,7 @@
#!/bin/bash -eu
DEFAULT_TESTS=(float value idct builtins)
-CONFIGS=( apron equalities bitwise symblocs gauges)
+CONFIGS=( apron equalities bitwise symblocs gauges octagons)
ARGS=("${@-}")
diff --git a/tests/builtins/diff_octagons b/tests/builtins/diff_octagons
new file mode 100644
index 0000000000000000000000000000000000000000..0054c1a3abad131720e7bd2fa952732a6567d75c
--- /dev/null
+++ b/tests/builtins/diff_octagons
@@ -0,0 +1,335 @@
+diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_octagons/Longinit_sequencer.res.oracle
+327c327
+< tests/builtins/result/Longinit_sequencer.sav
+---
+> tests/builtins/result_octagons/Longinit_sequencer.sav
+568c568
+< tests/builtins/result/Longinit_sequencer.sav
+---
+> tests/builtins/result_octagons/Longinit_sequencer.sav
+diff tests/builtins/oracle/allocated.0.res.oracle tests/builtins/oracle_octagons/allocated.0.res.oracle
+273c273
+< j ∈ [1..2147483647]
+---
+> 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
+> [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_7
+208a212,214
+> strong free on bases: {__malloc_main_l82_7}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+223a230,232
+> strong free on bases: {__malloc_main_l82_7}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+238a248,250
+> strong free on bases: {__malloc_main_l82_7}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+252,254c264,266
+< [eva] tests/builtins/allocated.c:82:
+< Call to builtin Frama_C_malloc_fresh for function malloc
+< [eva] tests/builtins/allocated.c:82: allocating variable __malloc_main_l82_7
+---
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_7}
+323a336,356
+> [eva] tests/builtins/allocated.c:82:
+> Call to builtin Frama_C_malloc_fresh for function malloc
+> [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: 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: 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: 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: 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: 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: allocating variable __malloc_main_l82_37
+329,330d361
+< Trace partitioning superposing up to 300 states
+< [eva] tests/builtins/allocated.c:84:
+333a365,385
+> strong free on bases: {__malloc_main_l82_37}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_32}
+> [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}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+403c455,473
+< strong free on bases: {__malloc_main_l82_7}
+---
+> 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:
+> strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_32}
+> [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
+< strong free on bases: {__malloc_main_l82_7}
+---
+> 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:
+> strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_32}
+> [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
+< strong free on bases: {__malloc_main_l82_7}
+---
+> 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:
+> strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_32}
+> [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
+< strong free on bases: {__malloc_main_l82_7}
+---
+> 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:
+> strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_32}
+> [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
+< strong free on bases: {__malloc_main_l82_7}
+---
+> 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:
+> strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_32}
+> [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
+< strong free on bases: {__malloc_main_l82_7}
+---
+> 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:
+> strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_32}
+> [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
+< strong free on bases: {__malloc_main_l82_7}
+---
+> 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:
+> strong free on bases: {__malloc_main_l82_36}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_35}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_34}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_33}
+> [eva] tests/builtins/allocated.c:87: Call to builtin free
+> [eva:malloc] tests/builtins/allocated.c:87:
+> strong free on bases: {__malloc_main_l82_32}
+> [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
+< [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
+< __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
+> __malloc_main_l82_31[0] ∈ {21} or UNINITIALIZED
+> [1] ∈ {24} or UNINITIALIZED
+> [2] ∈ {27} or UNINITIALIZED
+> __malloc_main_l82_32[0] ∈ {21} or UNINITIALIZED
+> [1] ∈ {24} or UNINITIALIZED
+> [2] ∈ {27} or UNINITIALIZED
+> __malloc_main_l82_33[0] ∈ {21} or UNINITIALIZED
+> [1] ∈ {24} or UNINITIALIZED
+> [2] ∈ {27} or UNINITIALIZED
+> __malloc_main_l82_34[0] ∈ {21} or UNINITIALIZED
+> [1] ∈ {24} or UNINITIALIZED
+> [2] ∈ {27} or UNINITIALIZED
+> __malloc_main_l82_35[0] ∈ {21} or UNINITIALIZED
+> [1] ∈ {24} or UNINITIALIZED
+> [2] ∈ {27} or UNINITIALIZED
+> __malloc_main_l82_36[0] ∈ {21} or UNINITIALIZED
+> [1] ∈ {24} or UNINITIALIZED
+> [2] ∈ {27} or UNINITIALIZED
+> __malloc_main_l82_37[0] ∈ {21} or UNINITIALIZED
+> [1] ∈ {24} or UNINITIALIZED
+> [2] ∈ {27} or UNINITIALIZED
+1184c1381
+< __malloc_main_l82_7[0..2] FROM __fc_heap_status; nondet (and SELF)
+---
+> __malloc_main_l82_7[0..1] FROM __fc_heap_status; nondet (and SELF)
+1207a1405,1411
+> __malloc_main_l82_31[0..2] FROM __fc_heap_status; nondet (and SELF)
+> __malloc_main_l82_32[0..2] FROM __fc_heap_status; nondet (and SELF)
+> __malloc_main_l82_33[0..2] FROM __fc_heap_status; nondet (and SELF)
+> __malloc_main_l82_34[0..2] FROM __fc_heap_status; nondet (and SELF)
+> __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
+< __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
+< __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];
+---
+> __malloc_main_l82_30[0..2]; __malloc_main_l82_31[0..2];
+> __malloc_main_l82_32[0..2]; __malloc_main_l82_33[0..2];
+> __malloc_main_l82_34[0..2]; __malloc_main_l82_35[0..2];
+> __malloc_main_l82_36[0..2]; __malloc_main_l82_37[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 tests/builtins/oracle/imprecise.res.oracle tests/builtins/oracle_octagons/imprecise.res.oracle
+224a225,226
+> [kernel] tests/builtins/imprecise.c:111:
+> more than 200(300) elements to enumerate. Approximating.
+233a236,237
+> [kernel] tests/builtins/imprecise.c:114:
+> more than 200(300) elements to enumerate. Approximating.
+237,240d240
+< [kernel] tests/builtins/imprecise.c:111:
+< more than 200(300) elements to enumerate. Approximating.
+< [kernel] tests/builtins/imprecise.c:114:
+< more than 200(300) elements to enumerate. Approximating.
+diff tests/builtins/oracle/linked_list.1.res.oracle tests/builtins/oracle_octagons/linked_list.1.res.oracle
+506a507,508
+> [kernel] tests/builtins/linked_list.c:43:
+> more than 100(128) elements to enumerate. Approximating.
+508a511,512
+> [kernel] tests/builtins/linked_list.c:44:
+> more than 100(128) elements to enumerate. Approximating.
+600,603d603
+< [kernel] tests/builtins/linked_list.c:43:
+< more than 100(128) elements to enumerate. Approximating.
+< [kernel] tests/builtins/linked_list.c:44:
+< more than 100(128) elements to enumerate. Approximating.
+diff tests/builtins/oracle/malloc-optimistic.res.oracle tests/builtins/oracle_octagons/malloc-optimistic.res.oracle
+3520c3520
+< i ∈ [14..100]
+---
+> i ∈ {98; 99; 100}
+3524c3524
+< i ∈ [14..100]
+---
+> i ∈ {98; 99; 100}
diff --git a/tests/builtins/test_config_octagons b/tests/builtins/test_config_octagons
new file mode 100644
index 0000000000000000000000000000000000000000..577aa8ef1795bfa93357f06a555474871a075d42
--- /dev/null
+++ b/tests/builtins/test_config_octagons
@@ -0,0 +1,3 @@
+MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-octagons-domain
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/float/diff_octagons b/tests/float/diff_octagons
new file mode 100644
index 0000000000000000000000000000000000000000..806b63f0fdd00d77aa58baea79238e5893426733
--- /dev/null
+++ b/tests/float/diff_octagons
@@ -0,0 +1,18 @@
+Only in tests/float/oracle: absorb.res.oracle
+Only in tests/float/oracle: absorb_sav.err
+Only in tests/float/oracle: absorb_sav.res
+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
+253a254,255
+> [eva:nonlin] tests/float/nonlin.c:101: non-linear 'f + f', lv 'f'
+> [eva:nonlin] tests/float/nonlin.c:101: subdividing on f
+257d258
+< [eva:nonlin] tests/float/nonlin.c:101: subdividing on f
+diff tests/float/oracle/nonlin.3.res.oracle tests/float/oracle_octagons/nonlin.3.res.oracle
+253a254,255
+> [eva:nonlin] tests/float/nonlin.c:101: non-linear 'f + f', lv 'f'
+> [eva:nonlin] tests/float/nonlin.c:101: subdividing on f
+257d258
+< [eva:nonlin] tests/float/nonlin.c:101: subdividing on f
diff --git a/tests/idct/diff_octagons b/tests/idct/diff_octagons
new file mode 100644
index 0000000000000000000000000000000000000000..46e477e3f73c2fc3d4aa05888afdfc1d43d7b003
--- /dev/null
+++ b/tests/idct/diff_octagons
@@ -0,0 +1,78 @@
+diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_octagons/ieee_1180_1990.res.oracle
+424a425,432
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+498a507,514
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+571a588,595
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+> [eva] tests/idct/ieee_1180_1990.c:85:
+> Reusing old results for call to IEEE_1180_1990_rand
+579a604,617
+> [eva] tests/idct/ieee_1180_1990.c:100:
+> Call to builtin Frama_C_sqrt for function sqrt
+> [eva] tests/idct/ieee_1180_1990.c:101:
+> Call to builtin Frama_C_cos for function cos
+> [eva] tests/idct/ieee_1180_1990.c:100:
+> Call to builtin Frama_C_sqrt for function sqrt
+> [eva] tests/idct/ieee_1180_1990.c:101:
+> Call to builtin Frama_C_cos for function cos
+> [eva] tests/idct/ieee_1180_1990.c:100:
+> Call to builtin Frama_C_sqrt for function sqrt
+> [eva] tests/idct/ieee_1180_1990.c:101:
+> Call to builtin Frama_C_cos for function cos
+> [eva] tests/idct/ieee_1180_1990.c:100:
+> Call to builtin Frama_C_sqrt for function sqrt
+581a620,621
+> [eva] tests/idct/ieee_1180_1990.c:100:
+> Call to builtin Frama_C_sqrt for function sqrt
+583a624,629
+> [eva] tests/idct/ieee_1180_1990.c:100:
+> Call to builtin Frama_C_sqrt for function sqrt
+> [eva] tests/idct/ieee_1180_1990.c:101:
+> Call to builtin Frama_C_cos for function cos
+> [eva] tests/idct/ieee_1180_1990.c:100:
+> Call to builtin Frama_C_sqrt for function sqrt
+605a652,661
+> [eva] tests/idct/ieee_1180_1990.c:140:
+> Call to builtin Frama_C_sqrt for function sqrt
+> [eva] tests/idct/ieee_1180_1990.c:141:
+> Call to builtin Frama_C_cos for function cos
+> [eva] tests/idct/ieee_1180_1990.c:140:
+> Call to builtin Frama_C_sqrt for function sqrt
+> [eva] tests/idct/ieee_1180_1990.c:141:
+> Call to builtin Frama_C_cos for function cos
+> [eva] tests/idct/ieee_1180_1990.c:140:
+> Call to builtin Frama_C_sqrt for function sqrt
+607a664,665
+> [eva] tests/idct/ieee_1180_1990.c:140:
+> Call to builtin Frama_C_sqrt for function sqrt
+609a668,677
+> [eva] tests/idct/ieee_1180_1990.c:140:
+> Call to builtin Frama_C_sqrt for function sqrt
+> [eva] tests/idct/ieee_1180_1990.c:141:
+> Call to builtin Frama_C_cos for function cos
+> [eva] tests/idct/ieee_1180_1990.c:140:
+> Call to builtin Frama_C_sqrt for function sqrt
+> [eva] tests/idct/ieee_1180_1990.c:141:
+> Call to builtin Frama_C_cos for function cos
+> [eva] tests/idct/ieee_1180_1990.c:140:
+> Call to builtin Frama_C_sqrt for function sqrt
diff --git a/tests/test_config_octagons b/tests/test_config_octagons
new file mode 100644
index 0000000000000000000000000000000000000000..43c789be567604dbbdb35d3aa449b6caeee10bd7
--- /dev/null
+++ b/tests/test_config_octagons
@@ -0,0 +1,3 @@
+MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-octagons-domain
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/value/diff_octagons b/tests/value/diff_octagons
new file mode 100644
index 0000000000000000000000000000000000000000..2b5ae606dfe09be4f1aa091b2742ab58c421eb1f
--- /dev/null
+++ b/tests/value/diff_octagons
@@ -0,0 +1,399 @@
+diff tests/value/oracle/alias.1.res.oracle tests/value/oracle_octagons/alias.1.res.oracle
+85c85
+< z ∈ {0; 1; 2}
+---
+> z ∈ {0; 2}
+diff tests/value/oracle/alias.2.res.oracle tests/value/oracle_octagons/alias.2.res.oracle
+76c76
+< z ∈ {-5; -4; -3; -2; -1; 0; 1; 1000}
+---
+> z ∈ {-2; -1; 0; 1000}
+diff tests/value/oracle/alias.3.res.oracle tests/value/oracle_octagons/alias.3.res.oracle
+67c67
+< z ∈ {0; 1; 2}
+---
+> z ∈ {0; 2}
+diff tests/value/oracle/alias.5.res.oracle tests/value/oracle_octagons/alias.5.res.oracle
+59a60
+> [eva] tests/value/alias.i:260: starting to merge loop iterations
+diff tests/value/oracle/alias.6.res.oracle tests/value/oracle_octagons/alias.6.res.oracle
+82c82
+< t ∈ {4; 5; 6}
+---
+> t ∈ {5}
+87c87
+< y ∈ {0; 1}
+---
+> y ∈ {1}
+94,96c94,96
+< tz1 ∈ {0; 1}
+< tz2 ∈ {0; 1}
+< tz3 ∈ {0; 1}
+---
+> tz1 ∈ {1}
+> tz2 ∈ {1}
+> tz3 ∈ {1}
+diff tests/value/oracle/bitfield.res.oracle tests/value/oracle_octagons/bitfield.res.oracle
+132a133,135
+> [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/builtins_split.res.oracle tests/value/oracle_octagons/builtins_split.res.oracle
+70a71,84
+> [eva] tests/value/builtins_split.c:104:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:104:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:104:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:104:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:104:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:104:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:104:
+> Call to builtin Frama_C_builtin_split_all
+81a96,109
+> [eva] tests/value/builtins_split.c:112:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:112:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:112:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:112:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:112:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:112:
+> Call to builtin Frama_C_builtin_split_all
+> [eva] tests/value/builtins_split.c:112:
+> Call to builtin Frama_C_builtin_split_all
+diff tests/value/oracle/call_simple.res.oracle tests/value/oracle_octagons/call_simple.res.oracle
+28c28
+< c ∈ [--..--]
+---
+> c ∈ [-2147483648..2147483646]
+diff tests/value/oracle/descending.res.oracle tests/value/oracle_octagons/descending.res.oracle
+42c42
+< i ∈ {31; 32}
+---
+> i ∈ {31}
+diff tests/value/oracle/downcast.res.oracle tests/value/oracle_octagons/downcast.res.oracle
+61c61
+< [100000..2147483647], [100145..2147483647], [100145..2147483647]
+---
+> [100000..2147483502], [100145..2147483647], [100145..2147483647]
+167c167
+< x_0 ∈ [100000..2147483647]
+---
+> x_0 ∈ [100000..2147483502]
+diff tests/value/oracle/equality.res.oracle tests/value/oracle_octagons/equality.res.oracle
+29,30c29,30
+< y ∈ [0..42] or UNINITIALIZED
+< w ∈ [0..42] or UNINITIALIZED
+---
+> y ∈ [0..42]
+> w ∈ [0..42]
+diff tests/value/oracle/find_ivaltop.res.oracle tests/value/oracle_octagons/find_ivaltop.res.oracle
+32,33c32,33
+< j ∈ {0; 1; 2; 3; 4; 5; 6; 7}
+< X ∈ {1; 2; 3; 4; 5; 6; 7; 8}
+---
+> j ∈ {7}
+> X ∈ {8}
+39c39
+< \result FROM t[0..7]
+---
+> \result FROM t[7]
+44c44
+< t[0..7]
+---
+> t[7]
+diff tests/value/oracle/for_loops.3.res.oracle tests/value/oracle_octagons/for_loops.3.res.oracle
+20c20
+< v ∈ [0..2147483647]
+---
+> v ∈ [5..2147483647]
+diff tests/value/oracle/gauges.res.oracle tests/value/oracle_octagons/gauges.res.oracle
+209,210d208
+< [eva:alarm] tests/value/gauges.c:156: Warning:
+< signed overflow. assert -2147483648 ≤ toCopy - 1;
+272,273d269
+< [eva:alarm] tests/value/gauges.c:201: Warning:
+< signed overflow. assert -2147483648 ≤ numNonZero - 1;
+296,300d291
+< [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
+< numNonZero ∈ [-2147483648..8]
+---
+> numNonZero ∈ {-1}
+798c789
+< n ∈ [-2147483648..99]
+---
+> n ∈ {-1}
+859c850
+< toCopy ∈ [-2147483648..99]
+---
+> toCopy ∈ {-1}
+diff tests/value/oracle/loop.res.oracle tests/value/oracle_octagons/loop.res.oracle
+26c26
+< r ∈ [0..2147483646],0%2
+---
+> r ∈ [46..2147483646],0%2
+diff tests/value/oracle/loop_wvar.1.res.oracle tests/value/oracle_octagons/loop_wvar.1.res.oracle
+12,13d11
+< [eva:alarm] tests/value/loop_wvar.i:57: Warning:
+< signed overflow. assert next + 1 ≤ 2147483647;
+41c39
+< next ∈ [0..2147483647]
+---
+> next ∈ [0..25]
+diff tests/value/oracle/modulo.res.oracle tests/value/oracle_octagons/modulo.res.oracle
+40a41,56
+> [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}
+50a67,82
+> [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}
+60a93,94
+> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-10..10], [-9..9], [-8..8]
+> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-9..9], [-8..8], [-7..7]
+diff tests/value/oracle/non_natural.res.oracle tests/value/oracle_octagons/non_natural.res.oracle
+58a59,60
+> [kernel] tests/value/non_natural.i:30:
+> more than 200(12500) elements to enumerate. Approximating.
+65a68,69
+> [kernel] tests/value/non_natural.i:23:
+> more than 200(12500) elements to enumerate. Approximating.
+70a75,76
+> [kernel] tests/value/non_natural.i:24:
+> more than 200(12500) elements to enumerate. Approximating.
+78a85,86
+> [kernel] tests/value/non_natural.i:25:
+> more than 200(12500) elements to enumerate. Approximating.
+86a95,96
+> [kernel] tests/value/non_natural.i:26:
+> more than 200(12500) elements to enumerate. Approximating.
+94a105,106
+> [kernel] tests/value/non_natural.i:27:
+> more than 200(12500) elements to enumerate. Approximating.
+102a115,116
+> [kernel] tests/value/non_natural.i:28:
+> more than 200(12500) elements to enumerate. Approximating.
+110a125,126
+> [kernel] tests/value/non_natural.i:29:
+> more than 200(12500) elements to enumerate. Approximating.
+129,130d144
+< [kernel] tests/value/non_natural.i:23:
+< more than 200(12500) elements to enumerate. Approximating.
+133,146d146
+< [kernel] tests/value/non_natural.i:24:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:25:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:26:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:27:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:28:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:29:
+< more than 200(12500) elements to enumerate. Approximating.
+< [kernel] tests/value/non_natural.i:30:
+< more than 200(12500) elements to enumerate. Approximating.
+199a200,201
+> [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
+> [eva:nonlin] tests/value/nonlin.c:67: non-linear 'x * x', lv 'x'
+> [eva:nonlin] tests/value/nonlin.c:67: subdividing on x
+108a111,113
+> [eva:nonlin] tests/value/nonlin.c:68: subdividing on x
+> [eva:nonlin] tests/value/nonlin.c:68: non-linear 'y * y', lv 'y'
+> [eva:nonlin] tests/value/nonlin.c:68: subdividing on y
+111a117,118
+> [eva:nonlin] tests/value/nonlin.c:70: non-linear 'z * x + x * y', lv 'x'
+> [eva:nonlin] tests/value/nonlin.c:70: subdividing on x
+176,178c183,185
+< square ∈ [-48..400]
+< square2 ∈ [-48..400]
+< res ∈ [-144..400]
+---
+> square ∈ [-200..400]
+> square2 ∈ [-200..400]
+> res ∈ [-200..400]
+diff tests/value/oracle/plevel.res.oracle tests/value/oracle_octagons/plevel.res.oracle
+12d11
+< [eva] Recording results for main
+14a14
+> [eva] Recording results for main
+diff tests/value/oracle/ptr_relation.1.res.oracle tests/value/oracle_octagons/ptr_relation.1.res.oracle
+24c24
+< j ∈ {-1; 0; 1}
+---
+> j ∈ {0}
+diff tests/value/oracle/relation_reduction.res.oracle tests/value/oracle_octagons/relation_reduction.res.oracle
+24,27d23
+< [eva:alarm] tests/value/relation_reduction.i:20: Warning:
+< accessing out of bounds index. assert 0 ≤ y;
+< [eva:alarm] tests/value/relation_reduction.i:20: Warning:
+< accessing out of bounds index. assert y < 9;
+34,37c30,33
+< R1 ∈ [-2147483648..2147483637]
+< R2 ∈ [-2147483638..2147483647]
+< R3 ∈ [--..--]
+< R4 ∈ {0; 1; 2; 3; 4; 5}
+---
+> R1 ∈ {0; 2}
+> R2 ∈ {0; 12}
+> R3 ∈ {0; 7}
+> R4 ∈ {0; 2}
+48c44
+< R4 FROM tab[0..8]; x (and SELF)
+---
+> R4 FROM tab[0..5]; x (and SELF)
+53c49
+< y; t; tab[0..8]
+---
+> y; t; tab[0..5]
+diff tests/value/oracle/relation_shift.res.oracle tests/value/oracle_octagons/relation_shift.res.oracle
+18,25d17
+< [eva:alarm] tests/value/relation_shift.i:15: Warning:
+< signed overflow. assert -2147483648 ≤ x - y;
+< [eva:alarm] tests/value/relation_shift.i:15: Warning:
+< signed overflow. assert x - y ≤ 2147483647;
+< [eva:alarm] tests/value/relation_shift.i:16: Warning:
+< signed overflow. assert -2147483648 ≤ z - y;
+< [eva:alarm] tests/value/relation_shift.i:16: Warning:
+< signed overflow. assert z - y ≤ 2147483647;
+31,32c23,24
+< r1 ∈ [--..--]
+< r2 ∈ [--..--]
+---
+> r1 ∈ {2}
+> r2 ∈ {7}
+35,37c27,29
+< x ∈ [-2147483647..2147483647]
+< y ∈ [-2147483648..2147483646]
+< z ∈ [-2147483642..2147483647]
+---
+> x ∈ [-2147483646..2147483642]
+> y ∈ [-2147483648..2147483640]
+> z ∈ [-2147483641..2147483647]
+49,50c41,42
+< r1 ∈ [--..--]
+< r2 ∈ [--..--]
+---
+> r1 ∈ {2}
+> r2 ∈ {7}
+53,55c45,47
+< x ∈ [-2147483647..2147483647]
+< y ∈ [-2147483648..2147483646]
+< z ∈ [-2147483642..2147483647]
+---
+> x ∈ [-2147483646..2147483642]
+> y ∈ [-2147483648..2147483640]
+> z ∈ [-2147483641..2147483647]
+diff tests/value/oracle/relations.res.oracle tests/value/oracle_octagons/relations.res.oracle
+80,81c80,82
+< e ∈ [--..--]
+< f ∈ [--..--]
+---
+> e ∈ {1}
+> f[bits 0 to 7] ∈ {1; 4}
+> [bits 8 to 31] ∈ [--..--]
+diff tests/value/oracle/relations2.res.oracle tests/value/oracle_octagons/relations2.res.oracle
+25c25
+< len ∈ [--..--]
+---
+> len ∈ [0..1023]
+36,37c36
+< [eva] tests/value/relations2.i:17:
+< Frama_C_show_each_end: [0..4294967295], [0..64]
+---
+> [eva] tests/value/relations2.i:17: Frama_C_show_each_end: [0..1023], [0..64]
+59c58
+< n ∈ [0..512]
+---
+> n ∈ [1..512]
+69,71d67
+< [eva:alarm] tests/value/relations2.i:34: Warning:
+< accessing out of bounds index.
+< assert (unsigned int)(i - (unsigned int)(t + 1)) < 514;
+80c76
+< n ∈ [0..512]
+---
+> n ∈ [1..512]
+97c93
+< n ∈ [0..512]
+---
+> n ∈ [1..512]
+140c136
+< len ∈ [--..--]
+---
+> len ∈ [0..1023]
+diff tests/value/oracle/semaphore.res.oracle tests/value/oracle_octagons/semaphore.res.oracle
+65c65
+< c ∈ {-26; -1}
+---
+> c ∈ {-1}
+diff tests/value/oracle/struct2.res.oracle tests/value/oracle_octagons/struct2.res.oracle
+81,84d80
+< accessing out of bounds index. assert 0 ≤ (int)(i + j);
+< [eva:alarm] tests/value/struct2.i:185: Warning:
+< accessing out of bounds index. assert (int)(i + j) < 2;
+< [eva:alarm] tests/value/struct2.i:185: Warning:
+106d101
+< [scope:rm_asserts] removing 2 assertion(s)
+diff tests/value/oracle/test.0.res.oracle tests/value/oracle_octagons/test.0.res.oracle
+17,18d16
+< [eva:alarm] tests/value/test.i:11: Warning:
+< signed overflow. assert j + ecart ≤ 2147483647;
+29c27
+< j ∈ [-1073741822..1]
+---
+> j ∈ {-1; 0; 1}
+diff tests/value/oracle/unroll.res.oracle tests/value/oracle_octagons/unroll.res.oracle
+22c22
+< G ∈ [17739..2147483647]
+---
+> G ∈ [17854..2147483647]
+diff tests/value/oracle/unroll_simple.res.oracle tests/value/oracle_octagons/unroll_simple.res.oracle
+17c17
+< G ∈ [8772..2147483647]
+---
+> G ∈ [8896..2147483647]