From 9a647053f699c985122efd2bb52883472a49e1da Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 9 Jan 2019 15:35:01 +0100
Subject: [PATCH] [Eva] Updates alternative oracles.
---
tests/builtins/diff_apron | 25 +-
tests/idct/diff_apron | 839 ++++++++++++++++++++++---------------
tests/idct/diff_equalities | 110 +++--
tests/idct/diff_gauges | 65 +--
tests/value/diff_apron | 142 +++----
tests/value/diff_gauges | 131 ++----
6 files changed, 656 insertions(+), 656 deletions(-)
diff --git a/tests/builtins/diff_apron b/tests/builtins/diff_apron
index 215d8f1df7c..7bad8145315 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/idct/diff_apron b/tests/idct/diff_apron
index 07ec6615cb6..e3b1cc3498b 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 5f09e60791d..c05946b24e4 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 9dadfa3ad4a..2e026cd69ba 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/value/diff_apron b/tests/value/diff_apron
index 8c2cbc88129..4db64f563c4 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 3d1ff9f636a..4bd4e2a505c 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
--
GitLab