diff --git a/src/plugins/value/engine/basic_partitioning.ml b/src/plugins/value/engine/basic_partitioning.ml
index a2ee7cd2334c2054306e511758b2aff6391218ef..ae99cfef5dc0c0e3fa85292ba024326b7ccbfa92 100644
--- a/src/plugins/value/engine/basic_partitioning.ml
+++ b/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 =
diff --git a/src/plugins/value/engine/legacy_partitioning.ml b/src/plugins/value/engine/legacy_partitioning.ml
index 119ce80be5b7c8fc63e922e867423bda28c061a4..bee9eba706bbe1df282416ca133e6ad35c265c87 100644
--- a/src/plugins/value/engine/legacy_partitioning.ml
+++ b/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 =
diff --git a/src/plugins/value/engine/loop_partitioning.ml b/src/plugins/value/engine/loop_partitioning.ml
index eda3d98eaddd19d1e10df402a34e5cf313d77c21..a6700d0c89021b88247c4f6f692926140260bc04 100644
--- a/src/plugins/value/engine/loop_partitioning.ml
+++ b/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 =
diff --git a/src/plugins/value/engine/partitioned_dataflow.ml b/src/plugins/value/engine/partitioned_dataflow.ml
index 24468248e01ddab61772479a99508b42e6ec234a..aa0be86c0bb64f3d80441a05509ce8adab7a4037 100644
--- a/src/plugins/value/engine/partitioned_dataflow.ml
+++ b/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
diff --git a/src/plugins/value/engine/state_partitioning.mli b/src/plugins/value/engine/state_partitioning.mli
index 50932afe1d8bee85ac3cadc44c8906d4c0fcc080..a76253bb3b3c35a6ecffcdfc75cdd2c1a269bd30 100644
--- a/src/plugins/value/engine/state_partitioning.mli
+++ b/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 --- *)
diff --git a/tests/builtins/diff_apron b/tests/builtins/diff_apron
index 215d8f1df7cece5656f8c82a14effb4a356c165a..7bad8145315eae01b8b8e80ebf71649c52f66c8d 100644
--- a/tests/builtins/diff_apron
+++ b/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
diff --git a/tests/builtins/oracle/allocated.0.res.oracle b/tests/builtins/oracle/allocated.0.res.oracle
index 7c583e99a0d108b55be78768c5e3ec3f8bda29fd..53996c93021c6cccab5e34b52c79a0da159e8edb 100644
--- a/tests/builtins/oracle/allocated.0.res.oracle
+++ b/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:
diff --git a/tests/idct/diff_apron b/tests/idct/diff_apron
index 07ec6615cb68f450e80398c2a18f2b35734090c3..e3b1cc3498b58bc966268b7fde9c6f975955f128 100644
--- a/tests/idct/diff_apron
+++ b/tests/idct/diff_apron
@@ -1,5 +1,9 @@
diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_1180_1990.res.oracle
-143,150c143,158
+147,158c147,170
+< [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:
@@ -25,7 +29,15 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
-386,404c394,427
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function IEEE_1180_1990_rand
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function IEEE_1180_1990_rand
+412,430c424,461
< [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:
@@ -66,6 +78,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function 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.
@@ -80,7 +96,7 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:260.
> [eva] Recording results for idct
> [eva] Done for function idct
-427,431c450,461
+455,459c486,497
< [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:
@@ -99,7 +115,7 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:284.
> [eva] Recording results for idct
> [eva] Done for function idct
-458,476c488,521
+486,504c524,561
< [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:
@@ -140,6 +156,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function 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.
@@ -154,7 +174,7 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:306.
> [eva] Recording results for idct
> [eva] Done for function idct
-499,503c544,555
+529,533c586,597
< [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:
@@ -173,7 +193,7 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:330.
> [eva] Recording results for idct
> [eva] Done for function idct
-527,540c579,602
+557,570c621,1920
< [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:
@@ -213,7 +233,36 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
-562a625,812
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function 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] computing for function IEEE_1180_1990_idctf <- main.
@@ -236,6 +285,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> 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] Recording results for IEEE_1180_1990_idctf
> [eva] Done for function IEEE_1180_1990_idctf
> [eva] computing for function idct <- main.
@@ -280,6 +333,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function 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.
@@ -332,6 +389,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function 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.
@@ -384,6 +445,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function 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.
@@ -402,7 +467,40 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> 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
-588a839,1026
+> [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] computing for function IEEE_1180_1990_idctf <- main.
+> Called from tests/idct/ieee_1180_1990.c:213.
+> [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:141:
+> Call to builtin Frama_C_cos for function cos
+> [eva] tests/idct/ieee_1180_1990.c:141:
+> Call to builtin Frama_C_cos for function cos
+> [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] 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] Recording results for IEEE_1180_1990_idctf
> [eva] Done for function IEEE_1180_1990_idctf
> [eva] computing for function idct <- main.
@@ -447,6 +545,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function 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.
@@ -499,6 +601,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function 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.
@@ -551,6 +657,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function 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.
@@ -573,6 +683,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> 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] computing for function IEEE_1180_1990_idctf <- main.
@@ -591,20 +705,24 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> 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
-595,597c1033,1036
-< [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] 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] Recording results for IEEE_1180_1990_idctf
+> [eva] Done for function IEEE_1180_1990_idctf
> [eva] computing for function idct <- main.
> Called from tests/idct/ieee_1180_1990.c:214.
> [eva] Recording results for idct
> [eva] Done for function idct
-602,604c1041,1048
-< [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_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] computing for function IEEE_1180_1990_idctf <- main.
> Called from tests/idct/ieee_1180_1990.c:237.
> [eva] Recording results for IEEE_1180_1990_idctf
@@ -613,36 +731,12 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:238.
> [eva] Recording results for idct
> [eva] Done for function idct
-607,634c1051,1100
-< [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: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:257.
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function IEEE_1180_1990_rand
> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
@@ -693,36 +787,12 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:284.
> [eva] Recording results for idct
> [eva] Done for function idct
-637,664c1103,1152
-< [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: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:303.
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function IEEE_1180_1990_rand
> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
@@ -773,22 +843,12 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:330.
> [eva] Recording results for idct
> [eva] Done for function idct
-667,680c1155,1178
-< [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] computing for function IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:211.
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function IEEE_1180_1990_rand
> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
@@ -813,7 +873,32 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
-702a1201,1384
+> [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] computing for function IEEE_1180_1990_idctf <- main.
@@ -836,6 +921,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> 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] Recording results for IEEE_1180_1990_idctf
> [eva] Done for function IEEE_1180_1990_idctf
> [eva] computing for function idct <- main.
@@ -880,9 +969,13 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function 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.
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function 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:258.
> [eva] Recording results for IEEE_1180_1990_dctf
> [eva] Done for function IEEE_1180_1990_dctf
@@ -932,6 +1025,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function 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.
@@ -984,6 +1081,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function 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.
@@ -998,7 +1099,14 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> 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
-706a1389,1526
+> [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:
@@ -1025,6 +1133,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> 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] Recording results for IEEE_1180_1990_idctf
> [eva] Done for function IEEE_1180_1990_idctf
> [eva] computing for function idct <- main.
@@ -1069,6 +1181,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function 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.
@@ -1121,6 +1237,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function 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.
@@ -1137,191 +1257,8 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> [eva] Done for function idct
> [eva] computing for function IEEE_1180_1990_dctf <- main.
> Called from tests/idct/ieee_1180_1990.c:328.
-709,891c1529,1920
-< [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] 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
-< [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] 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
-< [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] 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
-< [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] 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
-< [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] 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
----
+> [eva] Recording results for IEEE_1180_1990_dctf
+> [eva] Done for function IEEE_1180_1990_dctf
> [eva] computing for function IEEE_1180_1990_idctf <- main.
> Called from tests/idct/ieee_1180_1990.c:329.
> [eva] Recording results for IEEE_1180_1990_idctf
@@ -1356,6 +1293,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function 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.
@@ -1378,6 +1319,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> 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] computing for function IEEE_1180_1990_idctf <- main.
@@ -1400,6 +1345,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> 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] Recording results for IEEE_1180_1990_idctf
> [eva] Done for function IEEE_1180_1990_idctf
> [eva] computing for function idct <- main.
@@ -1444,6 +1393,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function 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.
@@ -1496,6 +1449,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function 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.
@@ -1548,52 +1505,258 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function 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] Recording results for IEEE_1180_1990_dctf
-> [eva] Done for function IEEE_1180_1990_dctf
-> [eva] computing for function IEEE_1180_1990_idctf <- main.
-> Called from tests/idct/ieee_1180_1990.c:213.
-> [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:141:
-> Call to builtin Frama_C_cos for function cos
-> [eva] tests/idct/ieee_1180_1990.c:141:
-> Call to builtin Frama_C_cos for function cos
-> [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] Recording results for IEEE_1180_1990_idctf
-> [eva] Done for function IEEE_1180_1990_idctf
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function IEEE_1180_1990_rand
+625,870c1975,2102
+< [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] 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
+< [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] 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
+< [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] 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
+< [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] 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
+< [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] 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
+< [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] 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
+< [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] computing for function idct <- main.
> Called from tests/idct/ieee_1180_1990.c:214.
> [eva] Recording results for idct
@@ -1636,6 +1799,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function 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.
@@ -1688,6 +1855,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
+> [eva] computing for function IEEE_1180_1990_rand <- IEEE_1180_1990_mkbk <- main.
+> Called from tests/idct/ieee_1180_1990.c:85.
+> [eva] Recording results for IEEE_1180_1990_rand
+> [eva] Done for function 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.
@@ -1714,11 +1885,3 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:330.
> [eva] Recording results for idct
> [eva] Done for function idct
-928c1957
-< M1[0..7][0..7] ∈ [--..--]
----
-> M1[0..7][0..7] ∈ [-2147483647..2147483647]
-981c2010
-< M1[0..7][0..7] ∈ [--..--]
----
-> M1[0..7][0..7] ∈ [-2147483647..2147483647]
diff --git a/tests/idct/diff_equalities b/tests/idct/diff_equalities
index 5f09e60791d3d583e2acf66b3d51a9cd27307033..c05946b24e4198945f24cbdb5026a6409c4233b5 100644
--- a/tests/idct/diff_equalities
+++ b/tests/idct/diff_equalities
@@ -1,136 +1,132 @@
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
diff --git a/tests/idct/diff_gauges b/tests/idct/diff_gauges
index 9dadfa3ad4acafa682d4b75a2e68cf7d8501c8a7..2e026cd69baf3e0a3aaf3b9860e252aa0206841c 100644
--- a/tests/idct/diff_gauges
+++ b/tests/idct/diff_gauges
@@ -1,68 +1,7 @@
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
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 90343756005917a5aded940e75b0e60e55de5dc5..2c7e41c81de51023519cf04af34b7d44f3d10625 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/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:
diff --git a/tests/misc/oracle/widen_hints.3.res.oracle b/tests/misc/oracle/widen_hints.3.res.oracle
index 3902e2fed2a871e7dfd08da77f11ae43418d47a5..79d60b32b3b9badb829a55c05956c4d962637469 100644
--- a/tests/misc/oracle/widen_hints.3.res.oracle
+++ b/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}
diff --git a/tests/misc/oracle/widen_hints2.0.res.oracle b/tests/misc/oracle/widen_hints2.0.res.oracle
index b949a5fac96d9e63bed6787a4bc70ae584ef37b5..0840ecb088a0a4ba0d87e80332ef9e85938a5576 100644
--- a/tests/misc/oracle/widen_hints2.0.res.oracle
+++ b/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
diff --git a/tests/value/diff_apron b/tests/value/diff_apron
index 8c2cbc881293cc729e99add053c790e25a4e7d06..4db64f563c465c1d4e071079d9cb5ed7031b8f26 100644
--- a/tests/value/diff_apron
+++ b/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:
diff --git a/tests/value/diff_gauges b/tests/value/diff_gauges
index 3d1ff9f636a54499fdc1814c7b5e351655892a57..4bd4e2a505c9cb67d339bb60fb2210dc2dcd8e14 100644
--- a/tests/value/diff_gauges
+++ b/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
diff --git a/tests/value/inversion2.i b/tests/value/inversion2.i
index d1f31a4f0e4cbf1d819eecfe4e5ed048bac130fe..e9a935555be48a67a2c5722bd65e1bda1bfb50fd 100644
--- a/tests/value/inversion2.i
+++ b/tests/value/inversion2.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-then -wlevel 4"
+ STDOPT: +"-then -eva-widening-delay 4 -eva-widening-period 3"
*/
int T[3] = {3,1,2};
diff --git a/tests/value/oracle/for_loops.3.res.oracle b/tests/value/oracle/for_loops.3.res.oracle
index 45b480710cf5a31a306d622bef103cafb6b77238..2a34a2785890e51ba8d1bfade2e5139520bf6cc8 100644
--- a/tests/value/oracle/for_loops.3.res.oracle
+++ b/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
diff --git a/tests/value/oracle/gauges.res.oracle b/tests/value/oracle/gauges.res.oracle
index c8dd303217a7811d5e5782c00a43c44f7a16fff6..289e246d8ac73d48cb1a4111f42a59e03092aa8b 100644
--- a/tests/value/oracle/gauges.res.oracle
+++ b/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
diff --git a/tests/value/oracle/precise_locations.res.oracle b/tests/value/oracle/precise_locations.res.oracle
index c959c220fa9c6c58ff14fc913b51819332300dcf..999fe42373a269c2c55b6dc086405196c483b91a 100644
--- a/tests/value/oracle/precise_locations.res.oracle
+++ b/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:
diff --git a/tests/value/oracle/widen_non_constant.res.oracle b/tests/value/oracle/widen_non_constant.res.oracle
index c8d94a6191b6ff0943a57b64cdb4fb7a8476e0c6..6d5b5622a50133d23f68a4dd49a64e297d862e3c 100644
--- a/tests/value/oracle/widen_non_constant.res.oracle
+++ b/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]
diff --git a/tests/value/oracle/widen_on_non_monotonic.res.oracle b/tests/value/oracle/widen_on_non_monotonic.res.oracle
index c0a867022e7b0ac9291602e4f3920c22181e3de8..5270640d92190f496ad3e554f4b893c6676e78ba 100644
--- a/tests/value/oracle/widen_on_non_monotonic.res.oracle
+++ b/tests/value/oracle/widen_on_non_monotonic.res.oracle
@@ -20,6 +20,7 @@
Called from tests/value/widen_on_non_monotonic.i:71.
[eva] tests/value/widen_on_non_monotonic.i:25: starting to merge loop iterations
[eva] tests/value/widen_on_non_monotonic.i:23: starting to merge loop iterations
+[eva] tests/value/widen_on_non_monotonic.i:26: starting to merge loop iterations
[eva:alarm] tests/value/widen_on_non_monotonic.i:27: Warning:
signed overflow. assert -2147483648 ≤ b - 1;
[eva] Recording results for main1
diff --git a/tests/value/precise_locations.i b/tests/value/precise_locations.i
index 3f3051f0dc6324e869083ba75cd0e769a668e19d..06340dba48ae65c8c9ed814351463b7a34cc27ab 100644
--- a/tests/value/precise_locations.i
+++ b/tests/value/precise_locations.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-then -inout -load-module report -report -then -plevel 250"
+ STDOPT: +"-eva-widening-period 3 -then -inout -load-module report -report -then -plevel 250"
*/
struct s {