Merge branch 'fix/eva/alternative-oracles' into 'master'

[Eva] Updates test oracles for alternative domains

See merge request frama-c/frama-c!2985

tests/builtins/diff_apron

-diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_apron/Longinit_sequencer.res.oracle
-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
-< [eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze
----
-> [eva] computing for function subanalyze <- analyze <- init_inner <- init_outer <- 
->                           main.
->   Called from tests/builtins/long_init.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] computing for function subanalyze <- analyze <- init_inner <- init_outer <- 
->                           main.
->   Called from tests/builtins/long_init.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] computing for function subanalyze <- analyze <- init_inner <- init_outer <- 
->                           main.
->   Called from tests/builtins/long_init.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] computing for function subanalyze <- analyze <- init_inner <- init_outer <- 
->                           main.
->   Called from tests/builtins/long_init.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-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
----
-> [eva] computing for function analyze <- main.
->   Called from tests/builtins/long_init.c:93.
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] Recording results for analyze
-> [eva] Done for function analyze
-> [eva] computing for function analyze <- main.
->   Called from tests/builtins/long_init.c:94.
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] Recording results for analyze
-> [eva] Done for function analyze
-320c382
-<   tests/builtins/result/Longinit_sequencer.sav
----
->   tests/builtins/result_apron/Longinit_sequencer.sav
-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
-< [eva] tests/builtins/long_init2.c:29: Reusing old results for call to subanalyze
----
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init2.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init2.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init2.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init2.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-556c630
-<   tests/builtins/result/Longinit_sequencer.sav
----
->   tests/builtins/result_apron/Longinit_sequencer.sav
-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
-< [eva] tests/builtins/long_init3.c:29: Reusing old results for call to subanalyze
----
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init3.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init3.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init3.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
-> [eva] computing for function subanalyze <- analyze <- main.
->   Called from tests/builtins/long_init3.c:29.
-> [eva] Recording results for subanalyze
-> [eva] Done for function subanalyze
 diff tests/builtins/oracle/allocated.0.res.oracle tests/builtins/oracle_apron/allocated.0.res.oracle
 260a261,263
 > [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc

tests/builtins/diff_bitwise

-diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_bitwise/Longinit_sequencer.res.oracle
-320c320
-<   tests/builtins/result/Longinit_sequencer.sav
----
->   tests/builtins/result_bitwise/Longinit_sequencer.sav
-556c556
-<   tests/builtins/result/Longinit_sequencer.sav
----
->   tests/builtins/result_bitwise/Longinit_sequencer.sav
 diff tests/builtins/oracle/allocated.0.res.oracle tests/builtins/oracle_bitwise/allocated.0.res.oracle
 260a261,263
 > [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc

tests/builtins/diff_equalities

-diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_equalities/Longinit_sequencer.res.oracle
-320c320
-<   tests/builtins/result/Longinit_sequencer.sav
----
->   tests/builtins/result_equalities/Longinit_sequencer.sav
-556c556
-<   tests/builtins/result/Longinit_sequencer.sav
----
->   tests/builtins/result_equalities/Longinit_sequencer.sav
 diff tests/builtins/oracle/alloc_weak.res.oracle tests/builtins/oracle_equalities/alloc_weak.res.oracle
 36,37d35
 < [eva:alarm] tests/builtins/alloc_weak.c:30: Warning: 

tests/builtins/diff_gauges

-diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_gauges/Longinit_sequencer.res.oracle
-320c320
-<   tests/builtins/result/Longinit_sequencer.sav
----
->   tests/builtins/result_gauges/Longinit_sequencer.sav
-556c556
-<   tests/builtins/result/Longinit_sequencer.sav
----
->   tests/builtins/result_gauges/Longinit_sequencer.sav
 diff tests/builtins/oracle/linked_list.0.res.oracle tests/builtins/oracle_gauges/linked_list.0.res.oracle
 1122a1123,1128
 > [eva] computing for function printf_va_1 <- main.

tests/builtins/diff_octagons

-diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_octagons/Longinit_sequencer.res.oracle
-320c320
-<   tests/builtins/result/Longinit_sequencer.sav
----
->   tests/builtins/result_octagons/Longinit_sequencer.sav
-556c556
-<   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]

tests/builtins/diff_symblocs

-diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_symblocs/Longinit_sequencer.res.oracle
-320c320
-<   tests/builtins/result/Longinit_sequencer.sav
----
->   tests/builtins/result_symblocs/Longinit_sequencer.sav
-556c556
-<   tests/builtins/result/Longinit_sequencer.sav
----
->   tests/builtins/result_symblocs/Longinit_sequencer.sav
 diff tests/builtins/oracle/alloc_weak.res.oracle tests/builtins/oracle_symblocs/alloc_weak.res.oracle
 36,37d35
 < [eva:alarm] tests/builtins/alloc_weak.c:30: Warning: 

tests/builtins/long_init.c

-/* run.config*
-   DONTRUN: tests run by Longinit_sequencer.i
-*/
-
-#include <stdlib.h>
-
-#define N1 10
-#define N2 50
-#define N3 10
-
-volatile int nondet;
-
-int a1[N1];
-struct st {
-  unsigned long t[N2];
-  double d[N3];
-} stuff;
-
-double subanalyze(double *d) {
-  return *d < 15 ? 1.0 : *d / 15.0;
-}
-
-double analyze(int *a, unsigned long *b, double *c) {
-  int i;
-  double res = 0.0;
-  /*@ slevel 5; */
-  for (i = 0; i < 5; i++) {
-    res += a[i + 3] + b[i * 2] + c[i + 1];
-    res += subanalyze(&c[i + 1]);
-  }
-  return res;
-}
-
-char garbled_mix = (char) "abc";
-char *s = "abc";
-//int another_global = 42; // from init_global2.c
-//int yet_another_global = 43; // from init_global3.c
-double *pr, *pr2, *pr_escaping, **ppr;
-int *alloc1, *alloc2, *alloc3;
-
-double dmin(double *pd1, double *pd2) {
-  if (*pd1 < *pd2) return *pd1;
-  else return *pd2;
-}
-
-int fun(int k) {
-  return k+1;
-}
-
-typedef int (*i_fp_i)(int);
-i_fp_i fp = &fun;
-
-/*@ assigns a1[..], stuff, pr, pr2, pr_escaping, alloc1, alloc2
-      \from \nothing; */
-void init_inner(int n, char const *tea) {
-  int i;
-  /*@ slevel N3; */
-  for (i = 0; i < N1; i++) {
-    a1[i] = i;
-  }
-  for (i = 0; i < N2; i++) {
-    stuff.t[i] = a1[i/5] + 3;
-  }
-  for (i = 0; i < N3; i++) {
-    stuff.d[i] = 3.125 * i;
-  }
-  /*@ slevel 0; */
-  double r = analyze(a1, stuff.t, stuff.d);
-  double r2 = analyze(a1, stuff.t+1, stuff.d+1);
-  pr = nondet ? &r : &r2;
-  pr2 = &r2;
-  pr_escaping = &r2;
-  alloc1 = malloc(sizeof(int*));
-  *alloc1 = (int) alloc1;
-  alloc2 = malloc(2*sizeof(int));
-  *alloc2 = 37;
-  free(alloc2);
-}
-
-int inited;
-
-/*@ assigns a1[..], stuff, pr, pr2, pr_escaping, alloc1, alloc2, inited
-      \from \nothing; */
-void init_outer() {
-    init_inner(13, "tea");
-    inited = 1;
-}
-
-int main() {
-  init_outer();
-  char *sa = s;
-  Frama_C_dump_each();
-  double r = analyze(a1, stuff.t, stuff.d);
-  double r2 = analyze(a1, stuff.t+1, stuff.d+1);
-  pr = nondet ? &r : &r2;
-  pr2 = nondet ? &r : &r2;
-  ppr = nondet ? &pr : &pr2;
-  double dm = dmin(pr, *ppr);
-  int res_from_fp = (*fp)(31);
-  int res = (int)r % 256;
-  *alloc1 = inited;
-  int local = *alloc1;
-  free(alloc1);
-  alloc3 = malloc(sizeof(int));
-  //local = another_global; // from init_global2.c
-  //int local2 = yet_another_global; // from init_global3.c
-  return 0;
-}

tests/builtins/long_init2.c

-/* run.config*
-   DONTRUN: tests run by Longinit_sequencer.i
-*/
-
-#include <stdlib.h>
-
-#define N1 10
-#define N2 50
-#define N3 10
-
-volatile int nondet;
-
-int a1[N1];
-struct st {
-  unsigned long t[N2];
-  double d[N3];
-} stuff;
-
-double subanalyze(double *d) {
-  return *d < 15 ? 1.0 : *d / 15.0;
-}
-
-double analyze(int *a, unsigned long *b, double *c) {
-  int i;
-  double res = 0.0;
-  /*@ slevel 5; */
-  for (i = 0; i < 5; i++) {
-    res += a[i + 3] + b[i * 2] + c[i + 1];
-    res += subanalyze(&c[i + 1]);
-  }
-  return res;
-}
-
-char garbled_mix = (char) "abc";
-char *s = "abc";
-int another_global = 42;
-//int yet_another_global = 43; // from init_global3.c
-double *pr, *pr2, *pr_escaping, **ppr;
-int *alloc1, *alloc2, *alloc3;
-
-double dmin(double *pd1, double *pd2) {
-  if (*pd1 < *pd2) return *pd1;
-  else return *pd2;
-}
-
-int fun(int k) {
-  return k+1;
-}
-
-typedef int (*i_fp_i)(int);
-i_fp_i fp = &fun;
-
-/*@ assigns a1[..], stuff, pr, pr2, pr_escaping, alloc1, alloc2
-      \from \nothing; */
-void init_inner(int n, char const *tea) {
-  int i;
-  /*@ slevel N3; */
-  for (i = 0; i < N1; i++) {
-    a1[i] = i;
-  }
-  for (i = 0; i < N2; i++) {
-    stuff.t[i] = a1[i/5] + 3;
-  }
-  for (i = 0; i < N3; i++) {
-    stuff.d[i] = 3.125 * i;
-  }
-  /*@ slevel 0; */
-  double r = analyze(a1, stuff.t, stuff.d);
-  double r2 = analyze(a1, stuff.t+1, stuff.d+1);
-  pr = nondet ? &r : &r2;
-  pr2 = &r2;
-  pr_escaping = &r2;
-  alloc1 = malloc(sizeof(int*));
-  *alloc1 = (int) alloc1;
-  alloc2 = malloc(2*sizeof(int));
-  *alloc2 = 37;
-  free(alloc2);
-}
-
-int inited;
-
-/*@ assigns a1[..], stuff, pr, pr2, pr_escaping, alloc1, alloc2, inited
-      \from \nothing; */
-void init_outer() {
-    init_inner(13, "tea");
-    inited = 1;
-}
-
-int main() {
-  init_outer();
-  char *sa = s;
-  Frama_C_dump_each();
-  double r = analyze(a1, stuff.t, stuff.d);
-  double r2 = analyze(a1, stuff.t+1, stuff.d+1);
-  pr = nondet ? &r : &r2;
-  pr2 = nondet ? &r : &r2;
-  ppr = nondet ? &pr : &pr2;
-  double dm = dmin(pr, *ppr);
-  int res_from_fp = (*fp)(31);
-  int res = (int)r % 256;
-  *alloc1 = inited;
-  int local = *alloc1;
-  free(alloc1);
-  alloc3 = malloc(sizeof(int));
-  local = another_global;
-  //int local2 = yet_another_global; // from init_global3.c
-  return 0;
-}

tests/builtins/long_init3.c

-/* run.config*
-   DONTRUN: tests run by Longinit_sequencer.i
-*/
-
-#include <stdlib.h>
-
-#define N1 10
-#define N2 50
-#define N3 10
-
-volatile int nondet;
-
-int a1[N1];
-struct st {
-  unsigned long t[N2];
-  double d[N3];
-} stuff;
-
-double subanalyze(double *d) {
-  return *d < 15 ? 1.0 : *d / 15.0;
-}
-
-double analyze(int *a, unsigned long *b, double *c) {
-  int i;
-  double res = 0.0;
-  /*@ slevel 5; */
-  for (i = 0; i < 5; i++) {
-    res += a[i + 3] + b[i * 2] + c[i + 1];
-    res += subanalyze(&c[i + 1]);
-  }
-  return res;
-}
-
-char garbled_mix = (char) "abc";
-char *s = "abc";
-int another_global = 42;
-int yet_another_global = 43;
-double *pr, *pr2, *pr_escaping, **ppr;
-int *alloc1, *alloc2, *alloc3;
-
-double dmin(double *pd1, double *pd2) {
-  if (*pd1 < *pd2) return *pd1;
-  else return *pd2;
-}
-
-int fun(int k) {
-  return k+1;
-}
-
-typedef int (*i_fp_i)(int);
-i_fp_i fp = &fun;
-
-/*@ assigns a1[..], stuff, pr, pr2, pr_escaping, alloc1, alloc2
-      \from \nothing; */
-void init_inner(int n, char const *tea) {
-  int i;
-  /*@ slevel N3; */
-  for (i = 0; i < N1; i++) {
-    a1[i] = i;
-  }
-  for (i = 0; i < N2; i++) {
-    stuff.t[i] = a1[i/5] + 3;
-  }
-  for (i = 0; i < N3; i++) {
-    stuff.d[i] = 3.125 * i;
-  }
-  /*@ slevel 0; */
-  double r = analyze(a1, stuff.t, stuff.d);
-  double r2 = analyze(a1, stuff.t+1, stuff.d+1);
-  pr = nondet ? &r : &r2;
-  pr2 = &r2;
-  pr_escaping = &r2;
-  alloc1 = malloc(sizeof(int*));
-  *alloc1 = (int) alloc1;
-  alloc2 = malloc(2*sizeof(int));
-  *alloc2 = 37;
-  free(alloc2);
-}
-
-int inited;
-
-/*@ assigns a1[..], stuff, pr, pr2, pr_escaping, alloc1, alloc2, inited
-      \from \nothing; */
-void init_outer() {
-    init_inner(13, "tea");
-    inited = 1;
-}
-
-int main() {
-  init_outer();
-  char *sa = s;
-  Frama_C_dump_each();
-  double r = analyze(a1, stuff.t, stuff.d);
-  double r2 = analyze(a1, stuff.t+1, stuff.d+1);
-  pr = nondet ? &r : &r2;
-  pr2 = nondet ? &r : &r2;
-  ppr = nondet ? &pr : &pr2;
-  double dm = dmin(pr, *ppr);
-  int res_from_fp = (*fp)(31);
-  int res = (int)r % 256;
-  *alloc1 = inited;
-  int local = *alloc1;
-  free(alloc1);
-  alloc3 = malloc(sizeof(int));
-  local = another_global;
-  int local2 = yet_another_global;
-  return 0;
-}

tests/value/diff_bitwise

@@ -24,10 +24,10 @@ diff tests/value/oracle/addition.res.oracle tests/value/oracle_bitwise/addition.
 ---
 >   p10 ∈ {{ garbled mix of &{p1} }}
 diff tests/value/oracle/bitwise.res.oracle tests/value/oracle_bitwise/bitwise.res.oracle
-79c79,82
-< [eva] tests/value/bitwise.i:144: Frama_C_show_each_dead: {0}
+98c98,101
+< [eva] tests/value/bitwise.i:158: Frama_C_show_each_dead: {0}
 ---
-> [eva] tests/value/bitwise.i:142: 
+> [eva] tests/value/bitwise.i:156: 
 >   The evaluation of the expression x & 2
 >   led to bottom without alarms:
 >   at this point the product of states has no possible concretization.
@@ -51,3 +51,4 @@ diff tests/value/oracle/logic_ptr_cast.res.oracle tests/value/oracle_bitwise/log
 <   The imprecision originates from Arithmetic {tests/value/logic_ptr_cast.i:8}
 ---
 > [eva] tests/value/logic_ptr_cast.i:8: Assigning imprecise value to p.
+Only in tests/value/oracle: unit_tests.res.oracle

tests/value/diff_equalities

@@ -121,18 +121,18 @@ diff tests/value/oracle/alias.6.res.oracle tests/value/oracle_equalities/alias.6
 ---
 >   x ∈ {33}
 diff tests/value/oracle/auto_loop_unroll.0.res.oracle tests/value/oracle_equalities/auto_loop_unroll.0.res.oracle
-82c82,85
-< [eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+81c81,84
+< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 ---
 > [eva] computing for function incr <- various_loops <- main.
->   Called from tests/value/auto_loop_unroll.c:103.
+>   Called from tests/value/auto_loop_unroll.c:101.
 > [eva] Recording results for incr
 > [eva] Done for function incr
-91c94,97
-< [eva] tests/value/auto_loop_unroll.c:103: Reusing old results for call to incr
+90c93,96
+< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
 ---
 > [eva] computing for function incr <- various_loops <- main.
->   Called from tests/value/auto_loop_unroll.c:103.
+>   Called from tests/value/auto_loop_unroll.c:101.
 > [eva] Recording results for incr
 > [eva] Done for function incr
 diff tests/value/oracle/backward_add_ptr.res.oracle tests/value/oracle_equalities/backward_add_ptr.res.oracle
@@ -688,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
-188c188
+194c194
 <   q ∈ {{ &x + [-400..400],0%4 }}
 ---
 >   q ∈ {{ &x }}
@@ -867,3 +867,4 @@ diff tests/value/oracle/struct2.res.oracle tests/value/oracle_equalities/struct2
 <            [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0..1];
 ---
 >            [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0];
+Only in tests/value/oracle: unit_tests.res.oracle

tests/value/diff_gauges

@@ -47,20 +47,98 @@ diff tests/value/oracle/auto_loop_unroll.0.res.oracle tests/value/oracle_gauges/
 <   Frama_C_show_each_32_80: [0..2147483647]
 ---
 > [eva] tests/value/auto_loop_unroll.c:82: Frama_C_show_each_32_80: [32..83]
-49,52c32
-< [eva:alarm] tests/value/auto_loop_unroll.c:86: Warning: 
+55,56d37
+< [eva:alarm] tests/value/auto_loop_unroll.c:88: Warning: 
 <   signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:90: 
+58c39
+<   Frama_C_show_each_40_50: [0..2147483647]
+---
+>   Frama_C_show_each_40_50: [40..1073741861]
+133,136c114
+< [eva:alarm] tests/value/auto_loop_unroll.c:120: Warning: 
+<   signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:122: 
+<   Frama_C_show_each_32_64: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:122: Frama_C_show_each_32_64: [32..65]
+185,188c163
+< [eva:alarm] tests/value/auto_loop_unroll.c:173: Warning: 
+<   signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:175: 
+<   Frama_C_show_each_imprecise: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:175: Frama_C_show_each_imprecise: [1..9]
+190,191d164
+< [eva:alarm] tests/value/auto_loop_unroll.c:181: Warning: 
+<   signed overflow. assert res + 1 ≤ 2147483647;
+195c168
+<   Frama_C_show_each_imprecise: [0..2147483647]
+---
+>   Frama_C_show_each_imprecise: [64..2147483647]
+201,203c174
+< [eva:alarm] tests/value/auto_loop_unroll.c:193: Warning: 
+<   signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:195: Frama_C_show_each_11: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:195: Frama_C_show_each_11: {11}
+205,207c176
+< [eva:alarm] tests/value/auto_loop_unroll.c:198: Warning: 
+<   signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:200: Frama_C_show_each_12: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:200: Frama_C_show_each_12: {12}
+209,210d177
+< [eva:alarm] tests/value/auto_loop_unroll.c:204: Warning: 
+<   signed overflow. assert res + 1 ≤ 2147483647;
+212a180,181
+> [eva:alarm] tests/value/auto_loop_unroll.c:204: Warning: 
+>   signed overflow. assert res + 1 ≤ 2147483647;
+216,217d184
+< [eva:alarm] tests/value/auto_loop_unroll.c:209: Warning: 
+<   signed overflow. assert res + 1 ≤ 2147483647;
+219a187,188
+> [eva:alarm] tests/value/auto_loop_unroll.c:209: Warning: 
+>   signed overflow. assert res + 1 ≤ 2147483647;
+223,224d191
+< [eva:alarm] tests/value/auto_loop_unroll.c:217: Warning: 
+<   signed overflow. assert res + 1 ≤ 2147483647;
+228,231c195
+< [eva:alarm] tests/value/auto_loop_unroll.c:222: Warning: 
+<   signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:226: 
 <   Frama_C_show_each_11_111: [0..2147483647]
 ---
-> [eva] tests/value/auto_loop_unroll.c:90: Frama_C_show_each_11_111: [11..111]
-60,61d39
-< [eva:alarm] tests/value/auto_loop_unroll.c:96: Warning: 
+> [eva] tests/value/auto_loop_unroll.c:226: Frama_C_show_each_11_111: [11..111]
+239,241c203
+< [eva:alarm] tests/value/auto_loop_unroll.c:236: Warning: 
 <   signed overflow. assert res + 1 ≤ 2147483647;
-63c41
-<   Frama_C_show_each_40_50: [0..2147483647]
+< [eva] tests/value/auto_loop_unroll.c:238: Frama_C_show_each_20: [0..2147483647]
 ---
->   Frama_C_show_each_40_50: [40..1073741861]
+> [eva] tests/value/auto_loop_unroll.c:238: Frama_C_show_each_20: [20..2147483646]
+243,244d204
+< [eva:alarm] tests/value/auto_loop_unroll.c:241: Warning: 
+<   signed overflow. assert res + 1 ≤ 2147483647;
+247c207,209
+< [eva] tests/value/auto_loop_unroll.c:243: Frama_C_show_each_21: [0..2147483647]
+---
+> [eva:alarm] tests/value/auto_loop_unroll.c:241: Warning: 
+>   signed overflow. assert res + 1 ≤ 2147483647;
+> [eva] tests/value/auto_loop_unroll.c:243: Frama_C_show_each_21: {21}
+253,255c215,216
+< [eva:alarm] tests/value/auto_loop_unroll.c:250: Warning: 
+<   signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:254: Frama_C_show_each_30: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:254: Frama_C_show_each_30: {30}
+> [eva] tests/value/auto_loop_unroll.c:258: starting to merge loop iterations
+258d218
+< [eva] tests/value/auto_loop_unroll.c:258: starting to merge loop iterations
+261,263c221
+< [eva:alarm] tests/value/auto_loop_unroll.c:267: Warning: 
+<   signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:272: Frama_C_show_each_32: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:272: Frama_C_show_each_32: {32}
 diff tests/value/oracle/auto_loop_unroll.1.res.oracle tests/value/oracle_gauges/auto_loop_unroll.1.res.oracle
 15,18c15
 < [eva:alarm] tests/value/auto_loop_unroll.c:31: Warning: 
@@ -76,6 +154,105 @@ diff tests/value/oracle/auto_loop_unroll.1.res.oracle tests/value/oracle_gauges/
 <   Frama_C_show_each_imprecise: [0..2147483647]
 ---
 > [eva] tests/value/auto_loop_unroll.c:41: Frama_C_show_each_imprecise: {100}
+329,332c323
+< [eva:alarm] tests/value/auto_loop_unroll.c:173: Warning: 
+<   signed overflow. assert res + 1 ≤ 2147483647;
+< [eva] tests/value/auto_loop_unroll.c:175: 
+<   Frama_C_show_each_imprecise: [0..2147483647]
+---
+> [eva] tests/value/auto_loop_unroll.c:175: Frama_C_show_each_imprecise: [1..9]
+334,335d324
+< [eva:alarm] tests/value/auto_loop_unroll.c:181: Warning: 
+<   signed overflow. assert res + 1 ≤ 2147483647;
+339c328
+<   Frama_C_show_each_imprecise: [0..2147483647]
+---
+>   Frama_C_show_each_imprecise: [64..2147483647]
+385a375,458
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 200 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 300 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 400 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 500 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 600 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 700 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 800 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 900 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 1000 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 1100 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 1200 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 1300 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 1400 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 1500 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 1600 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 1700 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 1800 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 1900 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 2000 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 2100 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 2200 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 2300 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 2400 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 2500 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 2600 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 2700 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 2800 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 2900 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 3000 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 3100 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 3200 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 3300 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 3400 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 3500 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 3600 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 3700 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 3800 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 3900 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 4000 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 4100 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 4200 states
+> [eva] tests/value/auto_loop_unroll.c:276: 
+>   Trace partitioning superposing up to 4300 states
 diff tests/value/oracle/bad_loop.res.oracle tests/value/oracle_gauges/bad_loop.res.oracle
 6a7
 > [eva] tests/value/bad_loop.i:12: starting to merge loop iterations
@@ -1047,6 +1224,7 @@ diff tests/value/oracle/undefined_sequence.0.res.oracle tests/value/oracle_gauge
 > [eva] tests/value/undefined_sequence.i:43: starting to merge loop iterations
 101a103
 > [eva] tests/value/undefined_sequence.i:49: starting to merge loop iterations
+Only in tests/value/oracle: unit_tests.res.oracle
 diff tests/value/oracle/unroll.res.oracle tests/value/oracle_gauges/unroll.res.oracle
 13,14d12
 < [eva:alarm] tests/value/unroll.i:34: Warning: 

tests/value/diff_octagons

@@ -33,6 +33,20 @@ diff tests/value/oracle/alias.6.res.oracle tests/value/oracle_octagons/alias.6.r
 >   tz1 ∈ {1}
 >   tz2 ∈ {1}
 >   tz3 ∈ {1}
+diff tests/value/oracle/auto_loop_unroll.0.res.oracle tests/value/oracle_octagons/auto_loop_unroll.0.res.oracle
+211,212d210
+< [eva:alarm] tests/value/auto_loop_unroll.c:203: Warning: 
+<   signed overflow. assert -2147483648 ≤ i_0 - 1;
+218,219d215
+< [eva:alarm] tests/value/auto_loop_unroll.c:208: Warning: 
+<   signed overflow. assert -2147483648 ≤ i_1 - 1;
+245,246d240
+< [eva:alarm] tests/value/auto_loop_unroll.c:240: Warning: 
+<   signed overflow. assert -2147483648 ≤ i - 1;
+306c300
+<   i ∈ [-2147483648..20]
+---
+>   i ∈ {-1}
 diff tests/value/oracle/bitfield.res.oracle tests/value/oracle_octagons/bitfield.res.oracle
 138a139,141
 > [eva] tests/value/bitfield.i:71: 
@@ -238,23 +252,23 @@ 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
-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
-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
-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
-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
-154a164
-> [eva:nonlin] tests/value/nonlin.c:113: subdividing on x
-155a166
-> [eva:nonlin] tests/value/nonlin.c:115: subdividing on x
+113a114,115
+> [eva:nonlin] tests/value/nonlin.c:71: non-linear 'x * x', lv 'x'
+> [eva:nonlin] tests/value/nonlin.c:71: subdividing on x
+116a119,121
+> [eva:nonlin] tests/value/nonlin.c:72: subdividing on x
+> [eva:nonlin] tests/value/nonlin.c:72: non-linear 'y * y', lv 'y'
+> [eva:nonlin] tests/value/nonlin.c:72: subdividing on y
+119a125,126
+> [eva:nonlin] tests/value/nonlin.c:74: non-linear 'z * x + x * y', lv 'x'
+> [eva:nonlin] tests/value/nonlin.c:74: subdividing on x
+157a165,166
+> [eva:nonlin] tests/value/nonlin.c:118: non-linear 'x * x', lv 'x'
+> [eva:nonlin] tests/value/nonlin.c:118: subdividing on x
+160a170
+> [eva:nonlin] tests/value/nonlin.c:119: subdividing on x
+161a172
+> [eva:nonlin] tests/value/nonlin.c:121: subdividing on x
 diff tests/value/oracle/plevel.res.oracle tests/value/oracle_octagons/plevel.res.oracle
 12d11
 < [eva] Recording results for main
@@ -386,6 +400,7 @@ diff tests/value/oracle/test.0.res.oracle tests/value/oracle_octagons/test.0.res
 <   j ∈ [-1073741822..1]
 ---
 >   j ∈ {-1; 0; 1}
+Only in tests/value/oracle: unit_tests.res.oracle
 diff tests/value/oracle/unroll.res.oracle tests/value/oracle_octagons/unroll.res.oracle
 22c22
 <   G ∈ [17739..2147483647]

tests/value/diff_symblocs

@@ -326,3 +326,4 @@ diff tests/value/oracle/test.0.res.oracle tests/value/oracle_symblocs/test.0.res
 <   tmp ∈ [--..--] or UNINITIALIZED
 ---
 >   tmp ∈ [-2147483647..2147483647] or UNINITIALIZED
+Only in tests/value/oracle: unit_tests.res.oracle