From 02475d7760a7803bae458c3c9225028460bbf8d8 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 7 Apr 2021 11:18:34 +0200
Subject: [PATCH] [EVA] removes previous oracles
---
tests/value/diff_apron | 1508 -----------------------------------
tests/value/diff_bitwise | 54 --
tests/value/diff_equalities | 870 --------------------
tests/value/diff_gauges | 1284 -----------------------------
tests/value/diff_octagons | 413 ----------
tests/value/diff_symblocs | 329 --------
6 files changed, 4458 deletions(-)
delete mode 100644 tests/value/diff_apron
delete mode 100644 tests/value/diff_bitwise
delete mode 100644 tests/value/diff_equalities
delete mode 100644 tests/value/diff_gauges
delete mode 100644 tests/value/diff_octagons
delete mode 100644 tests/value/diff_symblocs
diff --git a/tests/value/diff_apron b/tests/value/diff_apron
deleted file mode 100644
index b8f9fbe7d8c..00000000000
--- a/tests/value/diff_apron
+++ /dev/null
@@ -1,1508 +0,0 @@
-diff tests/value/oracle/alias.1.res.oracle tests/value/oracle_apron/alias.1.res.oracle
-85c85
-< z ∈ {0; 1; 2}
----
-> z ∈ {0; 2}
-diff tests/value/oracle/alias.2.res.oracle tests/value/oracle_apron/alias.2.res.oracle
-76c76
-< z ∈ {-5; -4; -3; -2; -1; 0; 1; 1000}
----
-> z ∈ {-1; 1000}
-diff tests/value/oracle/alias.3.res.oracle tests/value/oracle_apron/alias.3.res.oracle
-67c67
-< z ∈ {0; 1; 2}
----
-> z ∈ {0; 2}
-diff tests/value/oracle/alias.6.res.oracle tests/value/oracle_apron/alias.6.res.oracle
-82c82
-< t ∈ {4; 5; 6}
----
-> t ∈ {5}
-diff tests/value/oracle/array_degenerating_loop.res.oracle tests/value/oracle_apron/array_degenerating_loop.res.oracle
-11,12d10
-< [eva:alarm] tests/value/array_degenerating_loop.i:9: Warning:
-< signed overflow. assert G + t[i] ≤ 2147483647;
-14c12
-< Frama_C_show_each: [55..2147483647], [-2147483648..99]
----
-> Frama_C_show_each: [55..155], [-2147483648..99]
-diff tests/value/oracle/auto_loop_unroll.0.res.oracle tests/value/oracle_apron/auto_loop_unroll.0.res.oracle
-11,13c11
-< [eva:alarm] tests/value/auto_loop_unroll.c:25: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:27: Frama_C_show_each_auto: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:27: Frama_C_show_each_auto: {100}
-15,18c13
-< [eva:alarm] tests/value/auto_loop_unroll.c:31: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:33:
-< Frama_C_show_each_imprecise: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:33: Frama_C_show_each_imprecise: {1000}
-20,23c15
-< [eva:alarm] tests/value/auto_loop_unroll.c:39: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:41:
-< Frama_C_show_each_imprecise: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:41: Frama_C_show_each_imprecise: {100}
-32,34c24
-< [eva:alarm] tests/value/auto_loop_unroll.c:58: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:59: Frama_C_show_each_64: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:59: Frama_C_show_each_64: {64}
-36,38c26
-< [eva:alarm] tests/value/auto_loop_unroll.c:63: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:64: Frama_C_show_each_40: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:64: Frama_C_show_each_40: [0..120]
-40,42c28
-< [eva:alarm] tests/value/auto_loop_unroll.c:69: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:72: Frama_C_show_each_80: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:72: Frama_C_show_each_80: [0..160]
-44,47c30
-< [eva:alarm] tests/value/auto_loop_unroll.c:76: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:82:
-< Frama_C_show_each_32_80: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:82: Frama_C_show_each_32_80: [0..164]
-55,56d37
-< [eva:alarm] tests/value/auto_loop_unroll.c:88: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-60,62c41
-< [eva:alarm] tests/value/auto_loop_unroll.c:93: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:95: Frama_C_show_each_101: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:95: Frama_C_show_each_101: {101}
-71c50,53
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-81c63,66
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-90c75,78
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-107c95,98
-< [eva] tests/value/auto_loop_unroll.c:100: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:100.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-114,115d104
-< [eva:alarm] tests/value/auto_loop_unroll.c:14: Warning:
-< signed overflow. assert g + 1 ≤ 2147483647;
-118c107,110
-< [eva] tests/value/auto_loop_unroll.c:100: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:100.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-121,122d112
-< [eva:alarm] tests/value/auto_loop_unroll.c:18: Warning:
-< signed overflow. assert i + 1 ≤ 2147483647;
-125c115
-< [eva] tests/value/auto_loop_unroll.c:103: Frama_C_show_each_25: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:103: Frama_C_show_each_25: {25}
-131c121,122
-< [eva] tests/value/auto_loop_unroll.c:112: Frama_C_show_each_120: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:112:
-> Frama_C_show_each_120: [15..2147483647]
-133,136c124
-< [eva:alarm] tests/value/auto_loop_unroll.c:120: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:122:
-< Frama_C_show_each_32_64: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:122: Frama_C_show_each_32_64: [0..65]
-152,153d139
-< [eva:alarm] tests/value/auto_loop_unroll.c:145: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-160c146
-< Frama_C_show_each_imprecise: [0..2147483647]
----
-> Frama_C_show_each_imprecise: [10..2147483647]
-178,183c164,172
-< [eva] tests/value/auto_loop_unroll.c:162: Reusing old results for call to incr_g
-< [eva] tests/value/auto_loop_unroll.c:162: Reusing old results for call to incr_g
-< [eva:alarm] tests/value/auto_loop_unroll.c:164: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:166:
-< Frama_C_show_each_imprecise: [0..2147483647]
----
-> [eva] computing for function incr_g <- complex_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:162.
-> [eva] Recording results for incr_g
-> [eva] Done for function incr_g
-> [eva] computing for function incr_g <- complex_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:162.
-> [eva] Recording results for incr_g
-> [eva] Done for function incr_g
-> [eva] tests/value/auto_loop_unroll.c:166: Frama_C_show_each_imprecise: [0..64]
-185,188c174
-< [eva:alarm] tests/value/auto_loop_unroll.c:173: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:175:
-< Frama_C_show_each_imprecise: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:175: Frama_C_show_each_imprecise: [0..9]
-190,191d175
-< [eva:alarm] tests/value/auto_loop_unroll.c:181: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-195c179
-< Frama_C_show_each_imprecise: [0..2147483647]
----
-> Frama_C_show_each_imprecise: [64..2147483647]
-201,203c185
-< [eva:alarm] tests/value/auto_loop_unroll.c:193: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:195: Frama_C_show_each_11: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:195: Frama_C_show_each_11: {11}
-205,207c187
-< [eva:alarm] tests/value/auto_loop_unroll.c:198: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:200: Frama_C_show_each_12: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:200: Frama_C_show_each_12: {12}
-209,210d188
-< [eva:alarm] tests/value/auto_loop_unroll.c:204: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-212a191,192
-> [eva:alarm] tests/value/auto_loop_unroll.c:204: Warning:
-> signed overflow. assert res + 1 ≤ 2147483647;
-216,217d195
-< [eva:alarm] tests/value/auto_loop_unroll.c:209: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-219a198,199
-> [eva:alarm] tests/value/auto_loop_unroll.c:209: Warning:
-> signed overflow. assert res + 1 ≤ 2147483647;
-223,224d202
-< [eva:alarm] tests/value/auto_loop_unroll.c:217: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-228,231c206
-< [eva:alarm] tests/value/auto_loop_unroll.c:222: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:226:
-< Frama_C_show_each_11_111: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:226: Frama_C_show_each_11_111: [11..111]
-239,241c214
-< [eva:alarm] tests/value/auto_loop_unroll.c:236: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:238: Frama_C_show_each_20: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:238: Frama_C_show_each_20: [20..2147483646]
-243,244d215
-< [eva:alarm] tests/value/auto_loop_unroll.c:241: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-247c218,220
-< [eva] tests/value/auto_loop_unroll.c:243: Frama_C_show_each_21: [0..2147483647]
----
-> [eva:alarm] tests/value/auto_loop_unroll.c:241: Warning:
-> signed overflow. assert res + 1 ≤ 2147483647;
-> [eva] tests/value/auto_loop_unroll.c:243: Frama_C_show_each_21: {21}
-253,255c226,227
-< [eva:alarm] tests/value/auto_loop_unroll.c:250: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:254: Frama_C_show_each_30: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:254: Frama_C_show_each_30: {30}
-> [eva] tests/value/auto_loop_unroll.c:258: starting to merge loop iterations
-258,259c230,231
-< [eva] tests/value/auto_loop_unroll.c:258: starting to merge loop iterations
-< [eva] tests/value/auto_loop_unroll.c:263: Frama_C_show_each_top: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:263:
-> Frama_C_show_each_top: [31..2147483647]
-261,263c233
-< [eva:alarm] tests/value/auto_loop_unroll.c:267: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:272: Frama_C_show_each_32: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:272: Frama_C_show_each_32: {32}
-268c238
-< Frama_C_show_each_33_inf: [0..2147483647]
----
-> Frama_C_show_each_33_inf: [33..2147483647]
-272,273d241
-< [eva:alarm] tests/value/auto_loop_unroll.c:283: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-281c249
-< __retres ∈ [1..2147483647]
----
-> __retres ∈ [1..25]
-283c251
-< g ∈ [1..2147483647]
----
-> g ∈ [1..126]
-diff tests/value/oracle/auto_loop_unroll.1.res.oracle tests/value/oracle_apron/auto_loop_unroll.1.res.oracle
-15,18c15
-< [eva:alarm] tests/value/auto_loop_unroll.c:31: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:33:
-< Frama_C_show_each_imprecise: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:33: Frama_C_show_each_imprecise: {1000}
-20,23c17
-< [eva:alarm] tests/value/auto_loop_unroll.c:39: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:41:
-< Frama_C_show_each_imprecise: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:41: Frama_C_show_each_imprecise: {100}
-58c52,55
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-67c64,67
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-76c76,79
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-85c88,91
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-94c100,103
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-103c112,115
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-112c124,127
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-121c136,139
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-130c148,151
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-139c160,163
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-148c172,175
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-157c184,187
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-166c196,199
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-175c208,211
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-184c220,223
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-193c232,235
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-202c244,247
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-211c256,259
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-220c268,271
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-229c280,283
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-238c292,295
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-247c304,307
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-256c316,319
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-265c328,331
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-274c340,343
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-296,297d364
-< [eva:alarm] tests/value/auto_loop_unroll.c:145: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-304c371
-< Frama_C_show_each_imprecise: [0..2147483647]
----
-> Frama_C_show_each_imprecise: [10..2147483647]
-322,327c389,397
-< [eva] tests/value/auto_loop_unroll.c:162: Reusing old results for call to incr_g
-< [eva] tests/value/auto_loop_unroll.c:162: Reusing old results for call to incr_g
-< [eva:alarm] tests/value/auto_loop_unroll.c:164: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:166:
-< Frama_C_show_each_imprecise: [0..2147483647]
----
-> [eva] computing for function incr_g <- complex_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:162.
-> [eva] Recording results for incr_g
-> [eva] Done for function incr_g
-> [eva] computing for function incr_g <- complex_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:162.
-> [eva] Recording results for incr_g
-> [eva] Done for function incr_g
-> [eva] tests/value/auto_loop_unroll.c:166: Frama_C_show_each_imprecise: [0..64]
-329,332c399
-< [eva:alarm] tests/value/auto_loop_unroll.c:173: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:175:
-< Frama_C_show_each_imprecise: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:175: Frama_C_show_each_imprecise: [0..9]
-334,335d400
-< [eva:alarm] tests/value/auto_loop_unroll.c:181: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-339c404
-< Frama_C_show_each_imprecise: [0..2147483647]
----
-> Frama_C_show_each_imprecise: [64..2147483647]
-344c409
-< [eva:loop-unroll] tests/value/auto_loop_unroll.c:192: Automatic loop unrolling.
----
-> [eva] tests/value/auto_loop_unroll.c:192: starting to merge loop iterations
-346c411
-< [eva:loop-unroll] tests/value/auto_loop_unroll.c:197: Automatic loop unrolling.
----
-> [eva] tests/value/auto_loop_unroll.c:197: starting to merge loop iterations
-348,353c413,429
-< [eva:loop-unroll] tests/value/auto_loop_unroll.c:203: Automatic loop unrolling.
-< [eva] tests/value/auto_loop_unroll.c:206: Frama_C_show_each_0_13: [0..13]
-< [eva:loop-unroll] tests/value/auto_loop_unroll.c:208: Automatic loop unrolling.
-< [eva] tests/value/auto_loop_unroll.c:211: Frama_C_show_each_0_14: [0..14]
-< [eva:loop-unroll] tests/value/auto_loop_unroll.c:214: Automatic loop unrolling.
-< [eva] tests/value/auto_loop_unroll.c:219: Frama_C_show_each_0_15: [0..15]
----
-> [eva] tests/value/auto_loop_unroll.c:203: starting to merge loop iterations
-> [eva:alarm] tests/value/auto_loop_unroll.c:203: Warning:
-> signed overflow. assert -2147483648 ≤ i_0 - 1;
-> [eva:alarm] tests/value/auto_loop_unroll.c:204: Warning:
-> signed overflow. assert res + 1 ≤ 2147483647;
-> [eva] tests/value/auto_loop_unroll.c:206:
-> Frama_C_show_each_0_13: [0..2147483647]
-> [eva] tests/value/auto_loop_unroll.c:208: starting to merge loop iterations
-> [eva:alarm] tests/value/auto_loop_unroll.c:208: Warning:
-> signed overflow. assert -2147483648 ≤ i_1 - 1;
-> [eva:alarm] tests/value/auto_loop_unroll.c:209: Warning:
-> signed overflow. assert res + 1 ≤ 2147483647;
-> [eva] tests/value/auto_loop_unroll.c:211:
-> Frama_C_show_each_0_14: [0..2147483647]
-> [eva] tests/value/auto_loop_unroll.c:214: starting to merge loop iterations
-> [eva] tests/value/auto_loop_unroll.c:219:
-> Frama_C_show_each_0_15: [0..2147483647]
-364c440,444
-< [eva:loop-unroll] tests/value/auto_loop_unroll.c:240: Automatic loop unrolling.
----
-> [eva] tests/value/auto_loop_unroll.c:240: starting to merge loop iterations
-> [eva:alarm] tests/value/auto_loop_unroll.c:240: Warning:
-> signed overflow. assert -2147483648 ≤ i - 1;
-> [eva:alarm] tests/value/auto_loop_unroll.c:241: Warning:
-> signed overflow. assert res + 1 ≤ 2147483647;
-375c455,456
-< [eva] tests/value/auto_loop_unroll.c:263: Frama_C_show_each_top: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:263:
-> Frama_C_show_each_top: [31..2147483647]
-391,392d471
-< [eva:alarm] tests/value/auto_loop_unroll.c:283: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-425,426c504,505
-< i ∈ {-1}
-< res ∈ {21}
----
-> i ∈ [-2147483648..20]
-> res ∈ [0..2147483647]
-diff tests/value/oracle/backward_add_ptr.res.oracle tests/value/oracle_apron/backward_add_ptr.res.oracle
-71c71,74
-< [eva] tests/value/backward_add_ptr.c:91: Reusing old results for call to gm
----
-> [eva] computing for function gm <- main3 <- main.
-> Called from tests/value/backward_add_ptr.c:91.
-> [eva] Recording results for gm
-> [eva] Done for function gm
-93c96,99
-< [eva] tests/value/backward_add_ptr.c:110: Reusing old results for call to gm
----
-> [eva] computing for function gm <- main3 <- main.
-> Called from tests/value/backward_add_ptr.c:110.
-> [eva] Recording results for gm
-> [eva] Done for function gm
-107c113,116
-< [eva] tests/value/backward_add_ptr.c:125: Reusing old results for call to gm
----
-> [eva] computing for function gm <- main3 <- main.
-> Called from tests/value/backward_add_ptr.c:125.
-> [eva] Recording results for gm
-> [eva] Done for function gm
-160c169,172
-< [eva] tests/value/backward_add_ptr.c:160: Reusing old results for call to gm
----
-> [eva] computing for function gm <- main4 <- main.
-> Called from tests/value/backward_add_ptr.c:160.
-> [eva] Recording results for gm
-> [eva] Done for function gm
-diff tests/value/oracle/call_simple.res.oracle tests/value/oracle_apron/call_simple.res.oracle
-28c28
-< c ∈ [--..--]
----
-> c ∈ [-2147483648..2147483646]
-diff tests/value/oracle/deps_compose.res.oracle tests/value/oracle_apron/deps_compose.res.oracle
-24c24,27
-< [eva] tests/value/deps_compose.i:26: Reusing old results for call to f
----
-> [eva] computing for function f <- main.
-> Called from tests/value/deps_compose.i:26.
-> [eva] Recording results for f
-> [eva] Done for function f
-diff tests/value/oracle/divneg.res.oracle tests/value/oracle_apron/divneg.res.oracle
-57c57
-< vic ∈ {4294967295}
----
-> vic ∈ {-1}
-diff tests/value/oracle/domains_function.res.oracle tests/value/oracle_apron/domains_function.res.oracle
-107c107,110
-< [eva] tests/value/domains_function.c:63: Reusing old results for call to use
----
-> [eva] computing for function use <- test_propagation <- main.
-> Called from tests/value/domains_function.c:63.
-> [eva] Recording results for use
-> [eva] Done for function use
-diff tests/value/oracle/downcast.1.res.oracle tests/value/oracle_apron/downcast.1.res.oracle
-61c61
-< [100000..2147483647], [100145..2147483647], [100145..2147483647]
----
-> [100000..2147483502], [100145..2147483647], [100145..2147483647]
-diff tests/value/oracle/dur.res.oracle tests/value/oracle_apron/dur.res.oracle
-310c310
-< V6 ∈ [--..--] or UNINITIALIZED
----
-> V6 ∈ [0..32767] or UNINITIALIZED
-diff tests/value/oracle/find_ivaltop.res.oracle tests/value/oracle_apron/find_ivaltop.res.oracle
-32,33c32,33
-< j ∈ {0; 1; 2; 3; 4; 5; 6; 7}
-< X ∈ {1; 2; 3; 4; 5; 6; 7; 8}
----
-> j ∈ {7}
-> X ∈ {8}
-39c39
-< \result FROM t[0..7]
----
-> \result FROM t[7]
-44c44
-< t[0..7]
----
-> t[7]
-diff tests/value/oracle/for_loops.1.res.oracle tests/value/oracle_apron/for_loops.1.res.oracle
-39,41c39
-< [eva:alarm] tests/value/for_loops.c:16: Warning:
-< signed overflow. assert w + 1 ≤ 2147483647;
-< [eva] tests/value/for_loops.c:17: Frama_C_show_each_F: [0..2147483647]
----
-> [eva] tests/value/for_loops.c:17: Frama_C_show_each_F: [0..100]
-47c45
-< j ∈ [0..2147483647]
----
-> j ∈ [0..100]
-diff tests/value/oracle/for_loops.2.res.oracle tests/value/oracle_apron/for_loops.2.res.oracle
-37,39c37
-< [eva:alarm] tests/value/for_loops.c:42: Warning:
-< signed overflow. assert w + T[j] ≤ 2147483647;
-< [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/fptr.0.res.oracle tests/value/oracle_apron/fptr.0.res.oracle
-57c57,60
-< [eva] tests/value/fptr.i:9: Reusing old results for call to h
----
-> [eva] computing for function h <- f <- main.
-> Called from tests/value/fptr.i:9.
-> [eva] Recording results for h
-> [eva] Done for function h
-66,67c69,76
-< [eva] tests/value/fptr.i:9: Reusing old results for call to hh
-< [eva] tests/value/fptr.i:9: Reusing old results for call to h
----
-> [eva] computing for function hh <- f <- main.
-> Called from tests/value/fptr.i:9.
-> [eva] Recording results for hh
-> [eva] Done for function hh
-> [eva] computing for function h <- f <- main.
-> Called from tests/value/fptr.i:9.
-> [eva] Recording results for h
-> [eva] Done for function h
-72c81,92
-< [eva] tests/value/fptr.i:52: Reusing old results for call to f
----
-> [eva] computing for function f <- main.
-> Called from tests/value/fptr.i:52.
-> [eva] computing for function hh <- f <- main.
-> Called from tests/value/fptr.i:9.
-> [eva] Recording results for hh
-> [eva] Done for function hh
-> [eva] computing for function h <- f <- main.
-> Called from tests/value/fptr.i:9.
-> [eva] Recording results for h
-> [eva] Done for function h
-> [eva] Recording results for f
-> [eva] Done for function f
-diff tests/value/oracle/fptr.1.res.oracle tests/value/oracle_apron/fptr.1.res.oracle
-42c42,45
-< [eva] tests/value/fptr.i:9: Reusing old results for call to h
----
-> [eva] computing for function h <- f <- main_uninit.
-> Called from tests/value/fptr.i:9.
-> [eva] Recording results for h
-> [eva] Done for function h
-51,52c54,61
-< [eva] tests/value/fptr.i:9: Reusing old results for call to hh
-< [eva] tests/value/fptr.i:9: Reusing old results for call to h
----
-> [eva] computing for function hh <- f <- main_uninit.
-> Called from tests/value/fptr.i:9.
-> [eva] Recording results for hh
-> [eva] Done for function hh
-> [eva] computing for function h <- f <- main_uninit.
-> Called from tests/value/fptr.i:9.
-> [eva] Recording results for h
-> [eva] Done for function h
-57c66,77
-< [eva] tests/value/fptr.i:68: Reusing old results for call to f
----
-> [eva] computing for function f <- main_uninit.
-> Called from tests/value/fptr.i:68.
-> [eva] computing for function hh <- f <- main_uninit.
-> Called from tests/value/fptr.i:9.
-> [eva] Recording results for hh
-> [eva] Done for function hh
-> [eva] computing for function h <- f <- main_uninit.
-> Called from tests/value/fptr.i:9.
-> [eva] Recording results for h
-> [eva] Done for function h
-> [eva] Recording results for f
-> [eva] Done for function f
-diff tests/value/oracle/from_call.0.res.oracle tests/value/oracle_apron/from_call.0.res.oracle
-68c68,73
-< [eva] tests/value/from_call.i:20: Reusing old results for call to g
----
-> [eva] computing for function g <- f <- main.
-> Called from tests/value/from_call.i:20.
-> [eva] Recording results for g
-> [from] Computing for function g
-> [from] Done for function g
-> [eva] Done for function g
-78c83,88
-< [eva] tests/value/from_call.i:20: Reusing old results for call to g
----
-> [eva] computing for function g <- f <- main.
-> Called from tests/value/from_call.i:20.
-> [eva] Recording results for g
-> [from] Computing for function g
-> [from] Done for function g
-> [eva] Done for function g
-149,150c159,170
-< [eva] tests/value/from_call.i:44: Reusing old results for call to return_A1
-< [eva] tests/value/from_call.i:44: Reusing old results for call to return_A2
----
-> [eva] computing for function return_A1 <- dispatcher2 <- call_dispatcher2 <- main.
-> Called from tests/value/from_call.i:44.
-> [eva] Recording results for return_A1
-> [from] Computing for function return_A1
-> [from] Done for function return_A1
-> [eva] Done for function return_A1
-> [eva] computing for function return_A2 <- dispatcher2 <- call_dispatcher2 <- main.
-> Called from tests/value/from_call.i:44.
-> [eva] Recording results for return_A2
-> [from] Computing for function return_A2
-> [from] Done for function return_A2
-> [eva] Done for function return_A2
-diff tests/value/oracle/from_call.1.res.oracle tests/value/oracle_apron/from_call.1.res.oracle
-64c64,67
-< [eva] tests/value/from_call.i:20: Reusing old results for call to g
----
-> [eva] computing for function g <- f <- main.
-> Called from tests/value/from_call.i:20.
-> [eva] Recording results for g
-> [eva] Done for function g
-72c75,78
-< [eva] tests/value/from_call.i:20: Reusing old results for call to g
----
-> [eva] computing for function g <- f <- main.
-> Called from tests/value/from_call.i:20.
-> [eva] Recording results for g
-> [eva] Done for function g
-123,124c129,136
-< [eva] tests/value/from_call.i:44: Reusing old results for call to return_A1
-< [eva] tests/value/from_call.i:44: Reusing old results for call to return_A2
----
-> [eva] computing for function return_A1 <- dispatcher2 <- call_dispatcher2 <- main.
-> Called from tests/value/from_call.i:44.
-> [eva] Recording results for return_A1
-> [eva] Done for function return_A1
-> [eva] computing for function return_A2 <- dispatcher2 <- call_dispatcher2 <- main.
-> Called from tests/value/from_call.i:44.
-> [eva] Recording results for return_A2
-> [eva] Done for function return_A2
-diff tests/value/oracle/fun_ptr.0.res.oracle tests/value/oracle_apron/fun_ptr.0.res.oracle
-39c39,42
-< [eva] tests/value/fun_ptr.i:33: Reusing old results for call to f
----
-> [eva] computing for function f <- test2 <- main.
-> Called from tests/value/fun_ptr.i:33.
-> [eva] Recording results for f
-> [eva] Done for function f
-diff tests/value/oracle/fun_ptr.1.res.oracle tests/value/oracle_apron/fun_ptr.1.res.oracle
-43c43,46
-< [eva] tests/value/fun_ptr.i:33: Reusing old results for call to f
----
-> [eva] computing for function f <- test2 <- main.
-> Called from tests/value/fun_ptr.i:33.
-> [eva] Recording results for f
-> [eva] Done for function f
-diff tests/value/oracle/gauges.res.oracle tests/value/oracle_apron/gauges.res.oracle
-38,39d37
-< [eva:alarm] tests/value/gauges.c:26: Warning:
-< signed overflow. assert l + 1 ≤ 2147483647;
-70,71d67
-< [eva:alarm] tests/value/gauges.c:48: Warning:
-< signed overflow. assert l + 1 ≤ 2147483647;
-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]
-139,140d134
-< [eva:alarm] tests/value/gauges.c:99: Warning:
-< signed overflow. assert c + 1 ≤ 2147483647;
-187,188d180
-< [eva:alarm] tests/value/gauges.c:140: Warning:
-< signed overflow. assert j + 1 ≤ 2147483647;
-303,304d294
-< [eva:alarm] tests/value/gauges.c:220: Warning:
-< signed overflow. assert -2147483648 ≤ n - 1;
-319,320d308
-< [eva:alarm] tests/value/gauges.c:240: Warning:
-< signed overflow. assert j + 1 ≤ 2147483647;
-322c310
-< 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]
-328,329d315
-< [eva:alarm] tests/value/gauges.c:251: Warning:
-< signed overflow. assert j + 1 ≤ 2147483647;
-331c317
-< 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]
-337,338d322
-< [eva:alarm] tests/value/gauges.c:263: Warning:
-< signed overflow. assert j + 1 ≤ 2147483647;
-340c324
-< 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]
-346,347d329
-< [eva:alarm] tests/value/gauges.c:274: Warning:
-< signed overflow. assert j + 1 ≤ 2147483647;
-349c331
-< 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]
-357,358d338
-< [eva:alarm] tests/value/gauges.c:293: Warning:
-< signed overflow. assert j + 1 ≤ 2147483647;
-360c340
-< Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..2147483647]
----
-> Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..598]
-802c782
-< n ∈ [-2147483648..99]
----
-> n ∈ [-2147483547..99]
-805c785
-< i ∈ [0..2147483647]
----
-> i ∈ [10..2147483647]
-841c821
-< i ∈ [0..2147483647]
----
-> i ∈ [0..21]
-diff tests/value/oracle/ghost.res.oracle tests/value/oracle_apron/ghost.res.oracle
-10,11d9
-< [eva:alarm] tests/value/ghost.i:17: Warning:
-< signed overflow. assert G + 1 ≤ 2147483647;
-diff tests/value/oracle/hierarchical_convergence.res.oracle tests/value/oracle_apron/hierarchical_convergence.res.oracle
-40c40
-< j ∈ [0..2147483647]
----
-> j ∈ [0..99]
-diff tests/value/oracle/initialized_copy.1.res.oracle tests/value/oracle_apron/initialized_copy.1.res.oracle
-24,27c24
-< c_0[bits 0 to 7] ∈ {1} or UNINITIALIZED
-< [bits 8 to 15] ∈ {2}
-< [bits 16 to 23] ∈ {3}
-< [bits 24 to 31] ∈ {4}
----
-> c_0 ∈ {67305985} or UNINITIALIZED
-29,32c26
-< a_2[bits 0 to 7] ∈ {1} or UNINITIALIZED
-< [bits 8 to 15] ∈ {2}
-< [bits 16 to 23] ∈ {3}
-< [bits 24 to 31] ∈ {4}
----
-> a_2 ∈ {67305985} or UNINITIALIZED
-diff tests/value/oracle/invalid_loc_return.res.oracle tests/value/oracle_apron/invalid_loc_return.res.oracle
-70c70,73
-< [eva] tests/value/invalid_loc_return.i:17: Reusing old results for call to foo
----
-> [eva] computing for function foo <- main <- main2.
-> Called from tests/value/invalid_loc_return.i:17.
-> [eva] Recording results for foo
-> [eva] Done for function foo
-diff tests/value/oracle/local.res.oracle tests/value/oracle_apron/local.res.oracle
-22c22,25
-< [eva] tests/value/local.i:13: Reusing old results for call to f
----
-> [eva] computing for function f <- g <- main.
-> Called from tests/value/local.i:13.
-> [eva] Recording results for f
-> [eva] Done for function f
-diff tests/value/oracle/local_slevel.res.oracle tests/value/oracle_apron/local_slevel.res.oracle
-13,15c13,15
-< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {0; 1}
-< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {-1}, {0}, {0; 1}
-< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {0; 1; 2}
----
-> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {1}
-> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {-1}, {0}, {0}
-> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {1}
-18c18
-< Frama_C_show_each: {1}, [1..79],1%2, {0; 1; 2; 3}
----
-> Frama_C_show_each: {1}, [1..79],1%2, {1; 2; 3}
-22c22
-< Frama_C_show_each: {1}, [1..79],1%2, {0; 1; 2; 3; 4}
----
-> Frama_C_show_each: {1}, [1..79],1%2, {1; 2; 3; 4}
-26,34c26
-< Frama_C_show_each: {1}, [1..79],1%2, [0..2147483647]
-< [eva] tests/value/local_slevel.i:18:
-< Frama_C_show_each: {-1}, [0..78],0%2, [0..2147483647]
-< [eva] tests/value/local_slevel.i:18:
-< Frama_C_show_each: {1}, [1..79],1%2, [0..2147483648]
-< [eva] tests/value/local_slevel.i:18:
-< Frama_C_show_each: {-1}, [0..78],0%2, [0..2147483648]
-< [eva] tests/value/local_slevel.i:18:
-< Frama_C_show_each: {1}, [1..79],1%2, [0..4294967295]
----
-> Frama_C_show_each: {1}, [1..79],1%2, [1..79]
-36c28
-< Frama_C_show_each: {-1}, [0..78],0%2, [0..4294967295]
----
-> Frama_C_show_each: {-1}, [0..78],0%2, [0..78]
-152c144
-< r ∈ [--..--]
----
-> r ∈ [0..2147483647]
-393,395c385,387
-< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {0; 1}
-< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {-1}, {0}, {0; 1}
-< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {0; 1; 2}
----
-> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {1}
-> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {-1}, {0}, {0}
-> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {1}
-398c390
-< Frama_C_show_each: {1}, [1..79],1%2, {0; 1; 2; 3}
----
-> Frama_C_show_each: {1}, [1..79],1%2, {1; 2; 3}
-402c394
-< Frama_C_show_each: {1}, [1..79],1%2, {0; 1; 2; 3; 4}
----
-> Frama_C_show_each: {1}, [1..79],1%2, {1; 2; 3; 4}
-406,414c398
-< Frama_C_show_each: {1}, [1..79],1%2, [0..2147483647]
-< [eva] tests/value/local_slevel.i:18:
-< Frama_C_show_each: {-1}, [0..78],0%2, [0..2147483647]
-< [eva] tests/value/local_slevel.i:18:
-< Frama_C_show_each: {1}, [1..79],1%2, [0..2147483648]
-< [eva] tests/value/local_slevel.i:18:
-< Frama_C_show_each: {-1}, [0..78],0%2, [0..2147483648]
-< [eva] tests/value/local_slevel.i:18:
-< Frama_C_show_each: {1}, [1..79],1%2, [0..4294967295]
----
-> Frama_C_show_each: {1}, [1..79],1%2, [1..79]
-416c400
-< Frama_C_show_each: {-1}, [0..78],0%2, [0..4294967295]
----
-> Frama_C_show_each: {-1}, [0..78],0%2, [0..78]
-532c516
-< r ∈ [--..--]
----
-> r ∈ [0..2147483647]
-diff tests/value/oracle/logicdeps.res.oracle tests/value/oracle_apron/logicdeps.res.oracle
-31c31,39
-< [eva] tests/value/logicdeps.i:25: Reusing old results for call to g
----
-> [eva] computing for function g <- main.
-> Called from tests/value/logicdeps.i:25.
-> [eva] computing for function f <- g <- main.
-> Called from tests/value/logicdeps.i:13.
-> [eva] Done for function f
-> [eva] Recording results for g
-> [from] Computing for function g
-> [from] Done for function g
-> [eva] Done for function g
-51c59,67
-< [eva] tests/value/logicdeps.i:32: Reusing old results for call to g
----
-> [eva] computing for function g <- main.
-> Called from tests/value/logicdeps.i:32.
-> [eva] computing for function f <- g <- main.
-> Called from tests/value/logicdeps.i:13.
-> [eva] Done for function f
-> [eva] Recording results for g
-> [from] Computing for function g
-> [from] Done for function g
-> [eva] Done for function g
-diff tests/value/oracle/long.res.oracle tests/value/oracle_apron/long.res.oracle
-15,17c15,26
-< [eva] tests/value/long.i:12: Reusing old results for call to f
-< [eva] tests/value/long.i:12: Reusing old results for call to f
-< [eva] tests/value/long.i:12: Reusing old results for call to f
----
-> [eva] computing for function f <- main.
-> Called from tests/value/long.i:12.
-> [eva] Recording results for f
-> [eva] Done for function f
-> [eva] computing for function f <- main.
-> Called from tests/value/long.i:12.
-> [eva] Recording results for f
-> [eva] Done for function f
-> [eva] computing for function f <- main.
-> Called from tests/value/long.i:12.
-> [eva] Recording results for f
-> [eva] Done for function f
-diff tests/value/oracle/long_const.0.res.oracle tests/value/oracle_apron/long_const.0.res.oracle
-19c19,22
-< [eva] tests/value/long_const.i:25: Reusing old results for call to LL_ABS
----
-> [eva] computing for function LL_ABS <- div64 <- main.
-> Called from tests/value/long_const.i:25.
-> [eva] Recording results for LL_ABS
-> [eva] Done for function LL_ABS
-diff tests/value/oracle/long_const.1.res.oracle tests/value/oracle_apron/long_const.1.res.oracle
-19c19,22
-< [eva] tests/value/long_const.i:25: Reusing old results for call to LL_ABS
----
-> [eva] computing for function LL_ABS <- div64 <- main.
-> Called from tests/value/long_const.i:25.
-> [eva] Recording results for LL_ABS
-> [eva] Done for function LL_ABS
-diff tests/value/oracle/loop_wvar.1.res.oracle tests/value/oracle_apron/loop_wvar.1.res.oracle
-12,13d11
-< [eva:alarm] tests/value/loop_wvar.i:57: Warning:
-< signed overflow. assert next + 1 ≤ 2147483647;
-27,28c25
-< [eva] tests/value/loop_wvar.i:71: Frama_C_show_each: [0..9], [0..17], [0..11]
-< [eva] tests/value/loop_wvar.i:71: Frama_C_show_each: [0..9], [0..18], [0..12]
----
-> [eva] tests/value/loop_wvar.i:71: Frama_C_show_each: [0..9], [0..9], [0..9]
-37,38c34,35
-< j ∈ [0..18]
-< k ∈ [0..12]
----
-> j ∈ [0..17]
-> k ∈ [0..11]
-41c38
-< next ∈ [0..2147483647]
----
-> next ∈ [0..25]
-diff tests/value/oracle/loopinv.res.oracle tests/value/oracle_apron/loopinv.res.oracle
-51,53c51
-< [eva:alarm] tests/value/loopinv.c:45: Warning:
-< signed overflow. assert j + 1 ≤ 2147483647;
-< [eva] tests/value/loopinv.c:46: Frama_C_show_each: [0..99], [0..2147483647]
----
-> [eva] tests/value/loopinv.c:46: Frama_C_show_each: [0..99], [0..100]
-134,135d131
-< [ - ] Assertion 'Eva,signed_overflow' (file tests/value/loopinv.c, line 45)
-< tried with Eva.
-148,149c144,145
-< 4 To be validated
-< 13 Total
----
-> 3 To be validated
-> 12 Total
-diff tests/value/oracle/memexec.res.oracle tests/value/oracle_apron/memexec.res.oracle
-27,32c27,50
-< [eva] tests/value/memexec.c:13: Reusing old results for call to f11
-< [eva] tests/value/memexec.c:14: Reusing old results for call to f11
-< [eva] tests/value/memexec.c:16: Reusing old results for call to f11
-< [eva] tests/value/memexec.c:18: Reusing old results for call to f11
-< [eva] tests/value/memexec.c:20: Reusing old results for call to f11
-< [eva] tests/value/memexec.c:21: Reusing old results for call to f11
----
-> [eva] computing for function f11 <- f1 <- main.
-> Called from tests/value/memexec.c:13.
-> [eva] Recording results for f11
-> [eva] Done for function f11
-> [eva] computing for function f11 <- f1 <- main.
-> Called from tests/value/memexec.c:14.
-> [eva] Recording results for f11
-> [eva] Done for function f11
-> [eva] computing for function f11 <- f1 <- main.
-> Called from tests/value/memexec.c:16.
-> [eva] Recording results for f11
-> [eva] Done for function f11
-> [eva] computing for function f11 <- f1 <- main.
-> Called from tests/value/memexec.c:18.
-> [eva] Recording results for f11
-> [eva] Done for function f11
-> [eva] computing for function f11 <- f1 <- main.
-> Called from tests/value/memexec.c:20.
-> [eva] Recording results for f11
-> [eva] Done for function f11
-> [eva] computing for function f11 <- f1 <- main.
-> Called from tests/value/memexec.c:21.
-> [eva] Recording results for f11
-> [eva] Done for function f11
-106c124,127
-< [eva] tests/value/memexec.c:113: Reusing old results for call to f5_aux
----
-> [eva] computing for function f5_aux <- f5 <- main.
-> Called from tests/value/memexec.c:113.
-> [eva] Recording results for f5_aux
-> [eva] Done for function f5_aux
-129c150,153
-< [eva] tests/value/memexec.c:137: Reusing old results for call to f7_1
----
-> [eva] computing for function f7_1 <- f7 <- main.
-> Called from tests/value/memexec.c:137.
-> [eva] Recording results for f7_1
-> [eva] Done for function f7_1
-144c168,171
-< [eva] tests/value/memexec.c:150: Reusing old results for call to f8_1
----
-> [eva] computing for function f8_1 <- f8 <- main.
-> Called from tests/value/memexec.c:150.
-> [eva] Recording results for f8_1
-> [eva] Done for function f8_1
-diff tests/value/oracle/modulo.res.oracle tests/value/oracle_apron/modulo.res.oracle
-40a41,64
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [-9..-1], [-8..0]
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [1..9], [-8..0]
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [-9..-1], [0..8]
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [1..9], [0..8]
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> [-9..-1], {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {-8; -7; -6; -5; -4; -3; -2; -1},
-> {1; 2; 3; 4; 5; 6; 7},
-> {-6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
-50a75,98
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [1..9], [-8..0]
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [-9..-1], [-8..0]
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [1..9], [0..8]
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [-9..-1], [0..8]
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> [-9..-1], {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {-8; -7; -6; -5; -4; -3; -2; -1},
-> {1; 2; 3; 4; 5; 6; 7},
-> {-6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
-60a109,110
-> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-10..10], [-9..9], [-8..8]
-> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-9..9], [-8..8], [-7..7]
-diff tests/value/oracle/octagons.res.oracle tests/value/oracle_apron/octagons.res.oracle
-270,273c270,273
-< a ∈ [-1024..2147483647]
-< b ∈ [-1023..2147483647]
-< c ∈ [-1023..2147483647]
-< d ∈ [-1032..2147483647]
----
-> a ∈ [-603..2147483646]
-> b ∈ [-602..2147483647]
-> c ∈ [-602..1446]
-> d ∈ [-611..2147483647]
-diff tests/value/oracle/offsetmap.0.res.oracle tests/value/oracle_apron/offsetmap.0.res.oracle
-64,65c64
-< a[bits 0 to 7] ∈ {1; 6}
-< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
----
-> a ∈ {1; 6}
-67,68c66
-< a7[bits 0 to 7] ∈ {1}
-< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
----
-> a7 ∈ {1}
-108,109c106
-< a[bits 0 to 7] ∈ {1; 6}
-< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
----
-> a ∈ {1; 6}
-111,112c108
-< a7[bits 0 to 7] ∈ {1}
-< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
----
-> a7 ∈ {1}
-diff tests/value/oracle/offsetmap.1.res.oracle tests/value/oracle_apron/offsetmap.1.res.oracle
-64,69c64,66
-< a[bits 0 to 7] ∈ {1; 6}
-< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
-< b[bits 0 to 7] ∈ {0; 1}
-< [bits 8 to 31]# ∈ {0; 6}%32, bits 8 to 31
-< a7[bits 0 to 7] ∈ {1}
-< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
----
-> a ∈ {1; 6}
-> b ∈ {0; 1}
-> a7 ∈ {1}
-109,114c106,108
-< a[bits 0 to 7] ∈ {1; 6}
-< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
-< b[bits 0 to 7] ∈ {0; 1}
-< [bits 8 to 31]# ∈ {0; 6}%32, bits 8 to 31
-< a7[bits 0 to 7] ∈ {1}
-< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
----
-> a ∈ {1; 6}
-> b ∈ {0; 1}
-> a7 ∈ {1}
-diff tests/value/oracle/partitioning-annots.4.res.oracle tests/value/oracle_apron/partitioning-annots.4.res.oracle
-15,16d14
-< [eva:alarm] tests/value/partitioning-annots.c:138: Warning:
-< division by zero. assert j ≢ 0;
-diff tests/value/oracle/precise_locations.res.oracle tests/value/oracle_apron/precise_locations.res.oracle
-32,35c32,47
-< [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] 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
-> [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
-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
-< [eva] tests/value/precise_locations.i:39: Reusing old results for call to 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
-> [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
-> [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
-> [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
-< [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] 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
-> [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
-> [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
-> [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
-> [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.
-> Called from tests/value/precond.c:39.
-53c55,56
-< [eva] tests/value/precond.c:39: Reusing old results for call to f
----
-> [eva] Recording results for f
-> [eva] Done for function f
-diff tests/value/oracle/ptr_relation.1.res.oracle tests/value/oracle_apron/ptr_relation.1.res.oracle
-24c24
-< j ∈ {-1; 0; 1}
----
-> j ∈ {0}
-diff tests/value/oracle/raz.res.oracle tests/value/oracle_apron/raz.res.oracle
-14c14
-< i ∈ [0..2147483647]
----
-> i ∈ [0..10]
-diff tests/value/oracle/reevaluate_alarms.res.oracle tests/value/oracle_apron/reevaluate_alarms.res.oracle
-61c61
-< S ∈ [0..2147483647]
----
-> S ∈ [4..2147483647]
-diff tests/value/oracle/relation_reduction.res.oracle tests/value/oracle_apron/relation_reduction.res.oracle
-24,27d23
-< [eva:alarm] tests/value/relation_reduction.i:20: Warning:
-< accessing out of bounds index. assert 0 ≤ y;
-< [eva:alarm] tests/value/relation_reduction.i:20: Warning:
-< accessing out of bounds index. assert y < 9;
-34,37c30,33
-< R1 ∈ [-2147483648..2147483637]
-< R2 ∈ [-2147483638..2147483647]
-< R3 ∈ [--..--]
-< R4 ∈ {0; 1; 2; 3; 4; 5}
----
-> R1 ∈ {0; 2}
-> R2 ∈ {0; 12}
-> R3 ∈ {0; 7}
-> R4 ∈ {0; 2}
-diff tests/value/oracle/relation_shift.res.oracle tests/value/oracle_apron/relation_shift.res.oracle
-31,32c31,32
-< r1 ∈ [--..--]
-< r2 ∈ [--..--]
----
-> r1 ∈ {2}
-> r2 ∈ {7}
-35,37c35,37
-< x ∈ [-2147483647..2147483647]
-< y ∈ [-2147483648..2147483646]
-< z ∈ [-2147483642..2147483647]
----
-> x ∈ [-2147483646..2147483642]
-> y ∈ [-2147483648..2147483640]
-> z ∈ [-2147483641..2147483647]
-49,50c49,50
-< r1 ∈ [--..--]
-< r2 ∈ [--..--]
----
-> r1 ∈ {2}
-> r2 ∈ {7}
-53,55c53,55
-< x ∈ [-2147483647..2147483647]
-< y ∈ [-2147483648..2147483646]
-< z ∈ [-2147483642..2147483647]
----
-> x ∈ [-2147483646..2147483642]
-> y ∈ [-2147483648..2147483640]
-> z ∈ [-2147483641..2147483647]
-diff tests/value/oracle/relations.res.oracle tests/value/oracle_apron/relations.res.oracle
-80,81c80,82
-< e ∈ [--..--]
-< f ∈ [--..--]
----
-> e ∈ {1}
-> f[bits 0 to 7] ∈ {1; 4}
-> [bits 8 to 31] ∈ [--..--]
-diff tests/value/oracle/relations2.res.oracle tests/value/oracle_apron/relations2.res.oracle
-25c25
-< len ∈ [--..--]
----
-> len ∈ [0..1023]
-36,37c36
-< [eva] tests/value/relations2.i:17:
-< Frama_C_show_each_end: [0..4294967295], [0..64]
----
-> [eva] tests/value/relations2.i:17: Frama_C_show_each_end: [0..1023], [0..64]
-69,71d67
-< [eva:alarm] tests/value/relations2.i:34: Warning:
-< accessing out of bounds index.
-< assert (unsigned int)(i - (unsigned int)(t + 1)) < 514;
-124,125d119
-< [eva:alarm] tests/value/relations2.i:35: Warning:
-< signed overflow. assert s + b3 ≤ 2147483647;
-140c134
-< len ∈ [--..--]
----
-> len ∈ [0..1023]
-diff tests/value/oracle/return.res.oracle tests/value/oracle_apron/return.res.oracle
-12c12,15
-< [eva] tests/value/return.i:19: Reusing old results for call to f
----
-> [eva] computing for function f <- main.
-> Called from tests/value/return.i:19.
-> [eva] Recording results for f
-> [eva] Done for function f
-diff tests/value/oracle/static.res.oracle tests/value/oracle_apron/static.res.oracle
-22c22,25
-< [eva] tests/value/static.i:20: Reusing old results for call to f
----
-> [eva] computing for function f <- main.
-> Called from tests/value/static.i:20.
-> [eva] Recording results for f
-> [eva] Done for function f
-diff tests/value/oracle/struct2.res.oracle tests/value/oracle_apron/struct2.res.oracle
-81,84d80
-< accessing out of bounds index. assert 0 ≤ (int)(i + j);
-< [eva:alarm] tests/value/struct2.i:185: Warning:
-< accessing out of bounds index. assert (int)(i + j) < 2;
-< [eva:alarm] tests/value/struct2.i:185: Warning:
-106d101
-< [scope:rm_asserts] removing 2 assertion(s)
-diff tests/value/oracle/test.0.res.oracle tests/value/oracle_apron/test.0.res.oracle
-29c29
-< j ∈ [-1073741822..1]
----
-> j ∈ {-1; 0; 1}
-diff tests/value/oracle/undefined_sequence.1.res.oracle tests/value/oracle_apron/undefined_sequence.1.res.oracle
-33c33,36
-< [eva] tests/value/undefined_sequence.i:54: Reusing old results for call to g
----
-> [eva] computing for function g <- main.
-> Called from tests/value/undefined_sequence.i:54.
-> [eva] Recording results for g
-> [eva] Done for function g
-Only in tests/value/oracle: unit_tests.res.oracle
-diff tests/value/oracle/unroll.res.oracle tests/value/oracle_apron/unroll.res.oracle
-13,14d12
-< [eva:alarm] tests/value/unroll.i:34: Warning:
-< signed overflow. assert -2147483648 ≤ j - 1;
-26c24
-< j ∈ [-2147483648..-123]
----
-> j ∈ {-238}
-diff tests/value/oracle/unroll_simple.res.oracle tests/value/oracle_apron/unroll_simple.res.oracle
-8,9d7
-< [eva:alarm] tests/value/unroll_simple.i:11: Warning:
-< signed overflow. assert -2147483648 ≤ j - 1;
-21c19
-< j ∈ [-2147483648..-126]
----
-> j ∈ {-250}
-diff tests/value/oracle/widen_on_non_monotonic.res.oracle tests/value/oracle_apron/widen_on_non_monotonic.res.oracle
-25a26
-> [eva] tests/value/widen_on_non_monotonic.i:21: 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:
-< signed overflow. assert G + 1 ≤ 2147483647;
diff --git a/tests/value/diff_bitwise b/tests/value/diff_bitwise
deleted file mode 100644
index 7ef9494da77..00000000000
--- a/tests/value/diff_bitwise
+++ /dev/null
@@ -1,54 +0,0 @@
-diff tests/value/oracle/addition.res.oracle tests/value/oracle_bitwise/addition.res.oracle
-121,123c121
-< [eva] tests/value/addition.i:52:
-< Assigning imprecise value to p10.
-< The imprecision originates from Arithmetic {tests/value/addition.i:52}
----
-> [eva] tests/value/addition.i:52: Assigning imprecise value to p10.
-163a162
-> {{ garbled mix of &{p1} (origin: Misaligned {tests/value/addition.i:52}) }}
-165a165
-> {{ garbled mix of &{p2} (origin: Misaligned {tests/value/addition.i:56}) }}
-201,203c201
-< p10 ∈
-< {{ garbled mix of &{p1}
-< (origin: Arithmetic {tests/value/addition.i:52}) }}
----
-> p10 ∈ {{ garbled mix of &{p1} }}
-428a427
-> {{ garbled mix of &{p1} (origin: Misaligned {tests/value/addition.i:52}) }}
-467,469c466
-< p10 ∈
-< {{ garbled mix of &{p1}
-< (origin: Arithmetic {tests/value/addition.i:52}) }}
----
-> p10 ∈ {{ garbled mix of &{p1} }}
-diff tests/value/oracle/bitwise.res.oracle tests/value/oracle_bitwise/bitwise.res.oracle
-98c98,101
-< [eva] tests/value/bitwise.i:158: Frama_C_show_each_dead: {0}
----
-> [eva] tests/value/bitwise.i:156:
-> The evaluation of the expression x & 2
-> led to bottom without alarms:
-> at this point the product of states has no possible concretization.
-diff tests/value/oracle/bitwise_pointer.res.oracle tests/value/oracle_bitwise/bitwise_pointer.res.oracle
-34,36c34
-< [eva] tests/value/bitwise_pointer.i:18:
-< Assigning imprecise value to p.
-< The imprecision originates from Arithmetic {tests/value/bitwise_pointer.i:18}
----
-> [eva] tests/value/bitwise_pointer.i:18: Assigning imprecise value to p.
-41,43c39
-< [eva] tests/value/bitwise_pointer.i:22:
-< Assigning imprecise value to p1.
-< The imprecision originates from Arithmetic {tests/value/bitwise_pointer.i:22}
----
-> [eva] tests/value/bitwise_pointer.i:22: Assigning imprecise value to p1.
-diff tests/value/oracle/logic_ptr_cast.res.oracle tests/value/oracle_bitwise/logic_ptr_cast.res.oracle
-8,10c8
-< [eva] tests/value/logic_ptr_cast.i:8:
-< Assigning imprecise value to p.
-< The imprecision originates from Arithmetic {tests/value/logic_ptr_cast.i:8}
----
-> [eva] tests/value/logic_ptr_cast.i:8: Assigning imprecise value to p.
-Only in tests/value/oracle: unit_tests.res.oracle
diff --git a/tests/value/diff_equalities b/tests/value/diff_equalities
deleted file mode 100644
index f07475f33aa..00000000000
--- a/tests/value/diff_equalities
+++ /dev/null
@@ -1,870 +0,0 @@
-diff tests/value/oracle/CruiseControl.res.oracle tests/value/oracle_equalities/CruiseControl.res.oracle
-980c980
-< [0]._C4_ThrottleCmd._I0_Regul_ON ∈ {0; 1}
----
-> [0]._C4_ThrottleCmd._I0_Regul_ON ∈ {1}
-1018c1018
-< [0]._C4_ThrottleCmd._C0_ThrottleRegulation._C0_SaturateThrottle{._I0_ThrottleIn; ._O0_ThrottleOut} ∈
----
-> [0]._C4_ThrottleCmd._C0_ThrottleRegulation._C0_SaturateThrottle._I0_ThrottleIn ∈
-1019a1020,1021
-> [0]._C4_ThrottleCmd._C0_ThrottleRegulation._C0_SaturateThrottle._O0_ThrottleOut ∈
-> [-0.0000000000000000 .. 1.9999998807907104*2^127]
-1033c1035
-< [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
----
-> [-0.0000000000000000 .. 1.9999998807907104*2^127]
-1218c1220
-< [0]._C4_ThrottleCmd._I0_Regul_ON ∈ {0; 1}
----
-> [0]._C4_ThrottleCmd._I0_Regul_ON ∈ {1}
-1230c1232,1236
-< [0]._C4_ThrottleCmd._C0_ThrottleRegulation{._I1_CruiseSpeed; ._I2_VehiculeSpeed; ._O0_Throttle; ._L1_CruiseControl; ._L2_CruiseControl; ._L3_CruiseControl} ∈
----
-> [0]._C4_ThrottleCmd._C0_ThrottleRegulation{._I1_CruiseSpeed; ._I2_VehiculeSpeed} ∈
-> [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
-> [0]._C4_ThrottleCmd._C0_ThrottleRegulation._O0_Throttle ∈
-> [-0.0000000000000000 .. 1.9999998807907104*2^127]
-> [0]._C4_ThrottleCmd._C0_ThrottleRegulation{._L1_CruiseControl; ._L2_CruiseControl; ._L3_CruiseControl} ∈
-1248c1254
-< [0]._C4_ThrottleCmd._C0_ThrottleRegulation{._L4_CruiseControl; ._L13_CruiseControl} ∈
----
-> [0]._C4_ThrottleCmd._C0_ThrottleRegulation._L4_CruiseControl ∈
-1249a1256,1257
-> [0]._C4_ThrottleCmd._C0_ThrottleRegulation._L13_CruiseControl ∈
-> [-0.0000000000000000 .. 1.9999998807907104*2^127]
-1256c1264
-< [0]._C4_ThrottleCmd._C0_ThrottleRegulation._C0_SaturateThrottle{._I0_ThrottleIn; ._O0_ThrottleOut} ∈
----
-> [0]._C4_ThrottleCmd._C0_ThrottleRegulation._C0_SaturateThrottle._I0_ThrottleIn ∈
-1257a1266,1267
-> [0]._C4_ThrottleCmd._C0_ThrottleRegulation._C0_SaturateThrottle._O0_ThrottleOut ∈
-> [-0.0000000000000000 .. 1.9999998807907104*2^127]
-1271c1281
-< [-1.9999998807907104*2^127 .. 1.9999998807907104*2^127]
----
-> [-0.0000000000000000 .. 1.9999998807907104*2^127]
-diff tests/value/oracle/addition.res.oracle tests/value/oracle_equalities/addition.res.oracle
-138,141d137
-< [eva:alarm] tests/value/addition.i:61: Warning:
-< signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
-< [eva:alarm] tests/value/addition.i:61: Warning:
-< signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
-168c164
-< [scope:rm_asserts] removing 9 assertion(s)
----
-> [scope:rm_asserts] removing 7 assertion(s)
-407,410d402
-< [eva:alarm] tests/value/addition.i:61: Warning:
-< signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
-< [eva:alarm] tests/value/addition.i:61: Warning:
-< signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
-433c425
-< [scope:rm_asserts] removing 9 assertion(s)
----
-> [scope:rm_asserts] removing 7 assertion(s)
-diff tests/value/oracle/alias.0.res.oracle tests/value/oracle_equalities/alias.0.res.oracle
-103,104c103,104
-< t ∈ {1; 2; 4}
-< u ∈ {2; 3; 4; 5}
----
-> t ∈ {4}
-> u ∈ {5}
-110c110
-< t2 ∈ {0; 3; 6}
----
-> t2 ∈ {6}
-diff tests/value/oracle/alias.1.res.oracle tests/value/oracle_equalities/alias.1.res.oracle
-85c85
-< z ∈ {0; 1; 2}
----
-> z ∈ {0; 2}
-87,88c87,88
-< v2 ∈ {-1; 0; 1; 2; 3; 4}
-< PTR1 ∈ {{ &p2{[0], [1], [2]} }}
----
-> v2 ∈ {0; 1; 2}
-> PTR1 ∈ {{ &p2{[0], [1]} }}
-90c90
-< PTR3 ∈ {{ &p2{[1], [2], [4]} }}
----
-> PTR3 ∈ {{ &p2{[1], [2]} }}
-110c110
-< t2 FROM p2[0..2]; c
----
-> t2 FROM p2[0..1]; c
-diff tests/value/oracle/alias.2.res.oracle tests/value/oracle_equalities/alias.2.res.oracle
-76c76
-< z ∈ {-5; -4; -3; -2; -1; 0; 1; 1000}
----
-> z ∈ {-2; -1; 0; 1000}
-diff tests/value/oracle/alias.3.res.oracle tests/value/oracle_equalities/alias.3.res.oracle
-67c67
-< z ∈ {0; 1; 2}
----
-> z ∈ {0; 2}
-diff tests/value/oracle/alias.4.res.oracle tests/value/oracle_equalities/alias.4.res.oracle
-81c81
-< y ∈ {0; 3; 77}
----
-> y ∈ {77}
-diff tests/value/oracle/alias.5.res.oracle tests/value/oracle_equalities/alias.5.res.oracle
-59a60
-> [eva] tests/value/alias.i:260: starting to merge loop iterations
-170c171
-< y ∈ {0; 3; 77}
----
-> y ∈ {77}
-diff tests/value/oracle/alias.6.res.oracle tests/value/oracle_equalities/alias.6.res.oracle
-86c86
-< x ∈ {0; 4; 33}
----
-> x ∈ {33}
-diff tests/value/oracle/auto_loop_unroll.0.res.oracle tests/value/oracle_equalities/auto_loop_unroll.0.res.oracle
-81c81,84
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-90c93,96
-< [eva] tests/value/auto_loop_unroll.c:101: Reusing old results for call to incr
----
-> [eva] computing for function incr <- various_loops <- main.
-> Called from tests/value/auto_loop_unroll.c:101.
-> [eva] Recording results for incr
-> [eva] Done for function incr
-diff tests/value/oracle/backward_add_ptr.res.oracle tests/value/oracle_equalities/backward_add_ptr.res.oracle
-12c12
-< Frama_C_show_each_only_a: {0; 1}, {{ &a }}, {0}
----
-> Frama_C_show_each_only_a: {0}, {{ &a }}, {0}
-93c93,96
-< [eva] tests/value/backward_add_ptr.c:110: Reusing old results for call to gm
----
-> [eva] computing for function gm <- main3 <- main.
-> Called from tests/value/backward_add_ptr.c:110.
-> [eva] Recording results for gm
-> [eva] Done for function gm
-107c110,113
-< [eva] tests/value/backward_add_ptr.c:125: Reusing old results for call to gm
----
-> [eva] computing for function gm <- main3 <- main.
-> Called from tests/value/backward_add_ptr.c:125.
-> [eva] Recording results for gm
-> [eva] Done for function gm
-119c125
-< (origin: Arithmetic {tests/value/backward_add_ptr.c:68}) }},
----
-> (origin: Arithmetic Bottom) }},
-157,160c163,167
-< {{ garbled mix of &{b}
-< (origin: Arithmetic {tests/value/backward_add_ptr.c:68}) }},
-< [0..4294967295]
-< [eva] tests/value/backward_add_ptr.c:160: Reusing old results for call to gm
----
-> {{ garbled mix of &{b} (origin: Arithmetic Bottom) }}, [0..4294967295]
-> [eva] computing for function gm <- main4 <- main.
-> Called from tests/value/backward_add_ptr.c:160.
-> [eva] Recording results for gm
-> [eva] Done for function gm
-178c185
-< (origin: Arithmetic {tests/value/backward_add_ptr.c:68}) }},
----
-> (origin: Arithmetic Bottom) }},
-180c187
-< (origin: Arithmetic {tests/value/backward_add_ptr.c:68}) }}
----
-> (origin: Arithmetic Bottom) }}
-188c195
-< (origin: Arithmetic {tests/value/backward_add_ptr.c:68}) }}
----
-> (origin: Arithmetic Bottom) }}
-194c201
-< (origin: Arithmetic {tests/value/backward_add_ptr.c:68}) }},
----
-> (origin: Arithmetic Bottom) }},
-211a219,222
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:33}) }}
-> {{ garbled mix of &{a}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:33}) }}
-> {{ garbled mix of &{b}
-232a244,245
-> {{ garbled mix of &{a; b}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:106}) }}
-234a248,251
-> {{ garbled mix of &{a; b}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:107}) }}
-> {{ garbled mix of &{a; b}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:115}) }}
-238c255,257
-< (origin: Arithmetic {tests/value/backward_add_ptr.c:115}) }}
----
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:116}) }}
-> {{ garbled mix of &{a; b}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:121}) }}
-240a260,263
-> {{ garbled mix of &{a; b}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:122}) }}
-> {{ garbled mix of &{a; b}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:130}) }}
-242a266,267
-> {{ garbled mix of &{a; b}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:136}) }}
-245a271,272
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:137}) }}
-> {{ garbled mix of &{a; b}
-246a274,275
-> {{ garbled mix of &{a; b}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:145}) }}
-248a278,285
-> {{ garbled mix of &{a; b}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:150}) }}
-> {{ garbled mix of &{a; b}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:151}) }}
-> {{ garbled mix of &{a; b}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:156}) }}
-> {{ garbled mix of &{a; b}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:157}) }}
-250a288,311
-> {{ garbled mix of &{a; b}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:165}) }}
-> {{ garbled mix of &{b; c}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:165}) }}
-> {{ garbled mix of &{a; b}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:166}) }}
-> {{ garbled mix of &{b; c}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:166}) }}
-> {{ garbled mix of &{a; b}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:171}) }}
-> {{ garbled mix of &{b; c}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:171}) }}
-> {{ garbled mix of &{a; b}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:172}) }}
-> {{ garbled mix of &{b; c}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:172}) }}
-> {{ garbled mix of &{a; b}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:177}) }}
-> {{ garbled mix of &{b; c}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:177}) }}
-> {{ garbled mix of &{a; b}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:178}) }}
-> {{ garbled mix of &{b; c}
-> (origin: Arithmetic {tests/value/backward_add_ptr.c:178}) }}
-diff tests/value/oracle/bitfield.res.oracle tests/value/oracle_equalities/bitfield.res.oracle
-138a139,141
-> [eva] tests/value/bitfield.i:71:
-> Frama_C_show_each:
-> {{ garbled mix of &{b} (origin: Misaligned {tests/value/bitfield.i:70}) }}
-diff tests/value/oracle/bitwise_pointer.res.oracle tests/value/oracle_equalities/bitwise_pointer.res.oracle
-62c62
-< x ∈ [0..9]
----
-> x ∈ {5}
-75c75
-< x1 ∈ [0..9]
----
-> x1 ∈ {5}
-diff tests/value/oracle/call_simple.res.oracle tests/value/oracle_equalities/call_simple.res.oracle
-28c28
-< c ∈ [--..--]
----
-> c ∈ [-2147483648..2147483646]
-diff tests/value/oracle/case_analysis.res.oracle tests/value/oracle_equalities/case_analysis.res.oracle
-11a12,15
-> [eva] tests/value/case_analysis.i:18:
-> The evaluation of the expression r * r
-> led to bottom without alarms:
-> at this point the product of states has no possible concretization.
-18c22
-< rq ∈ [-0.0000000000000000 .. 100.0000000000000000]
----
-> rq ∈ [0.0000000000000000 .. 100.0000000000000000]
-diff tests/value/oracle/descending.res.oracle tests/value/oracle_equalities/descending.res.oracle
-42c42
-< i ∈ {31; 32}
----
-> i ∈ {31}
-diff tests/value/oracle/domains_function.res.oracle tests/value/oracle_equalities/domains_function.res.oracle
-19,20c19
-< [eva] tests/value/domains_function.c:92:
-< Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] tests/value/domains_function.c:92: Frama_C_show_each_top: {3}
-28,29c27
-< [eva] tests/value/domains_function.c:77:
-< Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] tests/value/domains_function.c:77: Frama_C_show_each_top: {1}
-32,33c30
-< [eva] tests/value/domains_function.c:96:
-< Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] tests/value/domains_function.c:96: Frama_C_show_each_top: {1}
-36,37c33
-< [eva] tests/value/domains_function.c:84:
-< Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] tests/value/domains_function.c:84: Frama_C_show_each_top: {2}
-40,41c36
-< [eva] tests/value/domains_function.c:98:
-< Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] tests/value/domains_function.c:98: Frama_C_show_each_top: {2}
-60,61c55
-< [eva] tests/value/domains_function.c:84:
-< Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] tests/value/domains_function.c:84: Frama_C_show_each_top: {2}
-64,65c58
-< [eva] tests/value/domains_function.c:113:
-< Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] tests/value/domains_function.c:113: Frama_C_show_each_top: {2}
-78,79c71
-< [eva] tests/value/domains_function.c:55:
-< Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] tests/value/domains_function.c:55: Frama_C_show_each_top: {42}
-108,109c100
-< [eva] tests/value/domains_function.c:64:
-< Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] tests/value/domains_function.c:64: Frama_C_show_each_top: {42}
-116c107
-< result ∈ [--..--]
----
-> result ∈ {2}
-130c121
-< result ∈ [--..--]
----
-> result ∈ {1}
-135c126
-< result ∈ [--..--]
----
-> result ∈ {2}
-138c129
-< result ∈ [--..--]
----
-> result ∈ {2}
-diff tests/value/oracle/downcast.2.res.oracle tests/value/oracle_equalities/downcast.2.res.oracle
-114c114
-< ux ∈ [--..--]
----
-> ux ∈ [0..65535]
-157c157
-< ux ∈ [--..--]
----
-> ux ∈ [0..65535]
-diff tests/value/oracle/fptr.1.res.oracle tests/value/oracle_equalities/fptr.1.res.oracle
-55,57d54
-< [eva] tests/value/fptr.i:67:
-< Frama_C_show_each_F: {{ NULL + [0..4294967295] ; &h ; &hh }}
-< [eva] tests/value/fptr.i:68: Reusing old results for call to f
-69c66
-< n ∈ {0; 1; 2}
----
-> n ∈ {0; 1}
-diff tests/value/oracle/from_call.0.res.oracle tests/value/oracle_equalities/from_call.0.res.oracle
-68c68,73
-< [eva] tests/value/from_call.i:20: Reusing old results for call to g
----
-> [eva] computing for function g <- f <- main.
-> Called from tests/value/from_call.i:20.
-> [eva] Recording results for g
-> [from] Computing for function g
-> [from] Done for function g
-> [eva] Done for function g
-78c83,88
-< [eva] tests/value/from_call.i:20: Reusing old results for call to g
----
-> [eva] computing for function g <- f <- main.
-> Called from tests/value/from_call.i:20.
-> [eva] Recording results for g
-> [from] Computing for function g
-> [from] Done for function g
-> [eva] Done for function g
-diff tests/value/oracle/from_call.1.res.oracle tests/value/oracle_equalities/from_call.1.res.oracle
-64c64,67
-< [eva] tests/value/from_call.i:20: Reusing old results for call to g
----
-> [eva] computing for function g <- f <- main.
-> Called from tests/value/from_call.i:20.
-> [eva] Recording results for g
-> [eva] Done for function g
-72c75,78
-< [eva] tests/value/from_call.i:20: Reusing old results for call to g
----
-> [eva] computing for function g <- f <- main.
-> Called from tests/value/from_call.i:20.
-> [eva] Recording results for g
-> [eva] Done for function g
-diff tests/value/oracle/from_termin.res.oracle tests/value/oracle_equalities/from_termin.res.oracle
-9a10
-> [eva] tests/value/from_termin.i:8: starting to merge loop iterations
-diff tests/value/oracle/imprecise_invalid_write.res.oracle tests/value/oracle_equalities/imprecise_invalid_write.res.oracle
-29a30,31
-> [kernel] tests/value/imprecise_invalid_write.i:9:
-> imprecise size for variable main1 (Undefined sizeof on a function.)
-diff tests/value/oracle/incompatible_states.res.oracle tests/value/oracle_equalities/incompatible_states.res.oracle
-14a15,18
-> [eva] tests/value/incompatible_states.c:24:
-> The evaluation of the expression x * x
-> led to bottom without alarms:
-> at this point the product of states has no possible concretization.
-27,29c31,34
-< [eva:alarm] tests/value/incompatible_states.c:41: Warning:
-< accessing uninitialized left-value.
-< assert \initialized(&t[(int)((int)(2 * i) / 2)]);
----
-> [eva] tests/value/incompatible_states.c:41:
-> The evaluation of the expression t[(2 * i) / 2]
-> led to bottom without alarms:
-> at this point the product of states has no possible concretization.
-41,42d45
-< [eva:alarm] tests/value/incompatible_states.c:53: Warning:
-< division by zero. assert t[i] ≢ 0;
-47,49d49
-< [eva] tests/value/incompatible_states.c:41:
-< assertion 'Eva,initialization' got final status invalid.
-< [scope:rm_asserts] removing 2 assertion(s)
-55c55
-< z ∈ [-3..100]
----
-> z ∈ {-3; -2}
-58c58
-< t[0] ∈ {0; 1}
----
-> t[0] ∈ {0}
-diff tests/value/oracle/library.res.oracle tests/value/oracle_equalities/library.res.oracle
-129,132d128
-< [eva:alarm] tests/value/library.i:44: Warning:
-< non-finite float value. assert \is_finite(*pf);
-< [eva:alarm] tests/value/library.i:44: Warning:
-< non-finite float value. assert \is_finite(\add_float(*pf, *pf));
-diff tests/value/oracle/long_const.0.res.oracle tests/value/oracle_equalities/long_const.0.res.oracle
-19c19,22
-< [eva] tests/value/long_const.i:25: Reusing old results for call to LL_ABS
----
-> [eva] computing for function LL_ABS <- div64 <- main.
-> Called from tests/value/long_const.i:25.
-> [eva] Recording results for LL_ABS
-> [eva] Done for function LL_ABS
-diff tests/value/oracle/long_const.1.res.oracle tests/value/oracle_equalities/long_const.1.res.oracle
-19c19,22
-< [eva] tests/value/long_const.i:25: Reusing old results for call to LL_ABS
----
-> [eva] computing for function LL_ABS <- div64 <- main.
-> Called from tests/value/long_const.i:25.
-> [eva] Recording results for LL_ABS
-> [eva] Done for function LL_ABS
-diff tests/value/oracle/modulo.res.oracle tests/value/oracle_equalities/modulo.res.oracle
-40a41,119
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [-9..-1], [-8..0]
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [1..9], [-8..0]
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [-9..-1], [0..8]
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [1..9], [0..8]
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> [-9..-1], {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {-8; -7; -6; -5; -4; -3; -2; -1},
-> {-7; -6; -5; -4; -3; -2; -1},
-> {-6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {-8; -7; -6; -5; -4; -3; -2; -1},
-> {1; 2; 3; 4; 5; 6; 7},
-> {-6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {1; 2; 3; 4; 5; 6; 7; 8}, {1; 2; 3; 4; 5; 6; 7}, {0; 1; 2; 3; 4; 5; 6}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {1; 2; 3; 4; 5; 6; 7}, {1; 2; 3; 4; 5; 6}, {0; 1; 2; 3; 4; 5}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {-7; -6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {1; 2; 3; 4; 5; 6; 7}, {-6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {-7; -6; -5; -4; -3; -2; -1},
-> {-6; -5; -4; -3; -2; -1},
-> {-5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {-6; -5; -4; -3; -2; -1}, {-5; -4; -3; -2; -1}, {-4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {-6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5}, {-4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1}, {0; 1; 2; 3; 4}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {1; 2; 3; 4; 5; 6}, {1; 2; 3; 4; 5}, {0; 1; 2; 3; 4}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {1; 2; 3; 4; 5}, {1; 2; 3; 4}, {0; 1; 2; 3}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {-5; -4; -3; -2; -1}, {1; 2; 3; 4}, {-3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {1; 2; 3; 4; 5}, {-4; -3; -2; -1}, {0; 1; 2; 3}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {-5; -4; -3; -2; -1}, {-4; -3; -2; -1}, {-3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {-4; -3; -2; -1}, {-3; -2; -1}, {-2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {-4; -3; -2; -1}, {1; 2; 3}, {-2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {1; 2; 3; 4}, {-3; -2; -1}, {0; 1; 2}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {1; 2; 3; 4}, {1; 2; 3}, {0; 1; 2}
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2; 3}, {1; 2}, {0; 1}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {-3; -2; -1}, {1; 2}, {-1; 0}
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2; 3}, {-2; -1}, {0; 1}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {-3; -2; -1}, {-2; -1}, {-1; 0}
-50a130,208
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [1..9], [-8..0]
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [-9..-1], [-8..0]
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [1..9], [0..8]
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [-9..-1], [0..8]
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> [-9..-1], {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {-8; -7; -6; -5; -4; -3; -2; -1},
-> {1; 2; 3; 4; 5; 6; 7},
-> {-6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {-8; -7; -6; -5; -4; -3; -2; -1},
-> {-7; -6; -5; -4; -3; -2; -1},
-> {-6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6; 7; 8}, {1; 2; 3; 4; 5; 6; 7}, {0; 1; 2; 3; 4; 5; 6}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {-7; -6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6; 7}, {1; 2; 3; 4; 5; 6}, {0; 1; 2; 3; 4; 5}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {-7; -6; -5; -4; -3; -2; -1},
-> {-6; -5; -4; -3; -2; -1},
-> {-5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6; 7}, {-6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {-6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5}, {-4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {-6; -5; -4; -3; -2; -1}, {-5; -4; -3; -2; -1}, {-4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {1; 2; 3; 4; 5; 6}, {1; 2; 3; 4; 5}, {0; 1; 2; 3; 4}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1}, {0; 1; 2; 3; 4}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {-5; -4; -3; -2; -1}, {1; 2; 3; 4}, {-3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {1; 2; 3; 4; 5}, {1; 2; 3; 4}, {0; 1; 2; 3}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {-5; -4; -3; -2; -1}, {-4; -3; -2; -1}, {-3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {1; 2; 3; 4; 5}, {-4; -3; -2; -1}, {0; 1; 2; 3}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {-4; -3; -2; -1}, {1; 2; 3}, {-2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {-4; -3; -2; -1}, {-3; -2; -1}, {-2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {1; 2; 3; 4}, {1; 2; 3}, {0; 1; 2}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {1; 2; 3; 4}, {-3; -2; -1}, {0; 1; 2}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {-3; -2; -1}, {1; 2}, {-1; 0}
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2; 3}, {1; 2}, {0; 1}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {-3; -2; -1}, {-2; -1}, {-1; 0}
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2; 3}, {-2; -1}, {0; 1}
-60a219,231
-> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-10..10], [-9..9], [-8..8]
-> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-9..9], [-8..8], [-7..7]
-> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-8..8], [-7..7], [-6..6]
-> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-7..7], [-6..6], [-5..5]
-> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-6..6], [-5..5], [-4..4]
-> [eva] tests/value/modulo.i:64:
-> Frama_C_show_each_3:
-> [-5..5], {-4; -3; -2; -1; 1; 2; 3; 4}, {-3; -2; -1; 0; 1; 2; 3}
-> [eva] tests/value/modulo.i:64:
-> Frama_C_show_each_3:
-> {-4; -3; -2; -1; 1; 2; 3; 4}, {-3; -2; -1; 1; 2; 3}, {-2; -1; 0; 1; 2}
-> [eva] tests/value/modulo.i:64:
-> Frama_C_show_each_3: {-3; -2; -1; 1; 2; 3}, {-2; -1; 1; 2}, {-1; 0; 1}
-diff tests/value/oracle/non_natural.res.oracle tests/value/oracle_equalities/non_natural.res.oracle
-58a59,60
-> [kernel] tests/value/non_natural.i:30:
-> more than 200(12500) elements to enumerate. Approximating.
-65a68,71
-> [kernel] tests/value/non_natural.i:23:
-> more than 200(12500) elements to enumerate. Approximating.
-> [kernel] tests/value/non_natural.i:23:
-> more than 200(12501) elements to enumerate. Approximating.
-70a77,80
-> [kernel] tests/value/non_natural.i:24:
-> more than 200(12500) elements to enumerate. Approximating.
-> [kernel] tests/value/non_natural.i:24:
-> more than 200(12501) elements to enumerate. Approximating.
-78a89,90
-> [kernel] tests/value/non_natural.i:25:
-> more than 200(12500) elements to enumerate. Approximating.
-86a99,100
-> [kernel] tests/value/non_natural.i:26:
-> more than 200(12500) elements to enumerate. Approximating.
-94a109,110
-> [kernel] tests/value/non_natural.i:27:
-> more than 200(12500) elements to enumerate. Approximating.
-102a119,120
-> [kernel] tests/value/non_natural.i:28:
-> more than 200(12500) elements to enumerate. Approximating.
-110a129,130
-> [kernel] tests/value/non_natural.i:29:
-> more than 200(12500) elements to enumerate. Approximating.
-127,146d146
-< [kernel] tests/value/non_natural.i:23:
-< more than 200(12501) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:23:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:24:
-< more than 200(12501) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:24:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:25:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:26:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:27:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:28:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:29:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:30:
-< more than 200(12500) elements to enumerate. Approximating.
-199a200,201
-> [kernel] tests/value/non_natural.i:39:
-> more than 200(12500) elements to enumerate. Approximating.
-diff tests/value/oracle/nonlin.res.oracle tests/value/oracle_equalities/nonlin.res.oracle
-194c194
-< q ∈ {{ &x + [-400..400],0%4 }}
----
-> q ∈ {{ &x }}
-diff tests/value/oracle/octagons.res.oracle tests/value/oracle_equalities/octagons.res.oracle
-29c29
-< Frama_C_show_each_unreduced_unsigned: [0..4294967295], [0..4294967295]
----
-> Frama_C_show_each_unreduced_unsigned: [0..4294967295], [6..4294967295]
-255c255
-< t ∈ [--..--] or UNINITIALIZED
----
-> t ∈ [6..4294967295] or UNINITIALIZED
-diff tests/value/oracle/offsetmap.0.res.oracle tests/value/oracle_equalities/offsetmap.0.res.oracle
-40d39
-< [eva] Recording results for g
-42a42
-> [eva] Recording results for g
-diff tests/value/oracle/offsetmap.1.res.oracle tests/value/oracle_equalities/offsetmap.1.res.oracle
-40d39
-< [eva] Recording results for g
-42a42
-> [eva] Recording results for g
-diff tests/value/oracle/origin.0.res.oracle tests/value/oracle_equalities/origin.0.res.oracle
-249,250c249
-< pm2[bits 0 to 15]# ∈ {{ (? *)&a }}%32, bits 16 to 31
-< [bits 16 to 31]# ∈ {{ (? *)&b }}%32, bits 0 to 15
----
-> pm2 ∈ {{ &a + {-4} ; &b + {-4} }}
-289,290c288
-< pm2[bits 0 to 15]# ∈ {{ (? *)&a }}%32, bits 16 to 31
-< [bits 16 to 31]# ∈ {{ (? *)&b }}%32, bits 0 to 15
----
-> pm2 ∈ {{ &a + {-4} ; &b + {-4} }}
-diff tests/value/oracle/period.res.oracle tests/value/oracle_equalities/period.res.oracle
-88,94d87
-< [eva:alarm] tests/value/period.c:53: Warning:
-< pointer downcast. assert (unsigned int)(&g) ≤ 2147483647;
-< [eva] tests/value/period.c:53:
-< Assigning imprecise value to p.
-< The imprecision originates from Arithmetic {tests/value/period.c:53}
-< [eva:alarm] tests/value/period.c:54: Warning:
-< out of bounds read. assert \valid_read(p);
-99d91
-< [scope:rm_asserts] removing 1 assertion(s)
-diff tests/value/oracle/plevel.res.oracle tests/value/oracle_equalities/plevel.res.oracle
-12d11
-< [eva] Recording results for main
-14a14
-> [eva] Recording results for main
-diff tests/value/oracle/pointer_comp.res.oracle tests/value/oracle_equalities/pointer_comp.res.oracle
-30a31,34
-> [kernel] tests/value/pointer_comp.c:43:
-> imprecise size for variable g (Undefined sizeof on a function.)
-> [kernel] tests/value/pointer_comp.c:43:
-> imprecise size for variable f (Undefined sizeof on a function.)
-diff tests/value/oracle/ptr_relation.0.res.oracle tests/value/oracle_equalities/ptr_relation.0.res.oracle
-23c23
-< i ∈ {0; 77; 333}
----
-> i ∈ {77}
-diff tests/value/oracle/redundant_alarms.res.oracle tests/value/oracle_equalities/redundant_alarms.res.oracle
-10,13d9
-< [eva:alarm] tests/value/redundant_alarms.c:11: Warning:
-< accessing uninitialized left-value. assert \initialized(p);
-< [eva:alarm] tests/value/redundant_alarms.c:12: Warning:
-< accessing uninitialized left-value. assert \initialized(p);
-24,25d19
-< [eva:alarm] tests/value/redundant_alarms.c:21: Warning:
-< accessing uninitialized left-value. assert \initialized(&t[i]);
-63,65c57
-< [scope:rm_asserts] removing 3 assertion(s)
-< [scope:rm_asserts] tests/value/redundant_alarms.c:12:
-< removing redundant assert Eva: initialization: \initialized(p);
----
-> [scope:rm_asserts] removing 2 assertion(s)
-108d99
-< /*@ assert Eva: initialization: \initialized(p); */
-110d100
-< /*@ assert Eva: initialization: \initialized(p); */
-127d116
-< /*@ assert Eva: initialization: \initialized(&t[i]); */
-196a186
-> int z;
-199,201d188
-< *p = 1;
-< int z = *p + 1;
-< int w = *p + 2;
-diff tests/value/oracle/relation_reduction.res.oracle tests/value/oracle_equalities/relation_reduction.res.oracle
-24,27d23
-< [eva:alarm] tests/value/relation_reduction.i:20: Warning:
-< accessing out of bounds index. assert 0 ≤ y;
-< [eva:alarm] tests/value/relation_reduction.i:20: Warning:
-< accessing out of bounds index. assert y < 9;
-34,37c30,33
-< R1 ∈ [-2147483648..2147483637]
-< R2 ∈ [-2147483638..2147483647]
-< R3 ∈ [--..--]
-< R4 ∈ {0; 1; 2; 3; 4; 5}
----
-> R1 ∈ {0; 2}
-> R2 ∈ {0; 12}
-> R3 ∈ {0; 7}
-> R4 ∈ {0; 2}
-48c44
-< R4 FROM tab[0..8]; x (and SELF)
----
-> R4 FROM tab[0..5]; x (and SELF)
-53c49
-< y; t; tab[0..8]
----
-> y; t; tab[0..5]
-diff tests/value/oracle/relation_shift.res.oracle tests/value/oracle_equalities/relation_shift.res.oracle
-35,36c35,36
-< x ∈ [-2147483647..2147483647]
-< y ∈ [-2147483648..2147483646]
----
-> x ∈ [-2147483647..2147483642]
-> y ∈ [-2147483648..2147483645]
-53,54c53,54
-< x ∈ [-2147483647..2147483647]
-< y ∈ [-2147483648..2147483646]
----
-> x ∈ [-2147483647..2147483642]
-> y ∈ [-2147483648..2147483645]
-diff tests/value/oracle/relations.res.oracle tests/value/oracle_equalities/relations.res.oracle
-60,61c60
-< u[0] ∈ [-2147483648..2147483646]
-< [1] ∈ [--..--]
----
-> u[0..1] ∈ [-2147483648..2147483646]
-67,70c66,69
-< R1 ∈ [--..--]
-< R2 ∈ [--..--]
-< R3 ∈ [-2147483648..2147483646]
-< R4 ∈ [--..--]
----
-> R1 ∈ {0; 3}
-> R2 ∈ {0; 3}
-> R3 ∈ {0; 2}
-> R4 ∈ {0; 2}
-diff tests/value/oracle/relations2.res.oracle tests/value/oracle_equalities/relations2.res.oracle
-59c59
-< n ∈ [0..512]
----
-> n ∈ [1..512]
-133d132
-< [eva] tests/value/relations2.i:57: Frama_C_show_each_NO2:
-diff tests/value/oracle/struct2.res.oracle tests/value/oracle_equalities/struct2.res.oracle
-55a56,57
-> [kernel] tests/value/struct2.i:78: Warning:
-> all target addresses were invalid. This path is assumed to be dead.
-59,60d60
-< accessing out of bounds index. assert 0 ≤ (int)(tab2[i] + j);
-< [eva:alarm] tests/value/struct2.i:82: Warning:
-83,84d82
-< accessing out of bounds index. assert (int)(i + j) < 2;
-< [eva:alarm] tests/value/struct2.i:185: Warning:
-106c104
-< [scope:rm_asserts] removing 2 assertion(s)
----
-> [scope:rm_asserts] removing 1 assertion(s)
-143,145c141,143
-< tab3[0..1] ∈ [--..--]
-< tab4[0] ∈ {0; 2}
-< [1] ∈ {0}
----
-> tab3[0] ∈ {0; 1}
-> [1] ∈ [--..--]
-> tab4[0..1] ∈ {0}
-148c146,147
-< tab6[0..1] ∈ {0; 2}
----
-> tab6[0] ∈ {0}
-> [1] ∈ {2}
-219c218
-< [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0..1];
----
-> [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0];
-Only in tests/value/oracle: unit_tests.res.oracle
diff --git a/tests/value/diff_gauges b/tests/value/diff_gauges
deleted file mode 100644
index f6010fb62ca..00000000000
--- a/tests/value/diff_gauges
+++ /dev/null
@@ -1,1284 +0,0 @@
-diff tests/value/oracle/alias.5.res.oracle tests/value/oracle_gauges/alias.5.res.oracle
-59a60
-> [eva] tests/value/alias.i:260: starting to merge loop iterations
-diff tests/value/oracle/auto_loop_unroll.0.res.oracle tests/value/oracle_gauges/auto_loop_unroll.0.res.oracle
-11,13c11
-< [eva:alarm] tests/value/auto_loop_unroll.c:25: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:27: Frama_C_show_each_auto: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:27: Frama_C_show_each_auto: {100}
-15,18c13
-< [eva:alarm] tests/value/auto_loop_unroll.c:31: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:33:
-< Frama_C_show_each_imprecise: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:33: Frama_C_show_each_imprecise: {1000}
-20,23c15
-< [eva:alarm] tests/value/auto_loop_unroll.c:39: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:41:
-< Frama_C_show_each_imprecise: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:41: Frama_C_show_each_imprecise: {100}
-32,34c24
-< [eva:alarm] tests/value/auto_loop_unroll.c:58: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:59: Frama_C_show_each_64: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:59: Frama_C_show_each_64: {64}
-36,38c26
-< [eva:alarm] tests/value/auto_loop_unroll.c:63: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:64: Frama_C_show_each_40: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:64: Frama_C_show_each_40: {40}
-40,42c28
-< [eva:alarm] tests/value/auto_loop_unroll.c:69: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:72: Frama_C_show_each_80: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:72: Frama_C_show_each_80: {80}
-44,47c30
-< [eva:alarm] tests/value/auto_loop_unroll.c:76: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:82:
-< Frama_C_show_each_32_80: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:82: Frama_C_show_each_32_80: [32..83]
-55,56d37
-< [eva:alarm] tests/value/auto_loop_unroll.c:88: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-58c39
-< Frama_C_show_each_40_50: [0..2147483647]
----
-> Frama_C_show_each_40_50: [40..1073741861]
-133,136c114
-< [eva:alarm] tests/value/auto_loop_unroll.c:120: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:122:
-< Frama_C_show_each_32_64: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:122: Frama_C_show_each_32_64: [32..65]
-185,188c163
-< [eva:alarm] tests/value/auto_loop_unroll.c:173: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:175:
-< Frama_C_show_each_imprecise: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:175: Frama_C_show_each_imprecise: [1..9]
-190,191d164
-< [eva:alarm] tests/value/auto_loop_unroll.c:181: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-195c168
-< Frama_C_show_each_imprecise: [0..2147483647]
----
-> Frama_C_show_each_imprecise: [64..2147483647]
-201,203c174
-< [eva:alarm] tests/value/auto_loop_unroll.c:193: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:195: Frama_C_show_each_11: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:195: Frama_C_show_each_11: {11}
-205,207c176
-< [eva:alarm] tests/value/auto_loop_unroll.c:198: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:200: Frama_C_show_each_12: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:200: Frama_C_show_each_12: {12}
-209,210d177
-< [eva:alarm] tests/value/auto_loop_unroll.c:204: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-212a180,181
-> [eva:alarm] tests/value/auto_loop_unroll.c:204: Warning:
-> signed overflow. assert res + 1 ≤ 2147483647;
-216,217d184
-< [eva:alarm] tests/value/auto_loop_unroll.c:209: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-219a187,188
-> [eva:alarm] tests/value/auto_loop_unroll.c:209: Warning:
-> signed overflow. assert res + 1 ≤ 2147483647;
-223,224d191
-< [eva:alarm] tests/value/auto_loop_unroll.c:217: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-228,231c195
-< [eva:alarm] tests/value/auto_loop_unroll.c:222: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:226:
-< Frama_C_show_each_11_111: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:226: Frama_C_show_each_11_111: [11..111]
-239,241c203
-< [eva:alarm] tests/value/auto_loop_unroll.c:236: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:238: Frama_C_show_each_20: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:238: Frama_C_show_each_20: [20..2147483646]
-243,244d204
-< [eva:alarm] tests/value/auto_loop_unroll.c:241: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-247c207,209
-< [eva] tests/value/auto_loop_unroll.c:243: Frama_C_show_each_21: [0..2147483647]
----
-> [eva:alarm] tests/value/auto_loop_unroll.c:241: Warning:
-> signed overflow. assert res + 1 ≤ 2147483647;
-> [eva] tests/value/auto_loop_unroll.c:243: Frama_C_show_each_21: {21}
-253,255c215,216
-< [eva:alarm] tests/value/auto_loop_unroll.c:250: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:254: Frama_C_show_each_30: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:254: Frama_C_show_each_30: {30}
-> [eva] tests/value/auto_loop_unroll.c:258: starting to merge loop iterations
-258d218
-< [eva] tests/value/auto_loop_unroll.c:258: starting to merge loop iterations
-261,263c221
-< [eva:alarm] tests/value/auto_loop_unroll.c:267: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:272: Frama_C_show_each_32: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:272: Frama_C_show_each_32: {32}
-diff tests/value/oracle/auto_loop_unroll.1.res.oracle tests/value/oracle_gauges/auto_loop_unroll.1.res.oracle
-15,18c15
-< [eva:alarm] tests/value/auto_loop_unroll.c:31: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:33:
-< Frama_C_show_each_imprecise: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:33: Frama_C_show_each_imprecise: {1000}
-20,23c17
-< [eva:alarm] tests/value/auto_loop_unroll.c:39: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:41:
-< Frama_C_show_each_imprecise: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:41: Frama_C_show_each_imprecise: {100}
-329,332c323
-< [eva:alarm] tests/value/auto_loop_unroll.c:173: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-< [eva] tests/value/auto_loop_unroll.c:175:
-< Frama_C_show_each_imprecise: [0..2147483647]
----
-> [eva] tests/value/auto_loop_unroll.c:175: Frama_C_show_each_imprecise: [1..9]
-334,335d324
-< [eva:alarm] tests/value/auto_loop_unroll.c:181: Warning:
-< signed overflow. assert res + 1 ≤ 2147483647;
-339c328
-< Frama_C_show_each_imprecise: [0..2147483647]
----
-> Frama_C_show_each_imprecise: [64..2147483647]
-385a375,458
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 200 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 300 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 400 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 500 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 600 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 700 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 800 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 900 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 1000 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 1100 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 1200 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 1300 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 1400 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 1500 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 1600 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 1700 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 1800 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 1900 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 2000 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 2100 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 2200 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 2300 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 2400 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 2500 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 2600 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 2700 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 2800 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 2900 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 3000 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 3100 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 3200 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 3300 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 3400 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 3500 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 3600 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 3700 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 3800 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 3900 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 4000 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 4100 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 4200 states
-> [eva] tests/value/auto_loop_unroll.c:276:
-> Trace partitioning superposing up to 4300 states
-diff tests/value/oracle/bad_loop.res.oracle tests/value/oracle_gauges/bad_loop.res.oracle
-6a7
-> [eva] tests/value/bad_loop.i:12: starting to merge loop iterations
-diff tests/value/oracle/bitfield.res.oracle tests/value/oracle_gauges/bitfield.res.oracle
-138a139,153
-> [eva] tests/value/bitfield.i:71:
-> Frama_C_show_each:
-> {{ garbled mix of &{b} (origin: Misaligned {tests/value/bitfield.i:70}) }}
-> [eva] tests/value/bitfield.i:73:
-> Frama_C_show_each:
-> {{ garbled mix of &{b} (origin: Misaligned {tests/value/bitfield.i:70}) }}
-> [eva] computing for function leaf <- imprecise_bts_1671 <- main.
-> Called from tests/value/bitfield.i:70.
-> [eva] Done for function leaf
-> [eva] tests/value/bitfield.i:71:
-> Frama_C_show_each:
-> {{ garbled mix of &{b} (origin: Misaligned {tests/value/bitfield.i:70}) }}
-> [eva] tests/value/bitfield.i:73:
-> Frama_C_show_each:
-> {{ garbled mix of &{b} (origin: Misaligned {tests/value/bitfield.i:70}) }}
-diff tests/value/oracle/cast2.res.oracle tests/value/oracle_gauges/cast2.res.oracle
-26a27
-> [eva] tests/value/cast2.i:24: starting to merge loop iterations
-diff tests/value/oracle/for_loops.1.res.oracle tests/value/oracle_gauges/for_loops.1.res.oracle
-39,41c39
-< [eva:alarm] tests/value/for_loops.c:16: Warning:
-< signed overflow. assert w + 1 ≤ 2147483647;
-< [eva] tests/value/for_loops.c:17: Frama_C_show_each_F: [0..2147483647]
----
-> [eva] tests/value/for_loops.c:17: Frama_C_show_each_F: [0..100]
-diff tests/value/oracle/for_loops.2.res.oracle tests/value/oracle_gauges/for_loops.2.res.oracle
-37,39c37
-< [eva:alarm] tests/value/for_loops.c:42: Warning:
-< signed overflow. assert w + T[j] ≤ 2147483647;
-< [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/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
-diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.oracle
-25,26d24
-< [eva:alarm] tests/value/gauges.c:23: Warning:
-< signed overflow. assert -2147483648 ≤ j - 4;
-38,39d35
-< [eva:alarm] tests/value/gauges.c:26: Warning:
-< signed overflow. assert l + 1 ≤ 2147483647;
-57,58d52
-< [eva:alarm] tests/value/gauges.c:45: Warning:
-< signed overflow. assert -2147483648 ≤ j - 4;
-61a56,57
-> [eva:alarm] tests/value/gauges.c:45: Warning:
-> signed overflow. assert -2147483648 ≤ j - 4;
-70,71d65
-< [eva:alarm] tests/value/gauges.c:48: Warning:
-< signed overflow. assert l + 1 ≤ 2147483647;
-83,84d76
-< [eva:alarm] tests/value/gauges.c:58: Warning:
-< accessing out of bounds index. assert j < 38;
-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:
-113,114d99
-< [eva:alarm] tests/value/gauges.c:81: Warning:
-< signed overflow. assert k + 1 ≤ 2147483647;
-116,117d100
-< [eva:alarm] tests/value/gauges.c:84: Warning:
-< signed overflow. assert k + 1 ≤ 2147483647;
-125c108
-< [eva] tests/value/gauges.c:86: Frama_C_show_each: [0..2147483647]
----
-> [eva] tests/value/gauges.c:86: Frama_C_show_each: {390}
-139,140d121
-< [eva:alarm] tests/value/gauges.c:99: Warning:
-< signed overflow. assert c + 1 ≤ 2147483647;
-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:
-< out of bounds write. assert \valid(p);
----
-> [eva] tests/value/gauges.c:129:
-> 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} }}
-187,188d167
-< [eva:alarm] tests/value/gauges.c:140: Warning:
-< signed overflow. assert j + 1 ≤ 2147483647;
-206,208d184
-< [eva:alarm] tests/value/gauges.c:158: Warning:
-< out of bounds write. assert \valid(tmp);
-< (tmp from p--)
-227,231c203,205
-< [eva] tests/value/gauges.c:172: Frama_C_show_each: [2147483646..4294967294]
-< [eva] tests/value/gauges.c:172: Frama_C_show_each: [1..4294967294]
-< [eva] tests/value/gauges.c:172: Frama_C_show_each: [1..4294967294]
-< [eva] tests/value/gauges.c:172: Frama_C_show_each: [1..4294967294]
-< [eva] tests/value/gauges.c:172: Frama_C_show_each: [1..4294967294]
----
-> [eva] tests/value/gauges.c:172: Frama_C_show_each: [2147483647..4294967294]
-> [eva] tests/value/gauges.c:172: Frama_C_show_each: [2147483647..4294967294]
-> [eva] tests/value/gauges.c:172: Frama_C_show_each: [2147483647..4294967294]
-235c209,210
-< [eva] tests/value/gauges.c:172: Frama_C_show_each: [1..4294967294]
----
-> [eva] tests/value/gauges.c:172: Frama_C_show_each: [2147483647..4294967294]
-> [eva] tests/value/gauges.c:172: Frama_C_show_each: [2147483647..4294967294]
-259,262d233
-< [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);
-270,275d240
-< [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++)
-303,304d267
-< [eva:alarm] tests/value/gauges.c:220: Warning:
-< signed overflow. assert -2147483648 ≤ n - 1;
-319,322c282
-< [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}
-328,329d287
-< [eva:alarm] tests/value/gauges.c:251: Warning:
-< signed overflow. assert j + 1 ≤ 2147483647;
-331c289
-< 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}
-337,340c295
-< [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}
-346,347d300
-< [eva:alarm] tests/value/gauges.c:274: Warning:
-< signed overflow. assert j + 1 ≤ 2147483647;
-349c302
-< 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}
-357,358d309
-< [eva:alarm] tests/value/gauges.c:293: Warning:
-< signed overflow. assert j + 1 ≤ 2147483647;
-360c311
-< Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..2147483647]
----
-> Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [99..119]
-422a374,377
-> # Gauges domain:
-> V: [{[ p -> {{ &x }}
-> i -> {1} ]}]
-> s398: λ(0)
-482a438,441
-> # Gauges domain:
-> V: [{[ i -> {1} ]}]
-> s398: λ([0 .. 1])
-> {[ i -> {1} ]}
-541a501,504
-> # Gauges domain:
-> V: [{[ i -> {1} ]}]
-> s398: λ([0 .. 2])
-> {[ i -> {1} ]}
-600a564,567
-> # Gauges domain:
-> V: [{[ i -> {1} ]}]
-> s398: λ([0 .. 10])
-> {[ i -> {1} ]}
-665a633,637
-> # Gauges domain:
-> V: [{[ p -> {{ &a }}
-> i -> {2} ]}]
-> s412: λ(0)
-> s411: λ(0)
-726a699,703
-> # Gauges domain:
-> V: [{[ i -> {2} ]}]
-> s412: λ(0)
-> s411: λ([0 .. 1])
-> {[ i -> {0} ]}
-728a706,833
-> [eva] tests/value/gauges.c:325:
-> Frama_C_dump_each:
-> # Cvalue domain:
-> __fc_heap_status ∈ [--..--]
-> __fc_random_counter ∈ [--..--]
-> __fc_rand_max ∈ {32767}
-> __fc_random48_init ∈ {0}
-> __fc_random48_counter[0..2] ∈ [--..--]
-> __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
-> __fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
-> [1] ∈ {{ NULL ; &S_1___fc_env[0] }}
-> [2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
-> __fc_mblen_state ∈ [--..--]
-> __fc_mbtowc_state ∈ [--..--]
-> __fc_wctomb_state ∈ [--..--]
-> v ∈ [--..--]
-> t[0..4] ∈ {0}
-> [5] ∈ [0..48],0%3
-> [6] ∈ {0}
-> [7] ∈ [0..48],0%3
-> [8] ∈ {0}
-> [9] ∈ [0..48],0%3
-> [10] ∈ {0}
-> [11] ∈ [0..48],0%3
-> [12] ∈ {0}
-> [13] ∈ [0..48],0%3
-> [14] ∈ {0}
-> [15] ∈ [0..48],0%3
-> [16] ∈ {0}
-> [17] ∈ [0..48],0%3
-> [18] ∈ {0}
-> [19] ∈ [0..48],0%3
-> [20] ∈ {0}
-> [21] ∈ [0..48],0%3
-> [22] ∈ {0}
-> [23] ∈ [0..48],0%3
-> [24] ∈ {0}
-> [25] ∈ [0..48],0%3
-> [26] ∈ {0}
-> [27] ∈ [0..48],0%3
-> [28] ∈ {0}
-> [29] ∈ [0..48],0%3
-> [30] ∈ {0}
-> [31] ∈ [0..48],0%3
-> [32] ∈ {0}
-> [33] ∈ [0..48],0%3
-> [34] ∈ {0}
-> [35] ∈ [0..48],0%3
-> [36] ∈ {0}
-> [37] ∈ [0..48],0%3
-> u[0..99] ∈ [0..100]
-> T[0..99] ∈ [--..--]
-> a ∈ {1}
-> b ∈ {0}
-> p ∈ {{ &a ; &b }}
-> i ∈ {2}
-> S_0___fc_env[0..1] ∈ [--..--]
-> S_1___fc_env[0..1] ∈ [--..--]
-> # Gauges domain:
-> V: [{[ i -> {2} ]}]
-> s412: λ(0)
-> s411: λ([0 .. 2])
-> {[ i -> {0} ]}
-> ==END OF DUMP==
-> [eva] tests/value/gauges.c:325:
-> Frama_C_dump_each:
-> # Cvalue domain:
-> __fc_heap_status ∈ [--..--]
-> __fc_random_counter ∈ [--..--]
-> __fc_rand_max ∈ {32767}
-> __fc_random48_init ∈ {0}
-> __fc_random48_counter[0..2] ∈ [--..--]
-> __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }}
-> __fc_env[0] ∈ {{ NULL ; &S_0___fc_env[0] }}
-> [1] ∈ {{ NULL ; &S_1___fc_env[0] }}
-> [2..4095] ∈ {{ NULL ; &S_0___fc_env[0] ; &S_1___fc_env[0] }}
-> __fc_mblen_state ∈ [--..--]
-> __fc_mbtowc_state ∈ [--..--]
-> __fc_wctomb_state ∈ [--..--]
-> v ∈ [--..--]
-> t[0..4] ∈ {0}
-> [5] ∈ [0..48],0%3
-> [6] ∈ {0}
-> [7] ∈ [0..48],0%3
-> [8] ∈ {0}
-> [9] ∈ [0..48],0%3
-> [10] ∈ {0}
-> [11] ∈ [0..48],0%3
-> [12] ∈ {0}
-> [13] ∈ [0..48],0%3
-> [14] ∈ {0}
-> [15] ∈ [0..48],0%3
-> [16] ∈ {0}
-> [17] ∈ [0..48],0%3
-> [18] ∈ {0}
-> [19] ∈ [0..48],0%3
-> [20] ∈ {0}
-> [21] ∈ [0..48],0%3
-> [22] ∈ {0}
-> [23] ∈ [0..48],0%3
-> [24] ∈ {0}
-> [25] ∈ [0..48],0%3
-> [26] ∈ {0}
-> [27] ∈ [0..48],0%3
-> [28] ∈ {0}
-> [29] ∈ [0..48],0%3
-> [30] ∈ {0}
-> [31] ∈ [0..48],0%3
-> [32] ∈ {0}
-> [33] ∈ [0..48],0%3
-> [34] ∈ {0}
-> [35] ∈ [0..48],0%3
-> [36] ∈ {0}
-> [37] ∈ [0..48],0%3
-> u[0..99] ∈ [0..100]
-> T[0..99] ∈ [--..--]
-> a ∈ {1}
-> b ∈ {0}
-> p ∈ {{ &a ; &b }}
-> i ∈ {2}
-> S_0___fc_env[0..1] ∈ [--..--]
-> S_1___fc_env[0..1] ∈ [--..--]
-> # Gauges domain:
-> V: [{[ i -> {2} ]}]
-> s412: λ(0)
-> s411: λ([0 .. +oo])
-> {[ i -> {0} ]}
-> ==END OF DUMP==
-736a842,843
-> [eva] tests/value/gauges.c:343: Call to builtin malloc
-> [eva] tests/value/gauges.c:343: Call to builtin malloc
-789,790c896,897
-< A ∈ {{ &A + [0..--],0%4 }}
-< B ∈ {{ &B + [0..--],0%4 }}
----
-> A ∈ {{ &A + [0..36],0%4 }}
-> B ∈ {{ &B + [0..36],0%4 }}
-802c909
-< n ∈ [-2147483648..99]
----
-> n ∈ [-2147483547..99]
-808c915
-< i ∈ {45; 46; 47; 48; 49; 50; 51}
----
-> i ∈ {45; 46; 47; 48}
-814c921
-< i ∈ {-59; -58; -57; -56; -55; -54; -53}
----
-> i ∈ {-58; -57; -56; -55; -54; -53}
-834c941
-< p ∈ {{ &u + [0..--],0%4 }}
----
-> p ∈ {{ &u + [0..400],0%4 }}
-836c943
-< k ∈ [0..2147483647]
----
-> k ∈ [0..390]
-841c948
-< i ∈ [0..2147483647]
----
-> i ∈ [0..21]
-852,853c959,961
-< [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] }}
-864c972
-< p ∈ {{ &T + [--..396],0%4 }}
----
-> p ∈ {{ &T + [-4..396],0%4 }}
-869,873c977
-< n ∈ {0}
-< arr[0] ∈ {0}
-< [1] ∈ {-1}
-< [2..65535] ∈ [--..--] or UNINITIALIZED
-< p ∈ {{ &arr + [12..--],0%4 }}
----
-> NON TERMINATING FUNCTION
-976a1081
-> [from] Non-terminating function main8_aux (no dependencies)
-999,1000c1104,1105
-< 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]
-1044c1149
-< NO EFFECTS
----
-> NON TERMINATING - NO EFFECTS
-1078c1183
-< p; A[0..9]; B[0..9]
----
-> p; A[0..8]; B[0..8]
-diff tests/value/oracle/hierarchical_convergence.res.oracle tests/value/oracle_gauges/hierarchical_convergence.res.oracle
-15a16
-> [eva] tests/value/hierarchical_convergence.c:10: Frama_C_show_each: {1}, {0}
-diff tests/value/oracle/infinite.res.oracle tests/value/oracle_gauges/infinite.res.oracle
-12a13,22
-> [eva] tests/value/infinite.i:6: starting to merge loop iterations
-> [eva] computing for function pause <- main.
-> Called from tests/value/infinite.i:9.
-> [eva] Done for function pause
-> [eva] computing for function pause <- main.
-> Called from tests/value/infinite.i:9.
-> [eva] Done for function pause
-> [eva] computing for function pause <- main.
-> Called from tests/value/infinite.i:9.
-> [eva] Done for function pause
-diff tests/value/oracle/inout.2.res.oracle tests/value/oracle_gauges/inout.2.res.oracle
-22a23
-> [eva] tests/value/inout.i:50: starting to merge loop iterations
-diff tests/value/oracle/inout.3.res.oracle tests/value/oracle_gauges/inout.3.res.oracle
-22a23
-> [eva] tests/value/inout.i:60: starting to merge loop iterations
-diff tests/value/oracle/inout.4.res.oracle tests/value/oracle_gauges/inout.4.res.oracle
-24a25
-> [eva] tests/value/inout.i:60: starting to merge loop iterations
-diff tests/value/oracle/local_slevel.res.oracle tests/value/oracle_gauges/local_slevel.res.oracle
-13,15c13,15
-< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {0; 1}
-< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {-1}, {0}, {0; 1}
-< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {0; 1; 2}
----
-> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {1}
-> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {-1}, {0}, {0}
-> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {1}
-18c18
-< Frama_C_show_each: {1}, [1..79],1%2, {0; 1; 2; 3}
----
-> Frama_C_show_each: {1}, [1..79],1%2, {1; 2; 3}
-22c22
-< Frama_C_show_each: {1}, [1..79],1%2, {0; 1; 2; 3; 4}
----
-> Frama_C_show_each: {1}, [1..79],1%2, {1; 2; 3; 4}
-26,34c26
-< Frama_C_show_each: {1}, [1..79],1%2, [0..2147483647]
-< [eva] tests/value/local_slevel.i:18:
-< Frama_C_show_each: {-1}, [0..78],0%2, [0..2147483647]
-< [eva] tests/value/local_slevel.i:18:
-< Frama_C_show_each: {1}, [1..79],1%2, [0..2147483648]
-< [eva] tests/value/local_slevel.i:18:
-< Frama_C_show_each: {-1}, [0..78],0%2, [0..2147483648]
-< [eva] tests/value/local_slevel.i:18:
-< Frama_C_show_each: {1}, [1..79],1%2, [0..4294967295]
----
-> Frama_C_show_each: {1}, [1..79],1%2, [1..79]
-36c28
-< Frama_C_show_each: {-1}, [0..78],0%2, [0..4294967295]
----
-> Frama_C_show_each: {-1}, [0..78],0%2, [0..78]
-152c144
-< r ∈ [--..--]
----
-> r ∈ [0..2147483647]
-393,395c385,387
-< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {0; 1}
-< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {-1}, {0}, {0; 1}
-< [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {0; 1; 2}
----
-> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {1}
-> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {-1}, {0}, {0}
-> [eva] tests/value/local_slevel.i:18: Frama_C_show_each: {1}, {1}, {1}
-398c390
-< Frama_C_show_each: {1}, [1..79],1%2, {0; 1; 2; 3}
----
-> Frama_C_show_each: {1}, [1..79],1%2, {1; 2; 3}
-402c394
-< Frama_C_show_each: {1}, [1..79],1%2, {0; 1; 2; 3; 4}
----
-> Frama_C_show_each: {1}, [1..79],1%2, {1; 2; 3; 4}
-406,414c398
-< Frama_C_show_each: {1}, [1..79],1%2, [0..2147483647]
-< [eva] tests/value/local_slevel.i:18:
-< Frama_C_show_each: {-1}, [0..78],0%2, [0..2147483647]
-< [eva] tests/value/local_slevel.i:18:
-< Frama_C_show_each: {1}, [1..79],1%2, [0..2147483648]
-< [eva] tests/value/local_slevel.i:18:
-< Frama_C_show_each: {-1}, [0..78],0%2, [0..2147483648]
-< [eva] tests/value/local_slevel.i:18:
-< Frama_C_show_each: {1}, [1..79],1%2, [0..4294967295]
----
-> Frama_C_show_each: {1}, [1..79],1%2, [1..79]
-416c400
-< Frama_C_show_each: {-1}, [0..78],0%2, [0..4294967295]
----
-> Frama_C_show_each: {-1}, [0..78],0%2, [0..78]
-532c516
-< r ∈ [--..--]
----
-> r ∈ [0..2147483647]
-diff tests/value/oracle/loop_no_var.res.oracle tests/value/oracle_gauges/loop_no_var.res.oracle
-6a7
-> [eva] tests/value/loop_no_var.i:3: starting to merge loop iterations
-diff tests/value/oracle/loop_wvar.1.res.oracle tests/value/oracle_gauges/loop_wvar.1.res.oracle
-27,28c27
-< [eva] tests/value/loop_wvar.i:71: Frama_C_show_each: [0..9], [0..17], [0..11]
-< [eva] tests/value/loop_wvar.i:71: Frama_C_show_each: [0..9], [0..18], [0..12]
----
-> [eva] tests/value/loop_wvar.i:71: Frama_C_show_each: [0..9], [0..9], [0..9]
-37,38c36,37
-< j ∈ [0..18]
-< k ∈ [0..12]
----
-> j ∈ [0..17]
-> k ∈ [0..11]
-diff tests/value/oracle/loopfun.1.res.oracle tests/value/oracle_gauges/loopfun.1.res.oracle
-9a10,12
-> [eva] tests/value/loopfun.i:23: starting to merge loop iterations
-> [eva:loop-unroll] tests/value/loopfun.i:25: loop not completely unrolled
-> [eva] tests/value/loopfun.i:25: starting to merge loop iterations
-11a15
-> [eva] tests/value/loopfun.i:26: starting to merge loop iterations
-13a18
-> [eva] tests/value/loopfun.i:27: starting to merge loop iterations
-diff tests/value/oracle/memexec.res.oracle tests/value/oracle_gauges/memexec.res.oracle
-101a102
-> [eva] tests/value/memexec.c:98: starting to merge loop iterations
-diff tests/value/oracle/modulo.res.oracle tests/value/oracle_gauges/modulo.res.oracle
-40a41,123
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [-9..-1], [-8..0]
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [1..9], [-8..0]
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [-9..-1], [0..8]
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [1..9], [0..8]
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> [-9..-1], {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {-8; -7; -6; -5; -4; -3; -2; -1},
-> {-7; -6; -5; -4; -3; -2; -1},
-> {-6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {-8; -7; -6; -5; -4; -3; -2; -1},
-> {1; 2; 3; 4; 5; 6; 7},
-> {-6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {1; 2; 3; 4; 5; 6; 7; 8}, {1; 2; 3; 4; 5; 6; 7}, {0; 1; 2; 3; 4; 5; 6}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {1; 2; 3; 4; 5; 6; 7}, {1; 2; 3; 4; 5; 6}, {0; 1; 2; 3; 4; 5}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {-7; -6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {1; 2; 3; 4; 5; 6; 7}, {-6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {-7; -6; -5; -4; -3; -2; -1},
-> {-6; -5; -4; -3; -2; -1},
-> {-5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {-6; -5; -4; -3; -2; -1}, {-5; -4; -3; -2; -1}, {-4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {-6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5}, {-4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1}, {0; 1; 2; 3; 4}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {1; 2; 3; 4; 5; 6}, {1; 2; 3; 4; 5}, {0; 1; 2; 3; 4}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {1; 2; 3; 4; 5}, {1; 2; 3; 4}, {0; 1; 2; 3}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {-5; -4; -3; -2; -1}, {1; 2; 3; 4}, {-3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {1; 2; 3; 4; 5}, {-4; -3; -2; -1}, {0; 1; 2; 3}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {-5; -4; -3; -2; -1}, {-4; -3; -2; -1}, {-3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {-4; -3; -2; -1}, {-3; -2; -1}, {-2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {-4; -3; -2; -1}, {1; 2; 3}, {-2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {1; 2; 3; 4}, {-3; -2; -1}, {0; 1; 2}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {1; 2; 3; 4}, {1; 2; 3}, {0; 1; 2}
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2; 3}, {1; 2}, {0; 1}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {-3; -2; -1}, {1; 2}, {-1; 0}
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2; 3}, {-2; -1}, {0; 1}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1: {-3; -2; -1}, {-2; -1}, {-1; 0}
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {-2; -1}, {-1}, {0}
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {-2; -1}, {1}, {0}
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2}, {-1}, {0}
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: {1; 2}, {1}, {0}
-50a134,216
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [1..9], [-8..0]
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [-9..-1], [-8..0]
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [1..9], [0..8]
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [-9..-1], [0..8]
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> [-9..-1], {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {-8; -7; -6; -5; -4; -3; -2; -1},
-> {1; 2; 3; 4; 5; 6; 7},
-> {-6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {-8; -7; -6; -5; -4; -3; -2; -1},
-> {-7; -6; -5; -4; -3; -2; -1},
-> {-6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6; 7; 8}, {1; 2; 3; 4; 5; 6; 7}, {0; 1; 2; 3; 4; 5; 6}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {-7; -6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6; 7}, {1; 2; 3; 4; 5; 6}, {0; 1; 2; 3; 4; 5}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {-7; -6; -5; -4; -3; -2; -1},
-> {-6; -5; -4; -3; -2; -1},
-> {-5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6; 7}, {-6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {-6; -5; -4; -3; -2; -1}, {1; 2; 3; 4; 5}, {-4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {-6; -5; -4; -3; -2; -1}, {-5; -4; -3; -2; -1}, {-4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {1; 2; 3; 4; 5; 6}, {1; 2; 3; 4; 5}, {0; 1; 2; 3; 4}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> {1; 2; 3; 4; 5; 6}, {-5; -4; -3; -2; -1}, {0; 1; 2; 3; 4}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {-5; -4; -3; -2; -1}, {1; 2; 3; 4}, {-3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {1; 2; 3; 4; 5}, {1; 2; 3; 4}, {0; 1; 2; 3}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {-5; -4; -3; -2; -1}, {-4; -3; -2; -1}, {-3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {1; 2; 3; 4; 5}, {-4; -3; -2; -1}, {0; 1; 2; 3}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {-4; -3; -2; -1}, {1; 2; 3}, {-2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {-4; -3; -2; -1}, {-3; -2; -1}, {-2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {1; 2; 3; 4}, {1; 2; 3}, {0; 1; 2}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {1; 2; 3; 4}, {-3; -2; -1}, {0; 1; 2}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {-3; -2; -1}, {1; 2}, {-1; 0}
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2; 3}, {1; 2}, {0; 1}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2: {-3; -2; -1}, {-2; -1}, {-1; 0}
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2; 3}, {-2; -1}, {0; 1}
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {-2; -1}, {1}, {0}
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {-2; -1}, {-1}, {0}
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2}, {1}, {0}
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: {1; 2}, {-1}, {0}
-60a227,240
-> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-10..10], [-9..9], [-8..8]
-> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-9..9], [-8..8], [-7..7]
-> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-8..8], [-7..7], [-6..6]
-> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-7..7], [-6..6], [-5..5]
-> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-6..6], [-5..5], [-4..4]
-> [eva] tests/value/modulo.i:64:
-> Frama_C_show_each_3:
-> [-5..5], {-4; -3; -2; -1; 1; 2; 3; 4}, {-3; -2; -1; 0; 1; 2; 3}
-> [eva] tests/value/modulo.i:64:
-> Frama_C_show_each_3:
-> {-4; -3; -2; -1; 1; 2; 3; 4}, {-3; -2; -1; 1; 2; 3}, {-2; -1; 0; 1; 2}
-> [eva] tests/value/modulo.i:64:
-> Frama_C_show_each_3: {-3; -2; -1; 1; 2; 3}, {-2; -1; 1; 2}, {-1; 0; 1}
-> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: {-2; -1; 1; 2}, {-1; 1}, {0}
-81a262,263
-> [eva] tests/value/modulo.i:95: starting to merge loop iterations
-> [eva] tests/value/modulo.i:82: starting to merge loop iterations
-diff tests/value/oracle/non_natural.res.oracle tests/value/oracle_gauges/non_natural.res.oracle
-60,63c60
-< Frama_C_show_each: {{ &p2 + [0..400000],0%32 }}
-< [eva:alarm] tests/value/non_natural.i:23: Warning:
-< out of bounds write. assert \valid(tmp);
-< (tmp from to++)
----
-> Frama_C_show_each: {{ &p2 + [0..399968],0%32 }}
-66,68d62
-< [eva:alarm] tests/value/non_natural.i:24: Warning:
-< out of bounds write. assert \valid(tmp_1);
-< (tmp_1 from to++)
-71,76d64
-< [eva:alarm] tests/value/non_natural.i:25: Warning:
-< out of bounds write. assert \valid(tmp_3);
-< (tmp_3 from to++)
-< [eva:alarm] tests/value/non_natural.i:25: Warning:
-< out of bounds read. assert \valid_read(tmp_4);
-< (tmp_4 from from++)
-79,84d66
-< [eva:alarm] tests/value/non_natural.i:26: Warning:
-< out of bounds write. assert \valid(tmp_5);
-< (tmp_5 from to++)
-< [eva:alarm] tests/value/non_natural.i:26: Warning:
-< out of bounds read. assert \valid_read(tmp_6);
-< (tmp_6 from from++)
-87,92d68
-< [eva:alarm] tests/value/non_natural.i:27: Warning:
-< out of bounds write. assert \valid(tmp_7);
-< (tmp_7 from to++)
-< [eva:alarm] tests/value/non_natural.i:27: Warning:
-< out of bounds read. assert \valid_read(tmp_8);
-< (tmp_8 from from++)
-95,100d70
-< [eva:alarm] tests/value/non_natural.i:28: Warning:
-< out of bounds write. assert \valid(tmp_9);
-< (tmp_9 from to++)
-< [eva:alarm] tests/value/non_natural.i:28: Warning:
-< out of bounds read. assert \valid_read(tmp_10);
-< (tmp_10 from from++)
-103,108d72
-< [eva:alarm] tests/value/non_natural.i:29: Warning:
-< out of bounds write. assert \valid(tmp_11);
-< (tmp_11 from to++)
-< [eva:alarm] tests/value/non_natural.i:29: Warning:
-< out of bounds read. assert \valid_read(tmp_12);
-< (tmp_12 from from++)
-111,125d74
-< [eva:alarm] tests/value/non_natural.i:30: Warning:
-< out of bounds write. assert \valid(tmp_13);
-< (tmp_13 from to++)
-< [eva:alarm] tests/value/non_natural.i:30: Warning:
-< out of bounds read. assert \valid_read(tmp_14);
-< (tmp_14 from from++)
-< [eva] tests/value/non_natural.i:22:
-< Frama_C_show_each: {{ &p2 + [0..400032],0%32 }}
-< [eva:alarm] tests/value/non_natural.i:23: Warning:
-< out of bounds read. assert \valid_read(tmp_0);
-< (tmp_0 from from++)
-< [eva:alarm] tests/value/non_natural.i:24: Warning:
-< out of bounds read. assert \valid_read(tmp_2);
-< (tmp_2 from from++)
-< [eva] tests/value/non_natural.i:22: Frama_C_show_each: {{ &p2 + [0..--],0%32 }}
-128,129d76
-< more than 200(12501) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:23:
-132,133d78
-< more than 200(12501) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:24:
-194,197c139
-< Frama_C_show_each: {{ &p2 + [0..400000],0%32 }}
-< [eva:alarm] tests/value/non_natural.i:39: Warning:
-< out of bounds write. assert \valid(tmp);
-< (tmp from to++)
----
-> Frama_C_show_each: {{ &p2 + [0..399968],0%32 }}
-200,202d141
-< [eva:alarm] tests/value/non_natural.i:40: Warning:
-< out of bounds write. assert \valid(tmp_1);
-< (tmp_1 from to++)
-205,210d143
-< [eva:alarm] tests/value/non_natural.i:41: Warning:
-< out of bounds write. assert \valid(tmp_3);
-< (tmp_3 from to++)
-< [eva:alarm] tests/value/non_natural.i:41: Warning:
-< out of bounds read. assert \valid_read(tmp_4);
-< (tmp_4 from from++)
-213,218d145
-< [eva:alarm] tests/value/non_natural.i:42: Warning:
-< out of bounds write. assert \valid(tmp_5);
-< (tmp_5 from to++)
-< [eva:alarm] tests/value/non_natural.i:42: Warning:
-< out of bounds read. assert \valid_read(tmp_6);
-< (tmp_6 from from++)
-221,226d147
-< [eva:alarm] tests/value/non_natural.i:43: Warning:
-< out of bounds write. assert \valid(tmp_7);
-< (tmp_7 from to++)
-< [eva:alarm] tests/value/non_natural.i:43: Warning:
-< out of bounds read. assert \valid_read(tmp_8);
-< (tmp_8 from from++)
-229,234d149
-< [eva:alarm] tests/value/non_natural.i:44: Warning:
-< out of bounds write. assert \valid(tmp_9);
-< (tmp_9 from to++)
-< [eva:alarm] tests/value/non_natural.i:44: Warning:
-< out of bounds read. assert \valid_read(tmp_10);
-< (tmp_10 from from++)
-237,242d151
-< [eva:alarm] tests/value/non_natural.i:45: Warning:
-< out of bounds write. assert \valid(tmp_11);
-< (tmp_11 from to++)
-< [eva:alarm] tests/value/non_natural.i:45: Warning:
-< out of bounds read. assert \valid_read(tmp_12);
-< (tmp_12 from from++)
-245,259d153
-< [eva:alarm] tests/value/non_natural.i:46: Warning:
-< out of bounds write. assert \valid(tmp_13);
-< (tmp_13 from to++)
-< [eva:alarm] tests/value/non_natural.i:46: Warning:
-< out of bounds read. assert \valid_read(tmp_14);
-< (tmp_14 from from++)
-< [eva] tests/value/non_natural.i:38:
-< Frama_C_show_each: {{ &p2 + [0..400032],0%32 }}
-< [eva:alarm] tests/value/non_natural.i:39: Warning:
-< out of bounds read. assert \valid_read(tmp_0);
-< (tmp_0 from from++)
-< [eva:alarm] tests/value/non_natural.i:40: Warning:
-< out of bounds read. assert \valid_read(tmp_2);
-< (tmp_2 from from++)
-< [eva] tests/value/non_natural.i:38: Frama_C_show_each: {{ &p2 + [0..--],0%32 }}
-268,269c162,163
-< to ∈ {{ &p2 + [32..--],0%32 }}
-< from ∈ {{ &p1 + [32..--],0%32 }}
----
-> to ∈ {{ &p2 + [32..400000],0%32 }}
-> from ∈ {{ &p1 + [32..400000],0%32 }}
-273,274c167,168
-< to ∈ {{ &p2 + [32..--],0%32 }}
-< from ∈ {{ &p1 + [32..--],0%32 }}
----
-> to ∈ {{ &p2 + [32..400000],0%32 }}
-> from ∈ {{ &p1 + [32..400000],0%32 }}
-330,332c224,232
-< p2[0] FROM to; from; count; p1[0..100000] (and SELF)
-< [1..99992] FROM to; from; count; p1[0..100001] (and SELF)
-< [99993] FROM to; from; count; p1[1..100001] (and SELF)
----
-> p2[0] FROM to; from; count; p1[0..99992] (and SELF)
-> [1] FROM to; from; count; p1[0..99993] (and SELF)
-> [2] FROM to; from; count; p1[0..99994] (and SELF)
-> [3] FROM to; from; count; p1[0..99995] (and SELF)
-> [4] FROM to; from; count; p1[0..99996] (and SELF)
-> [5] FROM to; from; count; p1[0..99997] (and SELF)
-> [6] FROM to; from; count; p1[0..99998] (and SELF)
-> [7..99992] FROM to; from; count; p1[0..99999] (and SELF)
-> [99993] FROM to; from; count; p1[1..99999] (and SELF)
-340,342c240,248
-< p2[0] FROM to; from; count; p1[0..100000] (and SELF)
-< [1..99992] FROM to; from; count; p1[0..100001] (and SELF)
-< [99993] FROM to; from; count; p1[1..100001] (and SELF)
----
-> p2[0] FROM to; from; count; p1[0..99992] (and SELF)
-> [1] FROM to; from; count; p1[0..99993] (and SELF)
-> [2] FROM to; from; count; p1[0..99994] (and SELF)
-> [3] FROM to; from; count; p1[0..99995] (and SELF)
-> [4] FROM to; from; count; p1[0..99996] (and SELF)
-> [5] FROM to; from; count; p1[0..99997] (and SELF)
-> [6] FROM to; from; count; p1[0..99998] (and SELF)
-> [7..99992] FROM to; from; count; p1[0..99999] (and SELF)
-> [99993] FROM to; from; count; p1[1..99999] (and SELF)
-360c266
-< p1[0..100001]
----
-> p1[0..99999]
-365c271
-< p1[0..100001]
----
-> p1[0..99999]
-diff tests/value/oracle/noreturn.res.oracle tests/value/oracle_gauges/noreturn.res.oracle
-8a9
-> [eva] tests/value/noreturn.i:20: starting to merge loop iterations
-16a18
-> [eva] tests/value/noreturn.i:16: starting to merge loop iterations
-32a35
-> [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/octagons.res.oracle tests/value/oracle_gauges/octagons.res.oracle
-121,128d120
-< [eva:alarm] tests/value/octagons.c:107: Warning:
-< signed overflow. assert a + 2 ≤ 2147483647;
-< [eva:alarm] tests/value/octagons.c:108: Warning:
-< signed overflow. assert b + 2 ≤ 2147483647;
-< [eva:alarm] tests/value/octagons.c:110: Warning:
-< signed overflow. assert a + k ≤ 2147483647;
-< [eva:alarm] tests/value/octagons.c:113: Warning:
-< signed overflow. assert -2147483648 ≤ c - a;
-130c122
-< [eva] tests/value/octagons.c:116: Frama_C_show_each_imprecise: [-2147483648..1]
----
-> [eva] tests/value/octagons.c:116: Frama_C_show_each_imprecise: [-2468..1]
-270,273c262,265
-< a ∈ [-1024..2147483647]
-< b ∈ [-1023..2147483647]
-< c ∈ [-1023..2147483647]
-< d ∈ [-1032..2147483647]
----
-> a ∈ [-182..1866]
-> b ∈ [-181..1867]
-> c ∈ [-602..1446]
-> d ∈ [-190..1874]
-275c267
-< d2 ∈ [-2147483648..1]
----
-> d2 ∈ [-2468..1]
-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
-diff tests/value/oracle/redundant_alarms.res.oracle tests/value/oracle_gauges/redundant_alarms.res.oracle
-47a48
-> [eva] tests/value/redundant_alarms.c:39: starting to merge loop iterations
-diff tests/value/oracle/reevaluate_alarms.res.oracle tests/value/oracle_gauges/reevaluate_alarms.res.oracle
-14,16d13
-< [eva:alarm] tests/value/reevaluate_alarms.i:14: Warning:
-< out of bounds write. assert \valid(tmp);
-< (tmp from p++)
-59c56
-< p ∈ {{ &T + [0..--],0%4 }}
----
-> p ∈ {{ &T{[0], [1], [2], [3], [4], [5]} }}
-124,125d120
-< [ - ] Assertion 'Eva,mem_access' (file tests/value/reevaluate_alarms.i, line 14)
-< tried with Eva.
-144,145c139,140
-< 4 To be validated
-< 4 Total
----
-> 3 To be validated
-> 3 Total
-182,183d176
-< [eva] tests/value/reevaluate_alarms.i:14:
-< assertion 'Eva,mem_access' got final status valid.
-274,275d266
-< [ Valid ] Assertion 'Eva,mem_access' (file tests/value/reevaluate_alarms.i, line 14)
-< by Eva (v2).
-294,295c285,286
-< 4 Completely validated
-< 4 Total
----
-> 3 Completely validated
-> 3 Total
-diff tests/value/oracle/semaphore.res.oracle tests/value/oracle_gauges/semaphore.res.oracle
-24a25,33
-> [eva] computing for function V <- g.
-> Called from tests/value/semaphore.i:31.
-> [eva] Done for function V
-> [eva] computing for function V <- g.
-> Called from tests/value/semaphore.i:31.
-> [eva] Done for function V
-> [eva] computing for function V <- g.
-> Called from tests/value/semaphore.i:31.
-> [eva] Done for function V
-diff tests/value/oracle/symbolic_locs.res.oracle tests/value/oracle_gauges/symbolic_locs.res.oracle
-135a136
-> [eva] tests/value/symbolic_locs.i:93: starting to merge loop iterations
-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
-101a103
-> [eva] tests/value/undefined_sequence.i:49: starting to merge loop iterations
-Only in tests/value/oracle: unit_tests.res.oracle
-diff tests/value/oracle/unroll.res.oracle tests/value/oracle_gauges/unroll.res.oracle
-13,14d12
-< [eva:alarm] tests/value/unroll.i:34: Warning:
-< signed overflow. assert -2147483648 ≤ j - 1;
-16a15
-> [eva] tests/value/unroll.i:39: starting to merge loop iterations
-26c25
-< j ∈ [-2147483648..-123]
----
-> j ∈ {-238}
-diff tests/value/oracle/unroll_simple.res.oracle tests/value/oracle_gauges/unroll_simple.res.oracle
-8,9d7
-< [eva:alarm] tests/value/unroll_simple.i:11: Warning:
-< signed overflow. assert -2147483648 ≤ j - 1;
-11a10
-> [eva] tests/value/unroll_simple.i:16: starting to merge loop iterations
-21c20
-< j ∈ [-2147483648..-126]
----
-> j ∈ {-250}
-diff tests/value/oracle/va_list2.0.res.oracle tests/value/oracle_gauges/va_list2.0.res.oracle
-50a51,62
-> [eva] tests/value/va_list2.c:16:
-> Frama_C_show_each_i:
-> {{ garbled mix of &{S_0_S___va_params; S_1_S___va_params} (origin: Well) }}
-> [eva] tests/value/va_list2.c:21:
-> Frama_C_show_each_f:
-> {{ garbled mix of &{S_0_S___va_params; S_1_S___va_params} (origin: Well) }}
-> [eva] tests/value/va_list2.c:16:
-> Frama_C_show_each_i:
-> {{ garbled mix of &{S_0_S___va_params; S_1_S___va_params} (origin: Well) }}
-> [eva] tests/value/va_list2.c:21:
-> Frama_C_show_each_f:
-> {{ garbled mix of &{S_0_S___va_params; S_1_S___va_params} (origin: Well) }}
-diff tests/value/oracle/va_list2.1.res.oracle tests/value/oracle_gauges/va_list2.1.res.oracle
-40a41,52
-> [eva] computing for function __builtin_va_arg <- main.
-> Called from tests/value/va_list2.c:15.
-> [eva] Done for function __builtin_va_arg
-> [eva] computing for function __builtin_va_arg <- main.
-> Called from tests/value/va_list2.c:20.
-> [eva] Done for function __builtin_va_arg
-> [eva] computing for function __builtin_va_arg <- main.
-> Called from tests/value/va_list2.c:15.
-> [eva] Done for function __builtin_va_arg
-> [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_on_non_monotonic.res.oracle tests/value/oracle_gauges/widen_on_non_monotonic.res.oracle
-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 tests/value/oracle/widen_overflow.res.oracle tests/value/oracle_gauges/widen_overflow.res.oracle
-31a32,34
-> [eva] computing for function u <- main.
-> Called from tests/value/widen_overflow.i:9.
-> [eva] Done for function u
diff --git a/tests/value/diff_octagons b/tests/value/diff_octagons
deleted file mode 100644
index 60823ae538c..00000000000
--- a/tests/value/diff_octagons
+++ /dev/null
@@ -1,413 +0,0 @@
-diff tests/value/oracle/alias.1.res.oracle tests/value/oracle_octagons/alias.1.res.oracle
-85c85
-< z ∈ {0; 1; 2}
----
-> z ∈ {0; 2}
-diff tests/value/oracle/alias.2.res.oracle tests/value/oracle_octagons/alias.2.res.oracle
-76c76
-< z ∈ {-5; -4; -3; -2; -1; 0; 1; 1000}
----
-> z ∈ {-2; -1; 0; 1000}
-diff tests/value/oracle/alias.3.res.oracle tests/value/oracle_octagons/alias.3.res.oracle
-67c67
-< z ∈ {0; 1; 2}
----
-> z ∈ {0; 2}
-diff tests/value/oracle/alias.5.res.oracle tests/value/oracle_octagons/alias.5.res.oracle
-59a60
-> [eva] tests/value/alias.i:260: starting to merge loop iterations
-diff tests/value/oracle/alias.6.res.oracle tests/value/oracle_octagons/alias.6.res.oracle
-82c82
-< t ∈ {4; 5; 6}
----
-> t ∈ {5}
-87c87
-< y ∈ {0; 1}
----
-> y ∈ {1}
-94,96c94,96
-< tz1 ∈ {0; 1}
-< tz2 ∈ {0; 1}
-< tz3 ∈ {0; 1}
----
-> tz1 ∈ {1}
-> tz2 ∈ {1}
-> tz3 ∈ {1}
-diff tests/value/oracle/auto_loop_unroll.0.res.oracle tests/value/oracle_octagons/auto_loop_unroll.0.res.oracle
-211,212d210
-< [eva:alarm] tests/value/auto_loop_unroll.c:203: Warning:
-< signed overflow. assert -2147483648 ≤ i_0 - 1;
-218,219d215
-< [eva:alarm] tests/value/auto_loop_unroll.c:208: Warning:
-< signed overflow. assert -2147483648 ≤ i_1 - 1;
-245,246d240
-< [eva:alarm] tests/value/auto_loop_unroll.c:240: Warning:
-< signed overflow. assert -2147483648 ≤ i - 1;
-306c300
-< i ∈ [-2147483648..20]
----
-> i ∈ {-1}
-diff tests/value/oracle/bitfield.res.oracle tests/value/oracle_octagons/bitfield.res.oracle
-138a139,141
-> [eva] tests/value/bitfield.i:71:
-> Frama_C_show_each:
-> {{ garbled mix of &{b} (origin: Misaligned {tests/value/bitfield.i:70}) }}
-diff tests/value/oracle/builtins_split.res.oracle tests/value/oracle_octagons/builtins_split.res.oracle
-70a71,84
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:104:
-> Call to builtin Frama_C_builtin_split_all
-81a96,109
-> [eva] tests/value/builtins_split.c:112:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:112:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:112:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:112:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:112:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:112:
-> Call to builtin Frama_C_builtin_split_all
-> [eva] tests/value/builtins_split.c:112:
-> Call to builtin Frama_C_builtin_split_all
-diff tests/value/oracle/call_simple.res.oracle tests/value/oracle_octagons/call_simple.res.oracle
-28c28
-< c ∈ [--..--]
----
-> c ∈ [-2147483648..2147483646]
-diff tests/value/oracle/descending.res.oracle tests/value/oracle_octagons/descending.res.oracle
-42c42
-< i ∈ {31; 32}
----
-> i ∈ {31}
-diff tests/value/oracle/downcast.1.res.oracle tests/value/oracle_octagons/downcast.1.res.oracle
-61c61
-< [100000..2147483647], [100145..2147483647], [100145..2147483647]
----
-> [100000..2147483502], [100145..2147483647], [100145..2147483647]
-166c166
-< x_0 ∈ [100000..2147483647]
----
-> x_0 ∈ [100000..2147483502]
-diff tests/value/oracle/equality.res.oracle tests/value/oracle_octagons/equality.res.oracle
-29,30c29,30
-< y ∈ [0..42] or UNINITIALIZED
-< w ∈ [0..42] or UNINITIALIZED
----
-> y ∈ [0..42]
-> w ∈ [0..42]
-diff tests/value/oracle/find_ivaltop.res.oracle tests/value/oracle_octagons/find_ivaltop.res.oracle
-32,33c32,33
-< j ∈ {0; 1; 2; 3; 4; 5; 6; 7}
-< X ∈ {1; 2; 3; 4; 5; 6; 7; 8}
----
-> j ∈ {7}
-> X ∈ {8}
-39c39
-< \result FROM t[0..7]
----
-> \result FROM t[7]
-44c44
-< t[0..7]
----
-> t[7]
-diff tests/value/oracle/for_loops.3.res.oracle tests/value/oracle_octagons/for_loops.3.res.oracle
-20c20
-< v ∈ [0..2147483647]
----
-> v ∈ [5..2147483647]
-diff tests/value/oracle/gauges.res.oracle tests/value/oracle_octagons/gauges.res.oracle
-209,210d208
-< [eva:alarm] tests/value/gauges.c:156: Warning:
-< signed overflow. assert -2147483648 ≤ toCopy - 1;
-276,277d273
-< [eva:alarm] tests/value/gauges.c:201: Warning:
-< signed overflow. assert -2147483648 ≤ numNonZero - 1;
-300,304d295
-< [eva] tests/value/gauges.c:218: Frama_C_show_each:
-< [eva] tests/value/gauges.c:218: Frama_C_show_each:
-< [eva] tests/value/gauges.c:218: Frama_C_show_each:
-< [eva:alarm] tests/value/gauges.c:220: Warning:
-< signed overflow. assert -2147483648 ≤ n - 1;
-791c782
-< numNonZero ∈ [-2147483648..8]
----
-> numNonZero ∈ {-1}
-802c793
-< n ∈ [-2147483648..99]
----
-> n ∈ {-1}
-863c854
-< toCopy ∈ [-2147483648..99]
----
-> toCopy ∈ {-1}
-diff tests/value/oracle/loop.res.oracle tests/value/oracle_octagons/loop.res.oracle
-26c26
-< r ∈ [0..2147483646],0%2
----
-> r ∈ [46..2147483646],0%2
-diff tests/value/oracle/loop_wvar.1.res.oracle tests/value/oracle_octagons/loop_wvar.1.res.oracle
-12,13d11
-< [eva:alarm] tests/value/loop_wvar.i:57: Warning:
-< signed overflow. assert next + 1 ≤ 2147483647;
-41c39
-< next ∈ [0..2147483647]
----
-> next ∈ [0..25]
-diff tests/value/oracle/modulo.res.oracle tests/value/oracle_octagons/modulo.res.oracle
-40a41,56
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [-9..-1], [-8..0]
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [-10..-1], [1..9], [-8..0]
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [-9..-1], [0..8]
-> [eva] tests/value/modulo.i:41: Frama_C_show_each_1: [1..10], [1..9], [0..8]
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> [-9..-1], {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
-> [eva] tests/value/modulo.i:41:
-> Frama_C_show_each_1:
-> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
-50a67,82
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [1..9], [-8..0]
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [-10..-1], [-9..-1], [-8..0]
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [1..9], [0..8]
-> [eva] tests/value/modulo.i:53: Frama_C_show_each_2: [1..10], [-9..-1], [0..8]
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> [-9..-1], {1; 2; 3; 4; 5; 6; 7; 8}, {-7; -6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> [1..9], {1; 2; 3; 4; 5; 6; 7; 8}, {0; 1; 2; 3; 4; 5; 6; 7}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> [-9..-1], {-8; -7; -6; -5; -4; -3; -2; -1}, {-7; -6; -5; -4; -3; -2; -1; 0}
-> [eva] tests/value/modulo.i:53:
-> Frama_C_show_each_2:
-> [1..9], {-8; -7; -6; -5; -4; -3; -2; -1}, {0; 1; 2; 3; 4; 5; 6; 7}
-60a93,94
-> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-10..10], [-9..9], [-8..8]
-> [eva] tests/value/modulo.i:64: Frama_C_show_each_3: [-9..9], [-8..8], [-7..7]
-diff tests/value/oracle/non_natural.res.oracle tests/value/oracle_octagons/non_natural.res.oracle
-58a59,60
-> [kernel] tests/value/non_natural.i:30:
-> more than 200(12500) elements to enumerate. Approximating.
-65a68,69
-> [kernel] tests/value/non_natural.i:23:
-> more than 200(12500) elements to enumerate. Approximating.
-70a75,76
-> [kernel] tests/value/non_natural.i:24:
-> more than 200(12500) elements to enumerate. Approximating.
-78a85,86
-> [kernel] tests/value/non_natural.i:25:
-> more than 200(12500) elements to enumerate. Approximating.
-86a95,96
-> [kernel] tests/value/non_natural.i:26:
-> more than 200(12500) elements to enumerate. Approximating.
-94a105,106
-> [kernel] tests/value/non_natural.i:27:
-> more than 200(12500) elements to enumerate. Approximating.
-102a115,116
-> [kernel] tests/value/non_natural.i:28:
-> more than 200(12500) elements to enumerate. Approximating.
-110a125,126
-> [kernel] tests/value/non_natural.i:29:
-> more than 200(12500) elements to enumerate. Approximating.
-129,130d144
-< [kernel] tests/value/non_natural.i:23:
-< more than 200(12500) elements to enumerate. Approximating.
-133,146d146
-< [kernel] tests/value/non_natural.i:24:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:25:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:26:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:27:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:28:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:29:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:30:
-< more than 200(12500) elements to enumerate. Approximating.
-199a200,201
-> [kernel] tests/value/non_natural.i:39:
-> more than 200(12500) elements to enumerate. Approximating.
-diff tests/value/oracle/nonlin.res.oracle tests/value/oracle_octagons/nonlin.res.oracle
-113a114,115
-> [eva:nonlin] tests/value/nonlin.c:71: non-linear 'x * x', lv 'x'
-> [eva:nonlin] tests/value/nonlin.c:71: subdividing on x
-116a119,121
-> [eva:nonlin] tests/value/nonlin.c:72: subdividing on x
-> [eva:nonlin] tests/value/nonlin.c:72: non-linear 'y * y', lv 'y'
-> [eva:nonlin] tests/value/nonlin.c:72: subdividing on y
-119a125,126
-> [eva:nonlin] tests/value/nonlin.c:74: non-linear 'z * x + x * y', lv 'x'
-> [eva:nonlin] tests/value/nonlin.c:74: subdividing on x
-157a165,166
-> [eva:nonlin] tests/value/nonlin.c:118: non-linear 'x * x', lv 'x'
-> [eva:nonlin] tests/value/nonlin.c:118: subdividing on x
-160a170
-> [eva:nonlin] tests/value/nonlin.c:119: subdividing on x
-161a172
-> [eva:nonlin] tests/value/nonlin.c:121: subdividing on x
-diff tests/value/oracle/plevel.res.oracle tests/value/oracle_octagons/plevel.res.oracle
-12d11
-< [eva] Recording results for main
-14a14
-> [eva] Recording results for main
-diff tests/value/oracle/ptr_relation.1.res.oracle tests/value/oracle_octagons/ptr_relation.1.res.oracle
-24c24
-< j ∈ {-1; 0; 1}
----
-> j ∈ {0}
-diff tests/value/oracle/relation_reduction.res.oracle tests/value/oracle_octagons/relation_reduction.res.oracle
-24,27d23
-< [eva:alarm] tests/value/relation_reduction.i:20: Warning:
-< accessing out of bounds index. assert 0 ≤ y;
-< [eva:alarm] tests/value/relation_reduction.i:20: Warning:
-< accessing out of bounds index. assert y < 9;
-34,37c30,33
-< R1 ∈ [-2147483648..2147483637]
-< R2 ∈ [-2147483638..2147483647]
-< R3 ∈ [--..--]
-< R4 ∈ {0; 1; 2; 3; 4; 5}
----
-> R1 ∈ {0; 2}
-> R2 ∈ {0; 12}
-> R3 ∈ {0; 7}
-> R4 ∈ {0; 2}
-48c44
-< R4 FROM tab[0..8]; x (and SELF)
----
-> R4 FROM tab[0..5]; x (and SELF)
-53c49
-< y; t; tab[0..8]
----
-> y; t; tab[0..5]
-diff tests/value/oracle/relation_shift.res.oracle tests/value/oracle_octagons/relation_shift.res.oracle
-18,25d17
-< [eva:alarm] tests/value/relation_shift.i:15: Warning:
-< signed overflow. assert -2147483648 ≤ x - y;
-< [eva:alarm] tests/value/relation_shift.i:15: Warning:
-< signed overflow. assert x - y ≤ 2147483647;
-< [eva:alarm] tests/value/relation_shift.i:16: Warning:
-< signed overflow. assert -2147483648 ≤ z - y;
-< [eva:alarm] tests/value/relation_shift.i:16: Warning:
-< signed overflow. assert z - y ≤ 2147483647;
-31,32c23,24
-< r1 ∈ [--..--]
-< r2 ∈ [--..--]
----
-> r1 ∈ {2}
-> r2 ∈ {7}
-35,37c27,29
-< x ∈ [-2147483647..2147483647]
-< y ∈ [-2147483648..2147483646]
-< z ∈ [-2147483642..2147483647]
----
-> x ∈ [-2147483646..2147483642]
-> y ∈ [-2147483648..2147483640]
-> z ∈ [-2147483641..2147483647]
-49,50c41,42
-< r1 ∈ [--..--]
-< r2 ∈ [--..--]
----
-> r1 ∈ {2}
-> r2 ∈ {7}
-53,55c45,47
-< x ∈ [-2147483647..2147483647]
-< y ∈ [-2147483648..2147483646]
-< z ∈ [-2147483642..2147483647]
----
-> x ∈ [-2147483646..2147483642]
-> y ∈ [-2147483648..2147483640]
-> z ∈ [-2147483641..2147483647]
-diff tests/value/oracle/relations.res.oracle tests/value/oracle_octagons/relations.res.oracle
-80,81c80,82
-< e ∈ [--..--]
-< f ∈ [--..--]
----
-> e ∈ {1}
-> f[bits 0 to 7] ∈ {1; 4}
-> [bits 8 to 31] ∈ [--..--]
-diff tests/value/oracle/relations2.res.oracle tests/value/oracle_octagons/relations2.res.oracle
-25c25
-< len ∈ [--..--]
----
-> len ∈ [0..1023]
-36,37c36
-< [eva] tests/value/relations2.i:17:
-< Frama_C_show_each_end: [0..4294967295], [0..64]
----
-> [eva] tests/value/relations2.i:17: Frama_C_show_each_end: [0..1023], [0..64]
-59c58
-< n ∈ [0..512]
----
-> n ∈ [1..512]
-69,71d67
-< [eva:alarm] tests/value/relations2.i:34: Warning:
-< accessing out of bounds index.
-< assert (unsigned int)(i - (unsigned int)(t + 1)) < 514;
-80c76
-< n ∈ [0..512]
----
-> n ∈ [1..512]
-97c93
-< n ∈ [0..512]
----
-> n ∈ [1..512]
-140c136
-< len ∈ [--..--]
----
-> len ∈ [0..1023]
-diff tests/value/oracle/semaphore.res.oracle tests/value/oracle_octagons/semaphore.res.oracle
-65c65
-< c ∈ {-26; -1}
----
-> c ∈ {-1}
-diff tests/value/oracle/struct2.res.oracle tests/value/oracle_octagons/struct2.res.oracle
-81,84d80
-< accessing out of bounds index. assert 0 ≤ (int)(i + j);
-< [eva:alarm] tests/value/struct2.i:185: Warning:
-< accessing out of bounds index. assert (int)(i + j) < 2;
-< [eva:alarm] tests/value/struct2.i:185: Warning:
-106d101
-< [scope:rm_asserts] removing 2 assertion(s)
-diff tests/value/oracle/test.0.res.oracle tests/value/oracle_octagons/test.0.res.oracle
-17,18d16
-< [eva:alarm] tests/value/test.i:11: Warning:
-< signed overflow. assert j + ecart ≤ 2147483647;
-29c27
-< j ∈ [-1073741822..1]
----
-> j ∈ {-1; 0; 1}
-Only in tests/value/oracle: unit_tests.res.oracle
-diff tests/value/oracle/unroll.res.oracle tests/value/oracle_octagons/unroll.res.oracle
-22c22
-< G ∈ [17739..2147483647]
----
-> G ∈ [17854..2147483647]
-diff tests/value/oracle/unroll_simple.res.oracle tests/value/oracle_octagons/unroll_simple.res.oracle
-17c17
-< G ∈ [8772..2147483647]
----
-> G ∈ [8896..2147483647]
diff --git a/tests/value/diff_symblocs b/tests/value/diff_symblocs
deleted file mode 100644
index a03b0b46bdb..00000000000
--- a/tests/value/diff_symblocs
+++ /dev/null
@@ -1,329 +0,0 @@
-diff tests/value/oracle/alias.0.res.oracle tests/value/oracle_symblocs/alias.0.res.oracle
-103,104c103,104
-< t ∈ {1; 2; 4}
-< u ∈ {2; 3; 4; 5}
----
-> t ∈ {4}
-> u ∈ {5}
-110c110
-< t2 ∈ {0; 3; 6}
----
-> t2 ∈ {6}
-diff tests/value/oracle/alias.4.res.oracle tests/value/oracle_symblocs/alias.4.res.oracle
-81c81
-< y ∈ {0; 3; 77}
----
-> y ∈ {77}
-diff tests/value/oracle/alias.5.res.oracle tests/value/oracle_symblocs/alias.5.res.oracle
-170c170
-< y ∈ {0; 3; 77}
----
-> y ∈ {77}
-diff tests/value/oracle/alias.6.res.oracle tests/value/oracle_symblocs/alias.6.res.oracle
-86c86
-< x ∈ {0; 4; 33}
----
-> x ∈ {33}
-diff tests/value/oracle/bitwise_pointer.res.oracle tests/value/oracle_symblocs/bitwise_pointer.res.oracle
-62c62
-< x ∈ [0..9]
----
-> x ∈ {5}
-75c75
-< x1 ∈ [0..9]
----
-> x1 ∈ {5}
-diff tests/value/oracle/bitwise_reduction.res.oracle tests/value/oracle_symblocs/bitwise_reduction.res.oracle
-20c20
-< {0; 1}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
----
-> {0; 1}, {0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
-23c23
-< {0; 1}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
----
-> {0; 1}, {0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
-30c30
-< {{ &t + {0; 4} }}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
----
-> {{ &t + {0; 4} }}, {0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
-33c33
-< {0; 1}, {0; 1; 0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
----
-> {0; 1}, {0x3000; 0x3001; 0x3200; 0x3201; 0xF000; 0xFF00}
-diff tests/value/oracle/domains_function.res.oracle tests/value/oracle_symblocs/domains_function.res.oracle
-19,20c19
-< [eva] tests/value/domains_function.c:92:
-< Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] tests/value/domains_function.c:92: Frama_C_show_each_top: {3}
-28,29c27
-< [eva] tests/value/domains_function.c:77:
-< Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] tests/value/domains_function.c:77: Frama_C_show_each_top: {1}
-32,33c30
-< [eva] tests/value/domains_function.c:96:
-< Frama_C_show_each_top: [-2147483648..2147483647]
----
-> [eva] tests/value/domains_function.c:96: Frama_C_show_each_top: {1}
-52,56c49,50
-< [eva] computing for function not_enabled <- recursively_enabled <- main.
-< Called from tests/value/domains_function.c:110.
-< [eva] tests/value/domains_function.c:77: Frama_C_show_each_top: {1}
-< [eva] Recording results for not_enabled
-< [eva] Done for function not_enabled
----
-> [eva] tests/value/domains_function.c:110:
-> Reusing old results for call to not_enabled
-58,63c52,53
-< [eva] computing for function disabled <- recursively_enabled <- main.
-< Called from tests/value/domains_function.c:112.
-< [eva] tests/value/domains_function.c:84:
-< Frama_C_show_each_top: [-2147483648..2147483647]
-< [eva] Recording results for disabled
-< [eva] Done for function disabled
----
-> [eva] tests/value/domains_function.c:112:
-> Reusing old results for call to disabled
-130c120
-< result ∈ [--..--]
----
-> result ∈ {1}
-diff tests/value/oracle/incompatible_states.res.oracle tests/value/oracle_symblocs/incompatible_states.res.oracle
-41,42d40
-< [eva:alarm] tests/value/incompatible_states.c:53: Warning:
-< division by zero. assert t[i] ≢ 0;
-49c47
-< [scope:rm_asserts] removing 2 assertion(s)
----
-> [scope:rm_asserts] removing 1 assertion(s)
-diff tests/value/oracle/library.res.oracle tests/value/oracle_symblocs/library.res.oracle
-129,132d128
-< [eva:alarm] tests/value/library.i:44: Warning:
-< non-finite float value. assert \is_finite(*pf);
-< [eva:alarm] tests/value/library.i:44: Warning:
-< non-finite float value. assert \is_finite(\add_float(*pf, *pf));
-diff tests/value/oracle/non_natural.res.oracle tests/value/oracle_symblocs/non_natural.res.oracle
-58a59,60
-> [kernel] tests/value/non_natural.i:30:
-> more than 200(12500) elements to enumerate. Approximating.
-65a68,71
-> [kernel] tests/value/non_natural.i:23:
-> more than 200(12501) elements to enumerate. Approximating.
-> [kernel] tests/value/non_natural.i:23:
-> more than 200(12500) elements to enumerate. Approximating.
-70a77,80
-> [kernel] tests/value/non_natural.i:24:
-> more than 200(12501) elements to enumerate. Approximating.
-> [kernel] tests/value/non_natural.i:24:
-> more than 200(12500) elements to enumerate. Approximating.
-78a89,90
-> [kernel] tests/value/non_natural.i:25:
-> more than 200(12500) elements to enumerate. Approximating.
-86a99,100
-> [kernel] tests/value/non_natural.i:26:
-> more than 200(12500) elements to enumerate. Approximating.
-94a109,110
-> [kernel] tests/value/non_natural.i:27:
-> more than 200(12500) elements to enumerate. Approximating.
-102a119,120
-> [kernel] tests/value/non_natural.i:28:
-> more than 200(12500) elements to enumerate. Approximating.
-110a129,130
-> [kernel] tests/value/non_natural.i:29:
-> more than 200(12500) elements to enumerate. Approximating.
-127,146d146
-< [kernel] tests/value/non_natural.i:23:
-< more than 200(12501) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:23:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:24:
-< more than 200(12501) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:24:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:25:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:26:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:27:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:28:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:29:
-< more than 200(12500) elements to enumerate. Approximating.
-< [kernel] tests/value/non_natural.i:30:
-< more than 200(12500) elements to enumerate. Approximating.
-199a200,201
-> [kernel] tests/value/non_natural.i:39:
-> more than 200(12500) elements to enumerate. Approximating.
-diff tests/value/oracle/offsetmap.0.res.oracle tests/value/oracle_symblocs/offsetmap.0.res.oracle
-40d39
-< [eva] Recording results for g
-42a42
-> [eva] Recording results for g
-diff tests/value/oracle/offsetmap.1.res.oracle tests/value/oracle_symblocs/offsetmap.1.res.oracle
-40d39
-< [eva] Recording results for g
-42a42
-> [eva] Recording results for g
-diff tests/value/oracle/plevel.res.oracle tests/value/oracle_symblocs/plevel.res.oracle
-12d11
-< [eva] Recording results for main
-14a14
-> [eva] Recording results for main
-diff tests/value/oracle/ptr_relation.0.res.oracle tests/value/oracle_symblocs/ptr_relation.0.res.oracle
-23c23
-< i ∈ {0; 77; 333}
----
-> i ∈ {77}
-diff tests/value/oracle/redundant_alarms.res.oracle tests/value/oracle_symblocs/redundant_alarms.res.oracle
-10,13d9
-< [eva:alarm] tests/value/redundant_alarms.c:11: Warning:
-< accessing uninitialized left-value. assert \initialized(p);
-< [eva:alarm] tests/value/redundant_alarms.c:12: Warning:
-< accessing uninitialized left-value. assert \initialized(p);
-24,27d19
-< [eva:alarm] tests/value/redundant_alarms.c:21: Warning:
-< accessing uninitialized left-value. assert \initialized(&t[i]);
-< [eva:alarm] tests/value/redundant_alarms.c:22: Warning:
-< accessing uninitialized left-value. assert \initialized(&t[i]);
-38,41d29
-< [eva:alarm] tests/value/redundant_alarms.c:32: Warning:
-< accessing uninitialized left-value. assert \initialized(&t[j]);
-< [eva:alarm] tests/value/redundant_alarms.c:33: Warning:
-< accessing uninitialized left-value. assert \initialized(&t[i]);
-63,69d50
-< [scope:rm_asserts] removing 3 assertion(s)
-< [scope:rm_asserts] tests/value/redundant_alarms.c:12:
-< removing redundant assert Eva: initialization: \initialized(p);
-< [scope:rm_asserts] tests/value/redundant_alarms.c:32:
-< removing redundant assert Eva: initialization: \initialized(&t[j]);
-< [scope:rm_asserts] tests/value/redundant_alarms.c:33:
-< removing redundant assert Eva: initialization: \initialized(&t[i]);
-108d88
-< /*@ assert Eva: initialization: \initialized(p); */
-110d89
-< /*@ assert Eva: initialization: \initialized(p); */
-127d105
-< /*@ assert Eva: initialization: \initialized(&t[i]); */
-129d106
-< /*@ assert Eva: initialization: \initialized(&t[i]); */
-142d118
-< /*@ assert Eva: initialization: \initialized(&t[j]); */
-144d119
-< /*@ assert Eva: initialization: \initialized(&t[i]); */
-196a172
-> int z;
-199,201d174
-< *p = 1;
-< int z = *p + 1;
-< int w = *p + 2;
-diff tests/value/oracle/relations2.res.oracle tests/value/oracle_symblocs/relations2.res.oracle
-133d132
-< [eva] tests/value/relations2.i:57: Frama_C_show_each_NO2:
-diff tests/value/oracle/struct2.res.oracle tests/value/oracle_symblocs/struct2.res.oracle
-55a56,57
-> [kernel] tests/value/struct2.i:78: Warning:
-> all target addresses were invalid. This path is assumed to be dead.
-59,60d60
-< accessing out of bounds index. assert 0 ≤ (int)(tab2[i] + j);
-< [eva:alarm] tests/value/struct2.i:82: Warning:
-83,84d82
-< accessing out of bounds index. assert (int)(i + j) < 2;
-< [eva:alarm] tests/value/struct2.i:185: Warning:
-106c104
-< [scope:rm_asserts] removing 2 assertion(s)
----
-> [scope:rm_asserts] removing 1 assertion(s)
-144,145c142
-< tab4[0] ∈ {0; 2}
-< [1] ∈ {0}
----
-> tab4[0..1] ∈ {0}
-148c145,146
-< tab6[0..1] ∈ {0; 2}
----
-> tab6[0] ∈ {0}
-> [1] ∈ {2}
-219c217
-< [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0..1];
----
-> [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0];
-diff tests/value/oracle/symbolic_locs.res.oracle tests/value/oracle_symblocs/symbolic_locs.res.oracle
-20a21,26
-> # Symbolic locations domain:
-> V: {[ t[i] -> {4} ]}
-> Z: {[ t[i] -> t[0..8]; i ]}
-> I: {[ t -> {t[i]}
-> i -> {t[i]} ]}
-> S: {[ i -> {t[i]} ]}
-31a38,42
-> # Symbolic locations domain:
-> V: {[ ]}
-> Z: {[ ]}
-> I: {[ ]}
-> S: {[ ]}
-48a60,65
-> # Symbolic locations domain:
-> V: {[ t[i] -> {4} ]}
-> Z: {[ t[i] -> t[0..8]; i ]}
-> I: {[ t -> {t[i]}
-> i -> {t[i]} ]}
-> S: {[ i -> {t[i]} ]}
-59a77,81
-> # Symbolic locations domain:
-> V: {[ ]}
-> Z: {[ ]}
-> I: {[ ]}
-> S: {[ ]}
-79a102,108
-> # Symbolic locations domain:
-> V: {[ t[i] -> {{ &x }} ]}
-> Z: {[ t[i] -> t[0..8]; i ]}
-> I: {[ t -> {t[i]}
-> i -> {t[i]} ]}
-> S: {[ i -> {t[i]}
-> x -> {t[i]} ]}
-92a122,126
-> # Symbolic locations domain:
-> V: {[ ]}
-> Z: {[ ]}
-> I: {[ ]}
-> S: {[ ]}
-108a143,148
-> # Symbolic locations domain:
-> V: {[ t[i] -> {1} ]}
-> Z: {[ t[i] -> t[0..8]; i ]}
-> I: {[ t -> {t[i]}
-> i -> {t[i]} ]}
-> S: {[ i -> {t[i]} ]}
-117a158,162
-> # Symbolic locations domain:
-> V: {[ ]}
-> Z: {[ ]}
-> I: {[ ]}
-> S: {[ ]}
-134a180,184
-> # Symbolic locations domain:
-> V: {[ ]}
-> Z: {[ ]}
-> I: {[ ]}
-> S: {[ ]}
-141,143c191
-< [eva:alarm] tests/value/symbolic_locs.i:111: Warning:
-< signed overflow. assert *p + 1 ≤ 2147483647;
-< [eva] tests/value/symbolic_locs.i:113: Frama_C_show_each: [0..2147483647]
----
-> [eva] tests/value/symbolic_locs.i:113: Frama_C_show_each: [10001..2147483647]
-152a201,205
-> # Symbolic locations domain:
-> V: {[ ]}
-> Z: {[ ]}
-> I: {[ ]}
-> S: {[ ]}
-diff tests/value/oracle/test.0.res.oracle tests/value/oracle_symblocs/test.0.res.oracle
-31c31
-< tmp ∈ [--..--] or UNINITIALIZED
----
-> tmp ∈ [-2147483647..2147483647] or UNINITIALIZED
-Only in tests/value/oracle: unit_tests.res.oracle
--
GitLab