Merge branch 'feature/eva/nested-widenings' into 'master'

[Eva] Improves widenings on nested loops

Closes Value/Value#122 and Value/Value#123

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

src/plugins/value/engine/basic_partitioning.ml

@@ -182,6 +182,9 @@ struct
     w.previous_state <- `Bottom;
     w.widening_counter <- widening_delay
 
+  let reset_widening_counter (w : widening) : unit =
+    w.widening_counter <- max w.widening_counter (widening_period - 1)
+
   (* Operators *)
 
   let clear_propagation (p : propagation) : unit =

src/plugins/value/engine/legacy_partitioning.ml

@@ -141,6 +141,9 @@ struct
     w.previous_state <- `Bottom;
     w.widening_counter <- widening_delay
 
+  let reset_widening_counter w =
+    w.widening_counter <- max w.widening_counter (widening_period - 1)
+
   (* Operators *)
 
   let clear_propagation (p : propagation) : unit =

src/plugins/value/engine/loop_partitioning.ml

@@ -359,6 +359,12 @@ struct
     in
     Tree.iter reset w.widening_tree
 
+  let reset_widening_counter (w : widening) : unit =
+    let reset w =
+      w.widening_counter <- max w.widening_counter (widening_period - 1)
+    in
+    Tree.iter reset w.widening_tree
+
   (* Operators *)
 
   let clear_propagation (p : propagation) : unit =

src/plugins/value/engine/partitioned_dataflow.ml

@@ -623,9 +623,12 @@ module Make_Dataflow
     | Wto.Node v ->
       ignore (process_vertex v)
     | Wto.Component (v, w) as component ->
-      (* Reset the component if hierachical_convergence is set *)
-      if hierachical_convergence then
-        reset_component (v :: Wto.flatten w);
+      (* Reset the component if hierachical_convergence is set.
+         Otherwise, only resets the widening counter for this component. This
+         is especially useful for nested loops. *)
+      if hierachical_convergence
+      then reset_component (v :: Wto.flatten w)
+      else Partition.reset_widening_counter (get_vertex_widening v);
       (* Iterate until convergence *)
       let iteration_count = ref 0 in
       while

src/plugins/value/engine/state_partitioning.mli

@@ -91,6 +91,12 @@ sig
   val reset_shadow : shadow -> unit
   val reset_widening : widening -> unit
 
+  (** Resets (or just delays) the widening counter. Used on nested loops, to
+      postpone the widening of the inner loop when iterating on the outer
+      loops. This is especially useful when the inner loop fixpoint does not
+      depend on the outer loop. *)
+  val reset_widening_counter : widening -> unit
+
 
   (* --- Partition transfer functions --- *)
 

tests/builtins/diff_apron

@@ -8,27 +8,14 @@ diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_a
 ---
 >   tests/builtins/result_apron/Longinit_sequencer.sav
 diff tests/builtins/oracle/allocated.0.res.oracle tests/builtins/oracle_apron/allocated.0.res.oracle
-243c243
-< [eva] tests/builtins/allocated.c:131: Frama_C_show_each: {0; 1; 2; 3; 4}
----
-> [eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..2147483647]
-250c250
-< [eva] tests/builtins/allocated.c:131: Frama_C_show_each: {0; 1; 2; 3; 4; 5}
----
-> [eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..2147483647]
-257c257
-< [eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..9]
----
-> [eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..2147483647]
-276c276
+260a261,263
+> [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
+> [eva:malloc] tests/builtins/allocated.c:127: 
+>   resizing variable `__malloc_main_l127' (0..31/319) to fit 0..63/319
+273c276
 <   j ∈ [1..2147483647]
 ---
->   j ∈ [1..12]
-282,283c282
-<   __malloc_w_main_l82[0..1] ∈ [7..2147483647] or UNINITIALIZED
-<                      [2] ∈ [7..27] or UNINITIALIZED
----
->   __malloc_w_main_l82[0..2] ∈ [7..27] or UNINITIALIZED
+>   j ∈ [1..10]
 diff tests/builtins/oracle/memexec-malloc.res.oracle tests/builtins/oracle_apron/memexec-malloc.res.oracle
 20c20,23
 < [eva] tests/builtins/memexec-malloc.c:25: Reusing old results for call to f

tests/builtins/oracle/allocated.0.res.oracle

@@ -233,34 +233,31 @@
 [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
 [eva:malloc] tests/builtins/allocated.c:127: 
   resizing variable `__malloc_main_l127' (0..31/95) to fit 0..63/127
-[eva] tests/builtins/allocated.c:131: Frama_C_show_each: {0; 1; 2; 3}
+[eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..2147483647]
 [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
 [eva:malloc] tests/builtins/allocated.c:127: 
   strong free on bases: {__malloc_main_l127}
 [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
 [eva:malloc] tests/builtins/allocated.c:127: 
   resizing variable `__malloc_main_l127' (0..31/127) to fit 0..63/159
-[eva] tests/builtins/allocated.c:131: Frama_C_show_each: {0; 1; 2; 3; 4}
+[eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..2147483647]
 [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
 [eva:malloc] tests/builtins/allocated.c:127: 
   strong free on bases: {__malloc_main_l127}
 [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
 [eva:malloc] tests/builtins/allocated.c:127: 
   resizing variable `__malloc_main_l127' (0..31/159) to fit 0..63/191
-[eva] tests/builtins/allocated.c:131: Frama_C_show_each: {0; 1; 2; 3; 4; 5}
+[eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..2147483647]
 [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
 [eva:malloc] tests/builtins/allocated.c:127: 
   strong free on bases: {__malloc_main_l127}
 [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
 [eva:malloc] tests/builtins/allocated.c:127: 
   resizing variable `__malloc_main_l127' (0..31/191) to fit 0..63/319
-[eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..9]
+[eva] tests/builtins/allocated.c:131: Frama_C_show_each: [0..2147483647]
 [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_free
 [eva:malloc] tests/builtins/allocated.c:127: 
   strong free on bases: {__malloc_main_l127}
-[eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc
-[eva:malloc] tests/builtins/allocated.c:127: 
-  resizing variable `__malloc_main_l127' (0..31/319) to fit 0..63/319
 [eva] Recording results for main
 [eva] done for function main
 [eva] tests/builtins/allocated.c:27: 

tests/idct/diff_equalities

 diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_equalities/ieee_1180_1990.res.oracle
-331a332,333
+355a356,357
 > [eva] tests/idct/ieee_1180_1990.c:219: Warning: 
 >   2's complement assumed for overflow
-335a338,339
+359a362,363
 > [eva] tests/idct/ieee_1180_1990.c:220: Warning: 
 >   2's complement assumed for overflow
-341,342d344
+365,366d368
 < [eva] tests/idct/ieee_1180_1990.c:219: Warning: 
 <   2's complement assumed for overflow
-365a368,369
+391a394,395
 > [eva] tests/idct/ieee_1180_1990.c:243: Warning: 
 >   2's complement assumed for overflow
-369a374,375
+395a400,401
 > [eva] tests/idct/ieee_1180_1990.c:244: Warning: 
 >   2's complement assumed for overflow
-375,376d380
+401,402d406
 < [eva] tests/idct/ieee_1180_1990.c:243: Warning: 
 <   2's complement assumed for overflow
-397a402,405
+423a428,435
 > [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
-410a419,420
+> [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
+436a449,450
 > [eva] tests/idct/ieee_1180_1990.c:265: Warning: 
 >   2's complement assumed for overflow
-414a425,426
+440a455,456
 > [eva] tests/idct/ieee_1180_1990.c:266: Warning: 
 >   2's complement assumed for overflow
-420,421d431
+446,447d461
 < [eva] tests/idct/ieee_1180_1990.c:265: Warning: 
 <   2's complement assumed for overflow
-437a448,449
+465a480,481
 > [eva] tests/idct/ieee_1180_1990.c:289: Warning: 
 >   2's complement assumed for overflow
-441a454,455
+469a486,487
 > [eva] tests/idct/ieee_1180_1990.c:290: Warning: 
 >   2's complement assumed for overflow
-447,448d460
+475,476d492
 < [eva] tests/idct/ieee_1180_1990.c:289: Warning: 
 <   2's complement assumed for overflow
-469a482,485
+497a514,521
 > [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
-482a499,500
+> [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
+510a535,536
 > [eva] tests/idct/ieee_1180_1990.c:311: Warning: 
 >   2's complement assumed for overflow
-486a505,506
+514a541,542
 > [eva] tests/idct/ieee_1180_1990.c:312: Warning: 
 >   2's complement assumed for overflow
-492,493d511
+520,521d547
 < [eva] tests/idct/ieee_1180_1990.c:311: Warning: 
 <   2's complement assumed for overflow
-509a528,529
+539a566,567
 > [eva] tests/idct/ieee_1180_1990.c:335: Warning: 
 >   2's complement assumed for overflow
-513a534,535
+543a572,573
 > [eva] tests/idct/ieee_1180_1990.c:336: Warning: 
 >   2's complement assumed for overflow
-519,520d540
+549,550d578
 < [eva] tests/idct/ieee_1180_1990.c:335: Warning: 
 <   2's complement assumed for overflow
-540a561,564
+570a599,606
+> [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
-548a573,578
+> [eva] tests/idct/ieee_1180_1990.c:85: 
+>   Reusing old results for call to IEEE_1180_1990_rand
+578a615,632
 > [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
-550a581,582
+> [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
-552a585,590
+> [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
-574a613,618
+580a635,636
+> [eva] tests/idct/ieee_1180_1990.c:100: 
+>   Call to builtin Frama_C_sqrt for function sqrt
+582a639,640
+> [eva] tests/idct/ieee_1180_1990.c:100: 
+>   Call to builtin Frama_C_sqrt for function sqrt
+604a663,676
 > [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
-576a621,622
-> [eva] tests/idct/ieee_1180_1990.c:140: 
->   Call to builtin Frama_C_sqrt for function sqrt
-578a625,630
+> [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
-620a673,676
-> [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
-650a707,710
-> [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
-680a741,744
-> [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
-688a753,754
-> [eva] tests/idct/ieee_1180_1990.c:100: 
->   Call to builtin Frama_C_sqrt for function sqrt
-690a757,762
-> [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: 
+606a679,680
+> [eva] tests/idct/ieee_1180_1990.c:140: 
 >   Call to builtin Frama_C_sqrt for function sqrt
-692a765,770
-> [eva] tests/idct/ieee_1180_1990.c:100: 
+608a683,688
+> [eva] tests/idct/ieee_1180_1990.c:140: 
 >   Call to builtin Frama_C_sqrt for function sqrt
-> [eva] tests/idct/ieee_1180_1990.c:101: 
+> [eva] tests/idct/ieee_1180_1990.c:141: 
 >   Call to builtin Frama_C_cos for function cos
-> [eva] tests/idct/ieee_1180_1990.c:100: 
+> [eva] tests/idct/ieee_1180_1990.c:140: 
 >   Call to builtin Frama_C_sqrt for function sqrt

tests/idct/diff_gauges

 diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_gauges/ieee_1180_1990.res.oracle
-51a52,55
-> [eva] tests/idct/idct.c:90: Call to builtin Frama_C_sqrt for function sqrt
-> [eva] tests/idct/idct.c:91: Call to builtin Frama_C_cos for function cos
-> [eva] tests/idct/idct.c:90: Call to builtin Frama_C_sqrt for function sqrt
-> [eva] tests/idct/idct.c:91: Call to builtin Frama_C_cos for function cos
-150a155,158
-> [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
-198a207,214
+578a579,580
 > [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
-280a297,304
-> [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
-548a573,574
-> [eva] tests/idct/ieee_1180_1990.c:100: 
->   Call to builtin Frama_C_sqrt for function sqrt
-574a601,602
+604a607,608
 > [eva] tests/idct/ieee_1180_1990.c:140: 
 >   Call to builtin Frama_C_sqrt for function sqrt
-688a717,718
-> [eva] tests/idct/ieee_1180_1990.c:100: 
->   Call to builtin Frama_C_sqrt for function sqrt
-891a922,950
-> [eva] tests/idct/ieee_1180_1990.c:236: 
->   Reusing old results for call to IEEE_1180_1990_dctf
-> [eva] tests/idct/ieee_1180_1990.c:237: 
->   Reusing old results for call to IEEE_1180_1990_idctf
-> [eva] tests/idct/ieee_1180_1990.c:238: Reusing old results for call to idct
-> [eva] tests/idct/ieee_1180_1990.c:257: 
->   Reusing old results for call to IEEE_1180_1990_mkbk
-> [eva] tests/idct/ieee_1180_1990.c:258: 
->   Reusing old results for call to IEEE_1180_1990_dctf
-> [eva] tests/idct/ieee_1180_1990.c:259: 
->   Reusing old results for call to IEEE_1180_1990_idctf
-> [eva] tests/idct/ieee_1180_1990.c:260: Reusing old results for call to idct
-> [eva] tests/idct/ieee_1180_1990.c:282: 
->   Reusing old results for call to IEEE_1180_1990_dctf
-> [eva] tests/idct/ieee_1180_1990.c:283: 
->   Reusing old results for call to IEEE_1180_1990_idctf
-> [eva] tests/idct/ieee_1180_1990.c:284: Reusing old results for call to idct
-> [eva] tests/idct/ieee_1180_1990.c:303: 
->   Reusing old results for call to IEEE_1180_1990_mkbk
-> [eva] tests/idct/ieee_1180_1990.c:304: 
->   Reusing old results for call to IEEE_1180_1990_dctf
-> [eva] tests/idct/ieee_1180_1990.c:305: 
->   Reusing old results for call to IEEE_1180_1990_idctf
-> [eva] tests/idct/ieee_1180_1990.c:306: Reusing old results for call to idct
-> [eva] tests/idct/ieee_1180_1990.c:328: 
->   Reusing old results for call to IEEE_1180_1990_dctf
-> [eva] tests/idct/ieee_1180_1990.c:329: 
->   Reusing old results for call to IEEE_1180_1990_idctf
-> [eva] tests/idct/ieee_1180_1990.c:330: Reusing old results for call to idct

tests/idct/oracle/ieee_1180_1990.res.oracle

@@ -49,6 +49,10 @@
 [eva] tests/idct/idct.c:91: Call to builtin Frama_C_cos for function cos
 [eva] tests/idct/idct.c:90: Call to builtin Frama_C_sqrt for function sqrt
 [eva] tests/idct/idct.c:91: Call to builtin Frama_C_cos for function cos
+[eva] tests/idct/idct.c:90: Call to builtin Frama_C_sqrt for function sqrt
+[eva] tests/idct/idct.c:91: Call to builtin Frama_C_cos for function cos
+[eva] tests/idct/idct.c:90: Call to builtin Frama_C_sqrt for function sqrt
+[eva] tests/idct/idct.c:91: Call to builtin Frama_C_cos for function cos
 [eva] tests/idct/idct.c:128: starting to merge loop iterations
 [eva] tests/idct/idct.c:126: starting to merge loop iterations
 [eva:alarm] tests/idct/idct.c:129: Warning: 
@@ -148,6 +152,10 @@
   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
 [eva] Recording results for IEEE_1180_1990_mkbk
 [eva] Done for function IEEE_1180_1990_mkbk
 [eva] computing for function IEEE_1180_1990_dctf <- main.
@@ -196,6 +204,14 @@
   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:108: starting to merge loop iterations
 [eva] tests/idct/ieee_1180_1990.c:105: starting to merge loop iterations
 [eva:alarm] tests/idct/ieee_1180_1990.c:109: Warning: 
@@ -278,6 +294,14 @@
   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
+[eva] tests/idct/ieee_1180_1990.c:141: 
+  Call to builtin Frama_C_cos for function cos
 [eva:alarm] tests/idct/ieee_1180_1990.c:150: Warning: 
   accessing uninitialized left-value. assert \initialized(&(*(m1 + k))[j]);
 [eva] tests/idct/ieee_1180_1990.c:149: starting to merge loop iterations
@@ -345,6 +369,8 @@
 [eva] tests/idct/ieee_1180_1990.c:215: starting to merge loop iterations
 [eva] tests/idct/ieee_1180_1990.c:234: starting to merge loop iterations
 [eva] tests/idct/ieee_1180_1990.c:233: starting to merge loop iterations
+[eva] tests/idct/ieee_1180_1990.c:235: Warning: 
+  2's complement assumed for overflow
 [eva] computing for function IEEE_1180_1990_dctf <- main.
   Called from tests/idct/ieee_1180_1990.c:236.
 [eva] Recording results for IEEE_1180_1990_dctf
@@ -422,6 +448,8 @@
 [eva] tests/idct/ieee_1180_1990.c:277: Warning: 
   2's complement assumed for overflow
 [eva] tests/idct/ieee_1180_1990.c:261: starting to merge loop iterations
+[eva] tests/idct/ieee_1180_1990.c:281: Warning: 
+  2's complement assumed for overflow
 [eva] tests/idct/ieee_1180_1990.c:280: starting to merge loop iterations
 [eva] tests/idct/ieee_1180_1990.c:279: starting to merge loop iterations
 [eva] tests/idct/ieee_1180_1990.c:282: 
@@ -494,6 +522,8 @@
 [eva] tests/idct/ieee_1180_1990.c:323: Warning: 
   2's complement assumed for overflow
 [eva] tests/idct/ieee_1180_1990.c:307: starting to merge loop iterations
+[eva] tests/idct/ieee_1180_1990.c:327: Warning: 
+  2's complement assumed for overflow
 [eva] tests/idct/ieee_1180_1990.c:326: starting to merge loop iterations
 [eva] tests/idct/ieee_1180_1990.c:325: starting to merge loop iterations
 [eva] tests/idct/ieee_1180_1990.c:328: 
@@ -593,119 +623,39 @@
 [eva] Recording results for IEEE_1180_1990_idctf
 [eva] Done for function IEEE_1180_1990_idctf
 [eva] tests/idct/ieee_1180_1990.c:214: Reusing old results for call to idct
-[eva] tests/idct/ieee_1180_1990.c:235: Warning: 
-  2's complement assumed for overflow
-[eva] computing for function IEEE_1180_1990_dctf <- main.
-  Called from tests/idct/ieee_1180_1990.c:236.
-[eva] Recording results for IEEE_1180_1990_dctf
-[eva] Done for function IEEE_1180_1990_dctf
+[eva] tests/idct/ieee_1180_1990.c:236: 
+  Reusing old results for call to IEEE_1180_1990_dctf
 [eva] tests/idct/ieee_1180_1990.c:237: 
   Reusing old results for call to IEEE_1180_1990_idctf
 [eva] tests/idct/ieee_1180_1990.c:238: Reusing old results for call to idct
-[eva] computing for function IEEE_1180_1990_mkbk <- main.
-  Called from tests/idct/ieee_1180_1990.c:257.
-[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
-[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] Recording results for IEEE_1180_1990_mkbk
-[eva] Done for function IEEE_1180_1990_mkbk
+[eva] tests/idct/ieee_1180_1990.c:257: 
+  Reusing old results for call to IEEE_1180_1990_mkbk
 [eva] tests/idct/ieee_1180_1990.c:258: 
   Reusing old results for call to IEEE_1180_1990_dctf
 [eva] tests/idct/ieee_1180_1990.c:259: 
   Reusing old results for call to IEEE_1180_1990_idctf
 [eva] tests/idct/ieee_1180_1990.c:260: Reusing old results for call to idct
-[eva] tests/idct/ieee_1180_1990.c:281: Warning: 
-  2's complement assumed for overflow
 [eva] tests/idct/ieee_1180_1990.c:282: 
   Reusing old results for call to IEEE_1180_1990_dctf
 [eva] tests/idct/ieee_1180_1990.c:283: 
   Reusing old results for call to IEEE_1180_1990_idctf
 [eva] tests/idct/ieee_1180_1990.c:284: Reusing old results for call to idct
-[eva] computing for function IEEE_1180_1990_mkbk <- main.
-  Called from tests/idct/ieee_1180_1990.c:303.
-[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
-[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] Recording results for IEEE_1180_1990_mkbk
-[eva] Done for function IEEE_1180_1990_mkbk
+[eva] tests/idct/ieee_1180_1990.c:303: 
+  Reusing old results for call to IEEE_1180_1990_mkbk
 [eva] tests/idct/ieee_1180_1990.c:304: 
   Reusing old results for call to IEEE_1180_1990_dctf
 [eva] tests/idct/ieee_1180_1990.c:305: 
   Reusing old results for call to IEEE_1180_1990_idctf
 [eva] tests/idct/ieee_1180_1990.c:306: Reusing old results for call to idct
-[eva] tests/idct/ieee_1180_1990.c:327: Warning: 
-  2's complement assumed for overflow
 [eva] tests/idct/ieee_1180_1990.c:328: 
   Reusing old results for call to IEEE_1180_1990_dctf
 [eva] tests/idct/ieee_1180_1990.c:329: 
   Reusing old results for call to IEEE_1180_1990_idctf
 [eva] tests/idct/ieee_1180_1990.c:330: Reusing old results for call to idct
-[eva] computing for function IEEE_1180_1990_mkbk <- main.
-  Called from tests/idct/ieee_1180_1990.c:211.
-[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
-[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] Recording results for IEEE_1180_1990_mkbk
-[eva] Done for function IEEE_1180_1990_mkbk
-[eva] computing for function IEEE_1180_1990_dctf <- main.
-  Called from tests/idct/ieee_1180_1990.c:212.
-[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:101: 
-  Call to builtin Frama_C_cos for function cos
-[eva] tests/idct/ieee_1180_1990.c:101: 
-  Call to builtin Frama_C_cos for function cos
-[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
-[eva] tests/idct/ieee_1180_1990.c:101: 
-  Call to builtin Frama_C_cos for function cos
-[eva] Recording results for IEEE_1180_1990_dctf
-[eva] Done for function IEEE_1180_1990_dctf
+[eva] tests/idct/ieee_1180_1990.c:211: 
+  Reusing old results for call to IEEE_1180_1990_mkbk
+[eva] tests/idct/ieee_1180_1990.c:212: 
+  Reusing old results for call to IEEE_1180_1990_dctf
 [eva] tests/idct/ieee_1180_1990.c:213: 
   Reusing old results for call to IEEE_1180_1990_idctf
 [eva] tests/idct/ieee_1180_1990.c:214: Reusing old results for call to idct
@@ -889,6 +839,35 @@
 [eva] tests/idct/ieee_1180_1990.c:213: 
   Reusing old results for call to IEEE_1180_1990_idctf
 [eva] tests/idct/ieee_1180_1990.c:214: Reusing old results for call to idct
+[eva] tests/idct/ieee_1180_1990.c:236: 
+  Reusing old results for call to IEEE_1180_1990_dctf
+[eva] tests/idct/ieee_1180_1990.c:237: 
+  Reusing old results for call to IEEE_1180_1990_idctf
+[eva] tests/idct/ieee_1180_1990.c:238: Reusing old results for call to idct
+[eva] tests/idct/ieee_1180_1990.c:257: 
+  Reusing old results for call to IEEE_1180_1990_mkbk
+[eva] tests/idct/ieee_1180_1990.c:258: 
+  Reusing old results for call to IEEE_1180_1990_dctf
+[eva] tests/idct/ieee_1180_1990.c:259: 
+  Reusing old results for call to IEEE_1180_1990_idctf
+[eva] tests/idct/ieee_1180_1990.c:260: Reusing old results for call to idct
+[eva] tests/idct/ieee_1180_1990.c:282: 
+  Reusing old results for call to IEEE_1180_1990_dctf
+[eva] tests/idct/ieee_1180_1990.c:283: 
+  Reusing old results for call to IEEE_1180_1990_idctf
+[eva] tests/idct/ieee_1180_1990.c:284: Reusing old results for call to idct
+[eva] tests/idct/ieee_1180_1990.c:303: 
+  Reusing old results for call to IEEE_1180_1990_mkbk
+[eva] tests/idct/ieee_1180_1990.c:304: 
+  Reusing old results for call to IEEE_1180_1990_dctf
+[eva] tests/idct/ieee_1180_1990.c:305: 
+  Reusing old results for call to IEEE_1180_1990_idctf
+[eva] tests/idct/ieee_1180_1990.c:306: Reusing old results for call to idct
+[eva] tests/idct/ieee_1180_1990.c:328: 
+  Reusing old results for call to IEEE_1180_1990_dctf
+[eva] tests/idct/ieee_1180_1990.c:329: 
+  Reusing old results for call to IEEE_1180_1990_idctf
+[eva] tests/idct/ieee_1180_1990.c:330: Reusing old results for call to idct
 [eva:alarm] tests/idct/ieee_1180_1990.c:357: Warning: 
   accessing uninitialized left-value. assert \initialized(&res[i].pmse[j][k]);
 [eva:alarm] tests/idct/ieee_1180_1990.c:368: Warning: 

tests/misc/oracle/widen_hints.3.res.oracle

@@ -74,23 +74,23 @@
 [eva:final-states] Values at end of function f:
   m ∈ {10}
   n ∈ {43}
-  t[0..87] ∈ {1} or UNINITIALIZED
-   [88..99] ∈ UNINITIALIZED
+  t[0..85] ∈ {1} or UNINITIALIZED
+   [86..99] ∈ UNINITIALIZED
   __retres ∈ {0}
 [eva:final-states] Values at end of function using_dynamic_global:
   b ∈ [0..88]
 [eva:final-states] Values at end of function main:
   m ∈ {10}
   n ∈ {43}
-  ss.i ∈ {87; 88}
+  ss.i ∈ {87}
     .d ∈ UNINITIALIZED
-  ip ∈ {87; 88}
+  ip ∈ {87}
   p ∈ {{ &ip }}
-  ip2 ∈ {87; 88}
+  ip2 ∈ {87}
   p2 ∈ {{ &ip2 }}
   pp ∈ {{ &p2 }}
   iarray[0] ∈ {0}
-        [1].i ∈ {87; 88}
+        [1].i ∈ {87}
   piarray[0] ∈ {{ &iarray[0] }}
          [1] ∈ {{ &iarray[1] }}
   outer_i ∈ {87}

tests/misc/oracle/widen_hints2.0.res.oracle

@@ -62,26 +62,25 @@
   Called from tests/misc/widen_hints2.c:86.
 [eva] tests/misc/widen_hints2.c:34: starting to merge loop iterations
 [eva] tests/misc/widen_hints2.c:35: starting to merge loop iterations
-[eva:alarm] tests/misc/widen_hints2.c:36: Warning: 
-  accessing out of bounds index. assert kk < 100;
 [eva] Recording results for g
 [eva] Done for function g
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function f:
-  tf[0..87] ∈ {1} or UNINITIALIZED
-    [88..99] ∈ UNINITIALIZED
+  tf[0..85] ∈ {1} or UNINITIALIZED
+    [86..99] ∈ UNINITIALIZED
   m ∈ {10}
   n ∈ {43}
 [eva:final-states] Values at end of function g:
-  tg[0..99] ∈ {1} or UNINITIALIZED
+  tg[0..85] ∈ {1} or UNINITIALIZED
+    [86..99] ∈ UNINITIALIZED
   m ∈ {10}
   n ∈ {43}
 [eva:final-states] Values at end of function main:
-  t[0..87] ∈ {0; 1}
-   [88..99] ∈ {0}
-  glob ∈ [87..2147483647]
+  t[0..85] ∈ {0; 1}
+   [86..99] ∈ {0}
+  glob ∈ {87; 88}
   m ∈ {10}
   n ∈ {43}
   __retres ∈ {0}
@@ -98,19 +97,19 @@
 [from] Function g:
   NO EFFECTS
 [from] Function main:
-  t[0..87] FROM \nothing (and SELF)
+  t[0..85] FROM \nothing (and SELF)
   glob FROM \nothing
   \result FROM \nothing
 [from] ====== END OF DEPENDENCIES ======
 [inout] Out (internal) for function f:
-    tf[0..87]; m; n; a; b
+    tf[0..85]; m; n; a; b
 [inout] Inputs for function f:
     \nothing
 [inout] Out (internal) for function g:
-    tg[0..99]; m; n; ll; kk
+    tg[0..85]; m; n; ll; kk
 [inout] Inputs for function g:
     \nothing
 [inout] Out (internal) for function main:
-    t[0..87]; glob; m; n; a; b; c; d; c_0; d_0; j; __retres
+    t[0..85]; glob; m; n; a; b; c; d; c_0; d_0; j; __retres
 [inout] Inputs for function main:
     glob

tests/value/diff_apron

@@ -265,91 +265,80 @@ diff tests/value/oracle/fun_ptr.1.res.oracle tests/value/oracle_apron/fun_ptr.1.
 > [eva] Recording results for f
 > [eva] Done for function f
 diff tests/value/oracle/gauges.res.oracle tests/value/oracle_apron/gauges.res.oracle
-32,35d31
-< [eva] tests/value/gauges.c:19: Frama_C_show_each_0: {{ "in" }}
-< [eva] tests/value/gauges.c:21: Frama_C_show_each_1: {{ "in" }}
+38,39d37
 < [eva:alarm] tests/value/gauges.c:26: Warning: 
 <   signed overflow. assert l + 1 ≤ 2147483647;
-60,63d55
-< [eva] tests/value/gauges.c:41: Frama_C_show_each_0: {{ "in" }}
-< [eva] tests/value/gauges.c:43: Frama_C_show_each_1: {{ "in" }}
+70,71d67
 < [eva:alarm] tests/value/gauges.c:48: Warning: 
 <   signed overflow. assert l + 1 ≤ 2147483647;
-104a97,99
-> [eva] tests/value/gauges.c:83: Frama_C_show_each: {{ "outer" }}
-> [eva] tests/value/gauges.c:78: starting to merge loop iterations
-> [eva] tests/value/gauges.c:80: Frama_C_show_each: {{ "inner" }}
-110,114d104
-< [eva] tests/value/gauges.c:78: starting to merge loop iterations
-< [eva] tests/value/gauges.c:80: Frama_C_show_each: {{ "inner" }}
-< [eva] tests/value/gauges.c:83: Frama_C_show_each: {{ "outer" }}
-< [eva] tests/value/gauges.c:80: Frama_C_show_each: {{ "inner" }}
-< [eva] tests/value/gauges.c:83: Frama_C_show_each: {{ "outer" }}
-117c107
+113,114d108
+< [eva:alarm] tests/value/gauges.c:81: Warning: 
+<   signed overflow. assert k + 1 ≤ 2147483647;
+116,117d109
+< [eva:alarm] tests/value/gauges.c:84: Warning: 
+<   signed overflow. assert k + 1 ≤ 2147483647;
+123a116,117
+> [eva:alarm] tests/value/gauges.c:81: Warning: 
+>   signed overflow. assert k + 1 ≤ 2147483647;
+125c119,121
 < [eva] tests/value/gauges.c:86: Frama_C_show_each: [0..2147483647]
 ---
+> [eva:alarm] tests/value/gauges.c:84: Warning: 
+>   signed overflow. assert k + 1 ≤ 2147483647;
 > [eva] tests/value/gauges.c:86: Frama_C_show_each: [15..2147483647]
-131,132d120
+139,140d134
 < [eva:alarm] tests/value/gauges.c:99: Warning: 
 <   signed overflow. assert c + 1 ≤ 2147483647;
-179,180d166
+187,188d180
 < [eva:alarm] tests/value/gauges.c:140: Warning: 
 <   signed overflow. assert j + 1 ≤ 2147483647;
-291,292d276
+299,300d290
 < [eva:alarm] tests/value/gauges.c:220: Warning: 
 <   signed overflow. assert -2147483648 ≤ n - 1;
-307,308d290
+315,316d304
 < [eva:alarm] tests/value/gauges.c:240: Warning: 
 <   signed overflow. assert j + 1 ≤ 2147483647;
-310c292
+318c306
 <   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]
-316,317d297
+324,325d311
 < [eva:alarm] tests/value/gauges.c:251: Warning: 
 <   signed overflow. assert j + 1 ≤ 2147483647;
-319c299
+327c313
 <   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]
-325,326d304
+333,334d318
 < [eva:alarm] tests/value/gauges.c:263: Warning: 
 <   signed overflow. assert j + 1 ≤ 2147483647;
-328c306
+336c320
 <   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]
-334,335d311
+342,343d325
 < [eva:alarm] tests/value/gauges.c:274: Warning: 
 <   signed overflow. assert j + 1 ≤ 2147483647;
-337c313
+345c327
 <   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]
-345,346d320
+353,354d334
 < [eva:alarm] tests/value/gauges.c:293: Warning: 
 <   signed overflow. assert j + 1 ≤ 2147483647;
-348c322
+356c336
 <   Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..2147483647]
 ---
 >   Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..598]
-716c690
-<   l ∈ [4..2147483647]
----
->   l ∈ [4..101]
-721c695
-<   l ∈ [4..2147483647]
----
->   l ∈ [4..101]
-772c746
+780c760
 <   n ∈ [-2147483648..99]
 ---
 >   n ∈ [-2147483547..99]
-775c749
+783c763
 <   i ∈ [0..2147483647]
 ---
 >   i ∈ [10..2147483647]
-811c785
+819c799
 <   i ∈ [0..2147483647]
 ---
 >   i ∈ [0..21]
@@ -748,7 +737,9 @@ diff tests/value/oracle/precise_locations.res.oracle tests/value/oracle_apron/pr
 >   Called from tests/value/precise_locations.i:39.
 > [eva] Recording results for ct
 > [eva] Done for function ct
-37,40c49,64
+37,42c49,72
+< [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
+< [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
 < [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
 < [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
 < [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
@@ -770,14 +761,17 @@ diff tests/value/oracle/precise_locations.res.oracle tests/value/oracle_apron/pr
 >   Called from tests/value/precise_locations.i:39.
 > [eva] Recording results for ct
 > [eva] Done for function ct
-193,198d216
-< [eva] Done for function f
-< [eva] computing for function g <- main.
-<   Called from tests/value/precise_locations.i:49.
-< [eva] Done for function g
-< [eva] computing for function f <- main.
-<   Called from tests/value/precise_locations.i:48.
-518,525c536,567
+> [eva] computing for function ct <- main.
+>   Called from tests/value/precise_locations.i:39.
+> [eva] Recording results for ct
+> [eva] Done for function ct
+> [eva] computing for function ct <- main.
+>   Called from tests/value/precise_locations.i:39.
+> [eva] Recording results for ct
+> [eva] Done for function ct
+520,529c550,589
+< [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
+< [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
 < [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
 < [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
 < [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
@@ -819,13 +813,14 @@ diff tests/value/oracle/precise_locations.res.oracle tests/value/oracle_apron/pr
 >   Called from tests/value/precise_locations.i:39.
 > [eva] Recording results for ct
 > [eva] Done for function ct
-736,741d777
-< [eva] computing for function f <- main.
-<   Called from tests/value/precise_locations.i:48.
-< [eva] Done for function f
-< [eva] computing for function g <- main.
-<   Called from tests/value/precise_locations.i:49.
-< [eva] Done for function g
+> [eva] computing for function ct <- main.
+>   Called from tests/value/precise_locations.i:39.
+> [eva] Recording results for ct
+> [eva] Done for function ct
+> [eva] computing for function ct <- main.
+>   Called from tests/value/precise_locations.i:39.
+> [eva] Recording results for ct
+> [eva] Done for function ct
 diff tests/value/oracle/precond.res.oracle tests/value/oracle_apron/precond.res.oracle
 49a50,51
 > [eva] computing for function f <- main.
@@ -977,39 +972,6 @@ diff tests/value/oracle/unroll_simple.res.oracle tests/value/oracle_apron/unroll
 <   j ∈ [-2147483648..-126]
 ---
 >   j ∈ {-250}
-diff tests/value/oracle/widen_non_constant.res.oracle tests/value/oracle_apron/widen_non_constant.res.oracle
-25c25
-<   Frama_C_show_each_in: {0; 1; 2}, [1..23]
----
->   Frama_C_show_each_in: [0..22], [1..23]
-27,28d26
-< [eva] tests/value/widen_non_constant.i:13: 
-<   Frama_C_show_each_in: [0..23], [1..23]
-44c42
-<   Frama_C_show_each_in: {0; 1; 2}, [1..23]
----
->   Frama_C_show_each_in: [0..22], [1..23]
-46,47d43
-< [eva] tests/value/widen_non_constant.i:29: 
-<   Frama_C_show_each_in: [0..25], [1..23]
-63c59
-<   Frama_C_show_each_in: {0; 1; 2}, [1..23]
----
->   Frama_C_show_each_in: [0..22], [1..23]
-65,70d60
-< [eva] tests/value/widen_non_constant.i:48: 
-<   Frama_C_show_each_in: [0..2147483647], [1..23]
-< [eva:alarm] tests/value/widen_non_constant.i:49: Warning: 
-<   out of bounds read. assert \valid_read(p + j);
-< [eva:alarm] tests/value/widen_non_constant.i:45: Warning: 
-<   signed overflow. assert j + 1 ≤ 2147483647;
-91c81
-<   j ∈ {23; 24; 25; 26}
----
->   j ∈ {23; 24; 25}
-diff tests/value/oracle/widen_on_non_monotonic.res.oracle tests/value/oracle_apron/widen_on_non_monotonic.res.oracle
-22a23
-> [eva] tests/value/widen_on_non_monotonic.i:26: starting to merge loop iterations
 diff tests/value/oracle/with_comment.res.oracle tests/value/oracle_apron/with_comment.res.oracle
 9,10d8
 < [eva:alarm] tests/value/with_comment.i:21: Warning: 

tests/value/diff_gauges

@@ -38,10 +38,6 @@ diff tests/value/oracle/for_loops.2.res.oracle tests/value/oracle_gauges/for_loo
 < [eva] tests/value/for_loops.c:43: Frama_C_show_each: [0..2147483647]
 ---
 > [eva] tests/value/for_loops.c:43: Frama_C_show_each: [0..1000]
-diff tests/value/oracle/for_loops.3.res.oracle tests/value/oracle_gauges/for_loops.3.res.oracle
-11a12,13
->   Frama_C_show_each_F: {0; 1; 2}, [0..2147483647]
-> [eva] tests/value/for_loops.c:55: 
 diff tests/value/oracle/from_termin.res.oracle tests/value/oracle_gauges/from_termin.res.oracle
 9a10
 > [eva] tests/value/from_termin.i:8: starting to merge loop iterations
@@ -49,41 +45,41 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.o
 25,26d24
 < [eva:alarm] tests/value/gauges.c:23: Warning: 
 <   signed overflow. assert -2147483648 ≤ j - 4;
-34,35d31
+38,39d35
 < [eva:alarm] tests/value/gauges.c:26: Warning: 
 <   signed overflow. assert l + 1 ≤ 2147483647;
-53,54d48
+57,58d52
 < [eva:alarm] tests/value/gauges.c:45: Warning: 
 <   signed overflow. assert -2147483648 ≤ j - 4;
-57a52,53
+61a56,57
 > [eva:alarm] tests/value/gauges.c:45: Warning: 
 >   signed overflow. assert -2147483648 ≤ j - 4;
-62,63d57
+70,71d65
 < [eva:alarm] tests/value/gauges.c:48: Warning: 
 <   signed overflow. assert l + 1 ≤ 2147483647;
-75,76d68
+83,84d76
 < [eva:alarm] tests/value/gauges.c:58: Warning: 
 <   accessing out of bounds index. assert j < 38;
-89,93d80
+97,101d88
 < [eva:alarm] tests/value/gauges.c:71: Warning: 
 <   out of bounds write. assert \valid(tmp);
 <                        (tmp from p++)
 < [eva] tests/value/gauges.c:72: Frama_C_show_each:
 < [eva] tests/value/gauges.c:72: Frama_C_show_each:
-105,106d91
+113,114d99
 < [eva:alarm] tests/value/gauges.c:81: Warning: 
 <   signed overflow. assert k + 1 ≤ 2147483647;
-108,109d92
+116,117d100
 < [eva:alarm] tests/value/gauges.c:84: Warning: 
 <   signed overflow. assert k + 1 ≤ 2147483647;
-117c100
+125c108
 < [eva] tests/value/gauges.c:86: Frama_C_show_each: [0..2147483647]
 ---
 > [eva] tests/value/gauges.c:86: Frama_C_show_each: {390}
-131,132d113
+139,140d121
 < [eva:alarm] tests/value/gauges.c:99: Warning: 
 <   signed overflow. assert c + 1 ≤ 2147483647;
-170,173c151,154
+178,181c159,162
 < [eva] tests/value/gauges.c:129: Frama_C_show_each: {{ &y + [4..36],0%4 }}
 < [eva] tests/value/gauges.c:129: Frama_C_show_each: {{ &y + [4..40],0%4 }}
 < [eva:alarm] tests/value/gauges.c:130: Warning: 
@@ -93,93 +89,93 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.o
 >   Frama_C_show_each: {{ &y + {4; 8; 12; 16; 20; 24} }}
 > [eva] tests/value/gauges.c:129: 
 >   Frama_C_show_each: {{ &y + {4; 8; 12; 16; 20; 24} }}
-179,180d159
+187,188d167
 < [eva:alarm] tests/value/gauges.c:140: Warning: 
 <   signed overflow. assert j + 1 ≤ 2147483647;
-198,200d176
+206,208d184
 < [eva:alarm] tests/value/gauges.c:158: Warning: 
 <   out of bounds write. assert \valid(tmp);
 <                        (tmp from p--)
-247,250d222
+255,258d230
 < [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);
-258,263d229
+266,271d237
 < [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++)
-307,310c273
+315,318c281
 < [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}
-316,317d278
+324,325d286
 < [eva:alarm] tests/value/gauges.c:251: Warning: 
 <   signed overflow. assert j + 1 ≤ 2147483647;
-319c280
+327c288
 <   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}
-325,328c286
+333,336c294
 < [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}
-334,335d291
+342,343d299
 < [eva:alarm] tests/value/gauges.c:274: Warning: 
 <   signed overflow. assert j + 1 ≤ 2147483647;
-337c293
+345c301
 <   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}
-345,346d300
+353,354d308
 < [eva:alarm] tests/value/gauges.c:293: Warning: 
 <   signed overflow. assert j + 1 ≤ 2147483647;
-348c302
+356c310
 <   Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..2147483647]
 ---
 >   Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [99..119]
-407a362,365
+415a370,373
 >   # Gauges domain:
 >   V: [{[ p -> {{ &x }}
 >          i -> {1} ]}]
 >   s395: λ(0)
-464a423,426
+472a431,434
 >   # Gauges domain:
 >   V: [{[ i -> {1} ]}]
 >   s395: λ([0 .. 1])
 >         {[ i -> {1} ]}
-520a483,486
+528a491,494
 >   # Gauges domain:
 >   V: [{[ i -> {1} ]}]
 >   s395: λ([0 .. 2])
 >         {[ i -> {1} ]}
-576a543,546
+584a551,554
 >   # Gauges domain:
 >   V: [{[ i -> {1} ]}]
 >   s395: λ([0 .. 10])
 >         {[ i -> {1} ]}
-638a609,613
+646a617,621
 >   # Gauges domain:
 >   V: [{[ p -> {{ &a }}
 >          i -> {2} ]}]
 >   s409: λ(0)
 >   s408: λ(0)
-696a672,676
+704a680,684
 >   # Gauges domain:
 >   V: [{[ i -> {2} ]}]
 >   s409: λ(0)
 >   s408: λ([0 .. 1])
 >         {[ i -> {0} ]}
-698a679,800
+706a687,808
 > [eva] tests/value/gauges.c:325: 
 >   Frama_C_dump_each:
 >   # Cvalue domain:
@@ -302,61 +298,53 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.o
 >   s408: λ([0 .. +oo])
 >         {[ i -> {0} ]}
 >   ==END OF DUMP==
-706a809,810
+714a817,818
 > [eva] tests/value/gauges.c:343: Call to builtin malloc
 > [eva] tests/value/gauges.c:343: Call to builtin malloc
-716c820
-<   l ∈ [4..2147483647]
----
->   l ∈ [4..53]
-721c825
-<   l ∈ [4..2147483647]
----
->   l ∈ [4..53]
-759,760c863,864
+767,768c871,872
 <   A ∈ {{ &A + [0..--],0%4 }}
 <   B ∈ {{ &B + [0..--],0%4 }}
 ---
 >   A ∈ {{ &A + [0..36],0%4 }}
 >   B ∈ {{ &B + [0..36],0%4 }}
-778c882
+786c890
 <   i ∈ {45; 46; 47; 48; 49; 50; 51}
 ---
 >   i ∈ {45; 46; 47; 48}
-784c888
+792c896
 <   i ∈ {-59; -58; -57; -56; -55; -54; -53}
 ---
 >   i ∈ {-58; -57; -56; -55; -54; -53}
-804c908
+812c916
 <   p ∈ {{ &u + [0..--],0%4 }}
 ---
 >   p ∈ {{ &u + [0..400],0%4 }}
-806c910
+814c918
 <   k ∈ [0..2147483647]
 ---
 >   k ∈ [0..390]
-811c915
+819c923
 <   i ∈ [0..2147483647]
 ---
 >   i ∈ [0..21]
-822,823c926,928
+830,831c934,936
 <    [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] }}
-834c939
+842c947
 <   p ∈ {{ &T + [--..396],0%4 }}
 ---
 >   p ∈ {{ &T + [-4..396],0%4 }}
-969,970c1074,1075
+977,978c1082,1083
 <   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]
-1048c1153
+1056c1161
 <     p; A[0..9]; B[0..9]
 ---
 >     p; A[0..8]; B[0..8]
@@ -850,11 +838,6 @@ diff tests/value/oracle/noreturn.res.oracle tests/value/oracle_gauges/noreturn.r
 > [eva] tests/value/noreturn.i:7: starting to merge loop iterations
 36a40
 > [eva] tests/value/noreturn.i:13: starting to merge loop iterations
-diff tests/value/oracle/precise_locations.res.oracle tests/value/oracle_gauges/precise_locations.res.oracle
-40a41
-> [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
-517a519
-> [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
 diff tests/value/oracle/reduce_formals.res.oracle tests/value/oracle_gauges/reduce_formals.res.oracle
 10a11
 > [eva] tests/value/reduce_formals.i:5: starting to merge loop iterations
@@ -901,10 +884,6 @@ diff tests/value/oracle/semaphore.res.oracle tests/value/oracle_gauges/semaphore
 diff tests/value/oracle/symbolic_locs.res.oracle tests/value/oracle_gauges/symbolic_locs.res.oracle
 133a134
 > [eva] tests/value/symbolic_locs.i:93: starting to merge loop iterations
-diff tests/value/oracle/test.0.res.oracle tests/value/oracle_gauges/test.0.res.oracle
-18a19,20
-> [eva:alarm] tests/value/test.i:10: Warning: 
->   signed overflow. assert i + 1 ≤ 2147483647;
 diff tests/value/oracle/undefined_sequence.0.res.oracle tests/value/oracle_gauges/undefined_sequence.0.res.oracle
 97a98
 > [eva] tests/value/undefined_sequence.i:43: starting to merge loop iterations
@@ -952,33 +931,7 @@ diff tests/value/oracle/va_list2.1.res.oracle tests/value/oracle_gauges/va_list2
 > [eva] computing for function __builtin_va_arg <- main.
 >   Called from tests/value/va_list2.c:20.
 > [eva] Done for function __builtin_va_arg
-diff tests/value/oracle/widen_non_constant.res.oracle tests/value/oracle_gauges/widen_non_constant.res.oracle
-28c28
-<   Frama_C_show_each_in: [0..23], [1..23]
----
->   Frama_C_show_each_in: [0..22], [1..23]
-47c47
-<   Frama_C_show_each_in: [0..25], [1..23]
----
->   Frama_C_show_each_in: [0..22], [1..23]
-66,70c66
-<   Frama_C_show_each_in: [0..2147483647], [1..23]
-< [eva:alarm] tests/value/widen_non_constant.i:49: Warning: 
-<   out of bounds read. assert \valid_read(p + j);
-< [eva:alarm] tests/value/widen_non_constant.i:45: Warning: 
-<   signed overflow. assert j + 1 ≤ 2147483647;
----
->   Frama_C_show_each_in: [0..22], [1..23]
-88c84
-<   j ∈ {23; 24}
----
->   j ∈ {23}
-91c87
-<   j ∈ {23; 24; 25; 26}
----
->   j ∈ {23; 24; 25}
 diff tests/value/oracle/widen_on_non_monotonic.res.oracle tests/value/oracle_gauges/widen_on_non_monotonic.res.oracle
-24a25,27
-> [eva] tests/value/widen_on_non_monotonic.i:26: starting to merge loop iterations
+25a26,27
 > [eva] tests/value/widen_on_non_monotonic.i:21: starting to merge loop iterations
 > [eva] tests/value/widen_on_non_monotonic.i:18: starting to merge loop iterations

tests/value/inversion2.i

 /* run.config*
-   STDOPT: +"-then -wlevel 4"
+   STDOPT: +"-then -eva-widening-delay 4 -eva-widening-period 3"
 */
 
 int T[3] = {3,1,2};

tests/value/oracle/for_loops.3.res.oracle

@@ -8,6 +8,8 @@
 [eva] tests/value/for_loops.c:50: starting to merge loop iterations
 [eva] tests/value/for_loops.c:52: starting to merge loop iterations
 [eva] tests/value/for_loops.c:55: Frama_C_show_each_F: {0; 1}, [0..2147483647]
+[eva] tests/value/for_loops.c:55: 
+  Frama_C_show_each_F: {0; 1; 2}, [0..2147483647]
 [eva] tests/value/for_loops.c:55: 
   Frama_C_show_each_F: {0; 1; 2; 3; 4; 5}, [0..2147483647]
 [eva] Recording results for main_4

tests/value/oracle/gauges.res.oracle

@@ -31,6 +31,10 @@
 [eva] tests/value/gauges.c:21: Frama_C_show_each_1: {{ "in" }}
 [eva] tests/value/gauges.c:19: Frama_C_show_each_0: {{ "in" }}
 [eva] tests/value/gauges.c:21: Frama_C_show_each_1: {{ "in" }}
+[eva] tests/value/gauges.c:19: Frama_C_show_each_0: {{ "in" }}
+[eva] tests/value/gauges.c:21: Frama_C_show_each_1: {{ "in" }}
+[eva] tests/value/gauges.c:19: Frama_C_show_each_0: {{ "in" }}
+[eva] tests/value/gauges.c:21: Frama_C_show_each_1: {{ "in" }}
 [eva:alarm] tests/value/gauges.c:26: Warning: 
   signed overflow. assert l + 1 ≤ 2147483647;
 [eva] Recording results for main0
@@ -59,6 +63,10 @@
 [eva] tests/value/gauges.c:43: Frama_C_show_each_1: {{ "in" }}
 [eva] tests/value/gauges.c:41: Frama_C_show_each_0: {{ "in" }}
 [eva] tests/value/gauges.c:43: Frama_C_show_each_1: {{ "in" }}
+[eva] tests/value/gauges.c:41: Frama_C_show_each_0: {{ "in" }}
+[eva] tests/value/gauges.c:43: Frama_C_show_each_1: {{ "in" }}
+[eva] tests/value/gauges.c:41: Frama_C_show_each_0: {{ "in" }}
+[eva] tests/value/gauges.c:43: Frama_C_show_each_1: {{ "in" }}
 [eva:alarm] tests/value/gauges.c:48: Warning: 
   signed overflow. assert l + 1 ≤ 2147483647;
 [eva] Recording results for main0_bis

tests/value/oracle/precise_locations.res.oracle

@@ -38,6 +38,8 @@
 [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
 [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
 [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
+[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
+[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
 [eva] tests/value/precise_locations.i:42: 
   Frama_C_dump_each:
   # Cvalue domain:
@@ -523,6 +525,8 @@
 [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
 [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
 [eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
+[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
+[eva] tests/value/precise_locations.i:39: Reusing old results for call to ct
 [eva] tests/value/precise_locations.i:42: 
   Frama_C_dump_each:
   # Cvalue domain:

tests/value/oracle/widen_non_constant.res.oracle

@@ -25,7 +25,7 @@
   Frama_C_show_each_in: {0; 1; 2}, [1..23]
 [eva] tests/value/widen_non_constant.i:11: Frama_C_show_each_out: [0..22]
 [eva] tests/value/widen_non_constant.i:13: 
-  Frama_C_show_each_in: [0..23], [1..23]
+  Frama_C_show_each_in: [0..22], [1..23]
 [eva] Recording results for main1
 [eva] Done for function main1
 [eva] computing for function main2 <- main.
@@ -44,7 +44,7 @@
   Frama_C_show_each_in: {0; 1; 2}, [1..23]
 [eva] tests/value/widen_non_constant.i:27: Frama_C_show_each_out: [0..22]
 [eva] tests/value/widen_non_constant.i:29: 
-  Frama_C_show_each_in: [0..25], [1..23]
+  Frama_C_show_each_in: [0..22], [1..23]
 [eva] Recording results for main2
 [eva] Done for function main2
 [eva] computing for function main3 <- main.
@@ -63,11 +63,7 @@
   Frama_C_show_each_in: {0; 1; 2}, [1..23]
 [eva] tests/value/widen_non_constant.i:46: Frama_C_show_each_out: [0..22]
 [eva] tests/value/widen_non_constant.i:48: 
-  Frama_C_show_each_in: [0..2147483647], [1..23]
-[eva:alarm] tests/value/widen_non_constant.i:49: Warning: 
-  out of bounds read. assert \valid_read(p + j);
-[eva:alarm] tests/value/widen_non_constant.i:45: Warning: 
-  signed overflow. assert j + 1 ≤ 2147483647;
+  Frama_C_show_each_in: [0..22], [1..23]
 [eva] Recording results for main3
 [eva] Done for function main3
 [eva] computing for function main4 <- main.
@@ -85,10 +81,10 @@
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main1:
   i ∈ {24} or UNINITIALIZED
-  j ∈ {23; 24}
+  j ∈ {23}
 [eva:final-states] Values at end of function main2:
   i ∈ {24; 25} or UNINITIALIZED
-  j ∈ {23; 24; 25; 26}
+  j ∈ {23; 24; 25}
 [eva:final-states] Values at end of function main3:
   i ∈ [24..2147483647] or UNINITIALIZED
   j ∈ [23..2147483647]
@@ -139,7 +135,7 @@
 [inout] Out (internal) for function main2:
     i; j
 [inout] Inputs for function main2:
-    N; B[0..25]
+    N; B[0..23]
 [inout] Out (internal) for function main3:
     i; j; p
 [inout] Inputs for function main3:
@@ -151,4 +147,4 @@
 [inout] Out (internal) for function main:
     t[0..19]; u[0..39]
 [inout] Inputs for function main:
-    N; A[0..23]; B[0..25]; C[0..23]
+    N; A[0..23]; B[0..23]; C[0..23]