From dddf3870639f9fe08b13c45146ff66ba69918e70 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 3 Apr 2019 09:56:47 +0200
Subject: [PATCH] [Eva] Updates test oracles for alternative domains.
---
tests/builtins/diff_apron | 4 +-
tests/builtins/diff_bitwise | 4 +-
tests/builtins/diff_equalities | 28 +++++------
tests/builtins/diff_gauges | 48 +++++++++++++++---
tests/builtins/diff_symblocs | 20 ++++----
tests/idct/diff_apron | 12 ++---
tests/idct/diff_equalities | 90 +++++++++++++++++-----------------
tests/idct/diff_gauges | 4 +-
tests/value/diff_apron | 6 +--
tests/value/diff_gauges | 51 ++++++++++++-------
10 files changed, 159 insertions(+), 108 deletions(-)
diff --git a/tests/builtins/diff_apron b/tests/builtins/diff_apron
index 7bad8145315..6e0afb298cf 100644
--- a/tests/builtins/diff_apron
+++ b/tests/builtins/diff_apron
@@ -1,9 +1,9 @@
diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_apron/Longinit_sequencer.res.oracle
-320c320
+323c323
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_apron/Longinit_sequencer.sav
-556c556
+562c562
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_apron/Longinit_sequencer.sav
diff --git a/tests/builtins/diff_bitwise b/tests/builtins/diff_bitwise
index 4994cdff7e3..a446ce5ec81 100644
--- a/tests/builtins/diff_bitwise
+++ b/tests/builtins/diff_bitwise
@@ -1,9 +1,9 @@
diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_bitwise/Longinit_sequencer.res.oracle
-320c320
+323c323
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_bitwise/Longinit_sequencer.sav
-556c556
+562c562
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_bitwise/Longinit_sequencer.sav
diff --git a/tests/builtins/diff_equalities b/tests/builtins/diff_equalities
index dc9d2d37177..534763b2be1 100644
--- a/tests/builtins/diff_equalities
+++ b/tests/builtins/diff_equalities
@@ -1,17 +1,17 @@
diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_equalities/Longinit_sequencer.res.oracle
-320c320
+323c323
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_equalities/Longinit_sequencer.sav
-556c556
+562c562
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_equalities/Longinit_sequencer.sav
diff tests/builtins/oracle/alloc_weak.res.oracle tests/builtins/oracle_equalities/alloc_weak.res.oracle
-34,35d33
+36,37d35
< [eva:alarm] tests/builtins/alloc_weak.c:30: Warning:
< accessing uninitialized left-value. assert \initialized(p);
-898c896
+900c898
< r ∈ [--..--]
---
> r ∈ {42}
@@ -301,31 +301,31 @@ diff tests/builtins/oracle/allocated.1.res.oracle tests/builtins/oracle_equaliti
> __malloc_main_l97[0]; __malloc_main_l114[0..3]; __malloc_main_l127;
> __malloc_main_l127_0[0..1]; __malloc_main_l127_1[0..2];
diff tests/builtins/oracle/imprecise.res.oracle tests/builtins/oracle_equalities/imprecise.res.oracle
-96a97,98
+100a101,102
> [kernel] tests/builtins/imprecise.c:51:
> imprecise size for variable v3 (abstract type 'struct u')
-216a219,220
+224a227,228
> [kernel] tests/builtins/imprecise.c:111:
> more than 200(300) elements to enumerate. Approximating.
-225a230,231
+233a238,239
> [kernel] tests/builtins/imprecise.c:114:
> more than 200(300) elements to enumerate. Approximating.
-229,232d234
+237,240d242
< [kernel] tests/builtins/imprecise.c:111:
< more than 200(300) elements to enumerate. Approximating.
< [kernel] tests/builtins/imprecise.c:114:
< more than 200(300) elements to enumerate. Approximating.
diff tests/builtins/oracle/linked_list.1.res.oracle tests/builtins/oracle_equalities/linked_list.1.res.oracle
-422a423,424
+455a456,457
> [kernel] tests/builtins/linked_list.c:19:
> more than 100(128) elements to enumerate. Approximating.
-470a473,474
+506a509,510
> [kernel] tests/builtins/linked_list.c:43:
> more than 100(128) elements to enumerate. Approximating.
-472a477,478
+508a513,514
> [kernel] tests/builtins/linked_list.c:44:
> more than 100(128) elements to enumerate. Approximating.
-558,561d563
+600,603d605
< [kernel] tests/builtins/linked_list.c:43:
< more than 100(128) elements to enumerate. Approximating.
< [kernel] tests/builtins/linked_list.c:44:
@@ -585,11 +585,11 @@ diff tests/builtins/oracle/malloc-optimistic.res.oracle tests/builtins/oracle_eq
---
> [eva] tests/builtins/malloc-optimistic.c:122: Frama_C_show_each: [30..99]
diff tests/builtins/oracle/write-const.res.oracle tests/builtins/oracle_equalities/write-const.res.oracle
-78c78
+84c84
< tmp ∈ {{ &a ; &b }}
---
> tmp ∈ {{ &b }}
-99c99
+107c107
< tmp ∈ {{ &a ; &b }}
---
> tmp ∈ {{ &b }}
diff --git a/tests/builtins/diff_gauges b/tests/builtins/diff_gauges
index b3a160758ab..f8f6c848e6d 100644
--- a/tests/builtins/diff_gauges
+++ b/tests/builtins/diff_gauges
@@ -1,14 +1,14 @@
diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_gauges/Longinit_sequencer.res.oracle
-320c320
+323c323
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_gauges/Longinit_sequencer.sav
-556c556
+562c562
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_gauges/Longinit_sequencer.sav
diff tests/builtins/oracle/linked_list.0.res.oracle tests/builtins/oracle_gauges/linked_list.0.res.oracle
-1052a1053,1058
+1094a1095,1100
> [eva] computing for function printf_va_1 <- main.
> Called from tests/builtins/linked_list.c:51.
> [eva] Done for function printf_va_1
@@ -16,7 +16,7 @@ diff tests/builtins/oracle/linked_list.0.res.oracle tests/builtins/oracle_gauges
> Called from tests/builtins/linked_list.c:51.
> [eva] Done for function printf_va_1
diff tests/builtins/oracle/linked_list.1.res.oracle tests/builtins/oracle_gauges/linked_list.1.res.oracle
-556a557,562
+598a599,604
> [eva] computing for function printf_va_1 <- main.
> Called from tests/builtins/linked_list.c:51.
> [eva] Done for function printf_va_1
@@ -39,10 +39,10 @@ diff tests/builtins/oracle/memcpy.res.oracle tests/builtins/oracle_gauges/memcpy
167a168,169
> [eva] tests/builtins/memcpy.c:96: Call to builtin memcpy
> [eva] tests/builtins/memcpy.c:96: Call to builtin memcpy
-446a449
+448a451
> [eva] tests/builtins/memcpy.c:230: starting to merge loop iterations
diff tests/builtins/oracle/realloc.res.oracle tests/builtins/oracle_gauges/realloc.res.oracle
-644a645,957
+689a690,1038
> [eva] tests/builtins/realloc.c:152: Call to builtin realloc
> [eva:malloc] bases_to_realloc: {__realloc_w_main10_l152}
> [eva:malloc] tests/builtins/realloc.c:152:
@@ -54,6 +54,9 @@ diff tests/builtins/oracle/realloc.res.oracle tests/builtins/oracle_gauges/reall
> __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] }}
@@ -80,6 +83,9 @@ diff tests/builtins/oracle/realloc.res.oracle tests/builtins/oracle_gauges/reall
> __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] }}
@@ -106,6 +112,9 @@ diff tests/builtins/oracle/realloc.res.oracle tests/builtins/oracle_gauges/reall
> __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] }}
@@ -132,6 +141,9 @@ diff tests/builtins/oracle/realloc.res.oracle tests/builtins/oracle_gauges/reall
> __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] }}
@@ -158,6 +170,9 @@ diff tests/builtins/oracle/realloc.res.oracle tests/builtins/oracle_gauges/reall
> __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] }}
@@ -184,6 +199,9 @@ diff tests/builtins/oracle/realloc.res.oracle tests/builtins/oracle_gauges/reall
> __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] }}
@@ -210,6 +228,9 @@ diff tests/builtins/oracle/realloc.res.oracle tests/builtins/oracle_gauges/reall
> __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] }}
@@ -236,6 +257,9 @@ diff tests/builtins/oracle/realloc.res.oracle tests/builtins/oracle_gauges/reall
> __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] }}
@@ -262,6 +286,9 @@ diff tests/builtins/oracle/realloc.res.oracle tests/builtins/oracle_gauges/reall
> __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] }}
@@ -289,6 +316,9 @@ diff tests/builtins/oracle/realloc.res.oracle tests/builtins/oracle_gauges/reall
> __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] }}
@@ -315,6 +345,9 @@ diff tests/builtins/oracle/realloc.res.oracle tests/builtins/oracle_gauges/reall
> __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] }}
@@ -341,6 +374,9 @@ diff tests/builtins/oracle/realloc.res.oracle tests/builtins/oracle_gauges/reall
> __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] }}
diff --git a/tests/builtins/diff_symblocs b/tests/builtins/diff_symblocs
index 72f7c197356..fc36c7d36a2 100644
--- a/tests/builtins/diff_symblocs
+++ b/tests/builtins/diff_symblocs
@@ -1,40 +1,40 @@
diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_symblocs/Longinit_sequencer.res.oracle
-320c320
+323c323
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_symblocs/Longinit_sequencer.sav
-556c556
+562c562
< tests/builtins/result/Longinit_sequencer.sav
---
> tests/builtins/result_symblocs/Longinit_sequencer.sav
diff tests/builtins/oracle/alloc_weak.res.oracle tests/builtins/oracle_symblocs/alloc_weak.res.oracle
-34,35d33
+36,37d35
< [eva:alarm] tests/builtins/alloc_weak.c:30: Warning:
< accessing uninitialized left-value. assert \initialized(p);
-898c896
+900c898
< r ∈ [--..--]
---
> r ∈ {42}
diff tests/builtins/oracle/imprecise.res.oracle tests/builtins/oracle_symblocs/imprecise.res.oracle
-216a217,218
+224a225,226
> [kernel] tests/builtins/imprecise.c:111:
> more than 200(300) elements to enumerate. Approximating.
-225a228,229
+233a236,237
> [kernel] tests/builtins/imprecise.c:114:
> more than 200(300) elements to enumerate. Approximating.
-229,232d232
+237,240d240
< [kernel] tests/builtins/imprecise.c:111:
< more than 200(300) elements to enumerate. Approximating.
< [kernel] tests/builtins/imprecise.c:114:
< more than 200(300) elements to enumerate. Approximating.
diff tests/builtins/oracle/linked_list.1.res.oracle tests/builtins/oracle_symblocs/linked_list.1.res.oracle
-470a471,472
+506a507,508
> [kernel] tests/builtins/linked_list.c:43:
> more than 100(128) elements to enumerate. Approximating.
-472a475,476
+508a511,512
> [kernel] tests/builtins/linked_list.c:44:
> more than 100(128) elements to enumerate. Approximating.
-558,561d561
+600,603d603
< [kernel] tests/builtins/linked_list.c:43:
< more than 100(128) elements to enumerate. Approximating.
< [kernel] tests/builtins/linked_list.c:44:
diff --git a/tests/idct/diff_apron b/tests/idct/diff_apron
index e3b1cc3498b..5ba6a7afd0f 100644
--- a/tests/idct/diff_apron
+++ b/tests/idct/diff_apron
@@ -37,7 +37,7 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
-412,430c424,461
+413,431c425,462
< [eva] tests/idct/ieee_1180_1990.c:85:
< Reusing old results for call to IEEE_1180_1990_rand
< [eva] tests/idct/ieee_1180_1990.c:85:
@@ -96,7 +96,7 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:260.
> [eva] Recording results for idct
> [eva] Done for function idct
-455,459c486,497
+456,460c487,498
< [eva] tests/idct/ieee_1180_1990.c:282:
< Reusing old results for call to IEEE_1180_1990_dctf
< [eva] tests/idct/ieee_1180_1990.c:283:
@@ -115,7 +115,7 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:284.
> [eva] Recording results for idct
> [eva] Done for function idct
-486,504c524,561
+487,505c525,562
< [eva] tests/idct/ieee_1180_1990.c:85:
< Reusing old results for call to IEEE_1180_1990_rand
< [eva] tests/idct/ieee_1180_1990.c:85:
@@ -174,7 +174,7 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:306.
> [eva] Recording results for idct
> [eva] Done for function idct
-529,533c586,597
+530,534c587,598
< [eva] tests/idct/ieee_1180_1990.c:328:
< Reusing old results for call to IEEE_1180_1990_dctf
< [eva] tests/idct/ieee_1180_1990.c:329:
@@ -193,7 +193,7 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:330.
> [eva] Recording results for idct
> [eva] Done for function idct
-557,570c621,1920
+558,571c622,1921
< [eva] tests/idct/ieee_1180_1990.c:85:
< Reusing old results for call to IEEE_1180_1990_rand
< [eva] tests/idct/ieee_1180_1990.c:85:
@@ -1509,7 +1509,7 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_apron/ieee_11
> Called from tests/idct/ieee_1180_1990.c:85.
> [eva] Recording results for IEEE_1180_1990_rand
> [eva] Done for function IEEE_1180_1990_rand
-625,870c1975,2102
+626,871c1976,2103
< [eva] tests/idct/ieee_1180_1990.c:214: Reusing old results for call to idct
< [eva] tests/idct/ieee_1180_1990.c:236:
< Reusing old results for call to IEEE_1180_1990_dctf
diff --git a/tests/idct/diff_equalities b/tests/idct/diff_equalities
index c05946b24e4..6d1b02bed20 100644
--- a/tests/idct/diff_equalities
+++ b/tests/idct/diff_equalities
@@ -1,23 +1,23 @@
diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_equalities/ieee_1180_1990.res.oracle
-355a356,357
-> [eva] tests/idct/ieee_1180_1990.c:219: Warning:
+356a357,358
+> [eva:signed-overflow] tests/idct/ieee_1180_1990.c:219: Warning:
> 2's complement assumed for overflow
-359a362,363
-> [eva] tests/idct/ieee_1180_1990.c:220: Warning:
+360a363,364
+> [eva:signed-overflow] tests/idct/ieee_1180_1990.c:220: Warning:
> 2's complement assumed for overflow
-365,366d368
-< [eva] tests/idct/ieee_1180_1990.c:219: Warning:
+366,367d369
+< [eva:signed-overflow] tests/idct/ieee_1180_1990.c:219: Warning:
< 2's complement assumed for overflow
-391a394,395
-> [eva] tests/idct/ieee_1180_1990.c:243: Warning:
+392a395,396
+> [eva:signed-overflow] tests/idct/ieee_1180_1990.c:243: Warning:
> 2's complement assumed for overflow
-395a400,401
-> [eva] tests/idct/ieee_1180_1990.c:244: Warning:
+396a401,402
+> [eva:signed-overflow] tests/idct/ieee_1180_1990.c:244: Warning:
> 2's complement assumed for overflow
-401,402d406
-< [eva] tests/idct/ieee_1180_1990.c:243: Warning:
+402,403d407
+< [eva:signed-overflow] tests/idct/ieee_1180_1990.c:243: Warning:
< 2's complement assumed for overflow
-423a428,435
+424a429,436
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
> [eva] tests/idct/ieee_1180_1990.c:85:
@@ -26,25 +26,25 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_equalities/ie
> Reusing old results for call to IEEE_1180_1990_rand
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
-436a449,450
-> [eva] tests/idct/ieee_1180_1990.c:265: Warning:
+437a450,451
+> [eva:signed-overflow] tests/idct/ieee_1180_1990.c:265: Warning:
> 2's complement assumed for overflow
-440a455,456
-> [eva] tests/idct/ieee_1180_1990.c:266: Warning:
+441a456,457
+> [eva:signed-overflow] tests/idct/ieee_1180_1990.c:266: Warning:
> 2's complement assumed for overflow
-446,447d461
-< [eva] tests/idct/ieee_1180_1990.c:265: Warning:
+447,448d462
+< [eva:signed-overflow] tests/idct/ieee_1180_1990.c:265: Warning:
< 2's complement assumed for overflow
-465a480,481
-> [eva] tests/idct/ieee_1180_1990.c:289: Warning:
+466a481,482
+> [eva:signed-overflow] tests/idct/ieee_1180_1990.c:289: Warning:
> 2's complement assumed for overflow
-469a486,487
-> [eva] tests/idct/ieee_1180_1990.c:290: Warning:
+470a487,488
+> [eva:signed-overflow] tests/idct/ieee_1180_1990.c:290: Warning:
> 2's complement assumed for overflow
-475,476d492
-< [eva] tests/idct/ieee_1180_1990.c:289: Warning:
+476,477d493
+< [eva:signed-overflow] tests/idct/ieee_1180_1990.c:289: Warning:
< 2's complement assumed for overflow
-497a514,521
+498a515,522
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
> [eva] tests/idct/ieee_1180_1990.c:85:
@@ -53,25 +53,25 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_equalities/ie
> Reusing old results for call to IEEE_1180_1990_rand
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
-510a535,536
-> [eva] tests/idct/ieee_1180_1990.c:311: Warning:
+511a536,537
+> [eva:signed-overflow] tests/idct/ieee_1180_1990.c:311: Warning:
> 2's complement assumed for overflow
-514a541,542
-> [eva] tests/idct/ieee_1180_1990.c:312: Warning:
+515a542,543
+> [eva:signed-overflow] tests/idct/ieee_1180_1990.c:312: Warning:
> 2's complement assumed for overflow
-520,521d547
-< [eva] tests/idct/ieee_1180_1990.c:311: Warning:
+521,522d548
+< [eva:signed-overflow] tests/idct/ieee_1180_1990.c:311: Warning:
< 2's complement assumed for overflow
-539a566,567
-> [eva] tests/idct/ieee_1180_1990.c:335: Warning:
+540a567,568
+> [eva:signed-overflow] tests/idct/ieee_1180_1990.c:335: Warning:
> 2's complement assumed for overflow
-543a572,573
-> [eva] tests/idct/ieee_1180_1990.c:336: Warning:
+544a573,574
+> [eva:signed-overflow] tests/idct/ieee_1180_1990.c:336: Warning:
> 2's complement assumed for overflow
-549,550d578
-< [eva] tests/idct/ieee_1180_1990.c:335: Warning:
+550,551d579
+< [eva:signed-overflow] tests/idct/ieee_1180_1990.c:335: Warning:
< 2's complement assumed for overflow
-570a599,606
+571a600,607
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
> [eva] tests/idct/ieee_1180_1990.c:85:
@@ -80,7 +80,7 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_equalities/ie
> Reusing old results for call to IEEE_1180_1990_rand
> [eva] tests/idct/ieee_1180_1990.c:85:
> Reusing old results for call to IEEE_1180_1990_rand
-578a615,632
+579a616,633
> [eva] tests/idct/ieee_1180_1990.c:100:
> Call to builtin Frama_C_sqrt for function sqrt
> [eva] tests/idct/ieee_1180_1990.c:101:
@@ -99,13 +99,13 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_equalities/ie
> Call to builtin Frama_C_cos for function cos
> [eva] tests/idct/ieee_1180_1990.c:100:
> Call to builtin Frama_C_sqrt for function sqrt
-580a635,636
+581a636,637
> [eva] tests/idct/ieee_1180_1990.c:100:
> Call to builtin Frama_C_sqrt for function sqrt
-582a639,640
+583a640,641
> [eva] tests/idct/ieee_1180_1990.c:100:
> Call to builtin Frama_C_sqrt for function sqrt
-604a663,676
+605a664,677
> [eva] tests/idct/ieee_1180_1990.c:140:
> Call to builtin Frama_C_sqrt for function sqrt
> [eva] tests/idct/ieee_1180_1990.c:141:
@@ -120,10 +120,10 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_equalities/ie
> Call to builtin Frama_C_cos for function cos
> [eva] tests/idct/ieee_1180_1990.c:140:
> Call to builtin Frama_C_sqrt for function sqrt
-606a679,680
+607a680,681
> [eva] tests/idct/ieee_1180_1990.c:140:
> Call to builtin Frama_C_sqrt for function sqrt
-608a683,688
+609a684,689
> [eva] tests/idct/ieee_1180_1990.c:140:
> Call to builtin Frama_C_sqrt for function sqrt
> [eva] tests/idct/ieee_1180_1990.c:141:
diff --git a/tests/idct/diff_gauges b/tests/idct/diff_gauges
index 2e026cd69ba..e7ae4765f4b 100644
--- a/tests/idct/diff_gauges
+++ b/tests/idct/diff_gauges
@@ -1,7 +1,7 @@
diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_gauges/ieee_1180_1990.res.oracle
-578a579,580
+579a580,581
> [eva] tests/idct/ieee_1180_1990.c:100:
> Call to builtin Frama_C_sqrt for function sqrt
-604a607,608
+605a608,609
> [eva] tests/idct/ieee_1180_1990.c:140:
> Call to builtin Frama_C_sqrt for function sqrt
diff --git a/tests/value/diff_apron b/tests/value/diff_apron
index 4db64f563c4..7b830e4e3d3 100644
--- a/tests/value/diff_apron
+++ b/tests/value/diff_apron
@@ -330,15 +330,15 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_apron/gauges.res.or
< Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..2147483647]
---
> Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..598]
-780c760
+798c778
< n ∈ [-2147483648..99]
---
> n ∈ [-2147483547..99]
-783c763
+801c781
< i ∈ [0..2147483647]
---
> i ∈ [10..2147483647]
-819c799
+837c817
< i ∈ [0..2147483647]
---
> i ∈ [0..21]
diff --git a/tests/value/diff_gauges b/tests/value/diff_gauges
index 4bd4e2a505c..99a2a77d76e 100644
--- a/tests/value/diff_gauges
+++ b/tests/value/diff_gauges
@@ -143,45 +143,48 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.o
< Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..2147483647]
---
> Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [99..119]
-415a370,373
+418a373,376
> # Gauges domain:
> V: [{[ p -> {{ &x }}
> i -> {1} ]}]
> s395: λ(0)
-472a431,434
+478a437,440
> # Gauges domain:
> V: [{[ i -> {1} ]}]
> s395: λ([0 .. 1])
> {[ i -> {1} ]}
-528a491,494
+537a500,503
> # Gauges domain:
> V: [{[ i -> {1} ]}]
> s395: λ([0 .. 2])
> {[ i -> {1} ]}
-584a551,554
+596a563,566
> # Gauges domain:
> V: [{[ i -> {1} ]}]
> s395: λ([0 .. 10])
> {[ i -> {1} ]}
-646a617,621
+661a632,636
> # Gauges domain:
> V: [{[ p -> {{ &a }}
> i -> {2} ]}]
> s409: λ(0)
> s408: λ(0)
-704a680,684
+722a698,702
> # Gauges domain:
> V: [{[ i -> {2} ]}]
> s409: λ(0)
> s408: λ([0 .. 1])
> {[ i -> {0} ]}
-706a687,808
+724a705,832
> [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] }}
@@ -243,6 +246,9 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.o
> __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] }}
@@ -298,53 +304,53 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.o
> s408: λ([0 .. +oo])
> {[ i -> {0} ]}
> ==END OF DUMP==
-714a817,818
+732a841,842
> [eva] tests/value/gauges.c:343: Call to builtin malloc
> [eva] tests/value/gauges.c:343: Call to builtin malloc
-767,768c871,872
+785,786c895,896
< A ∈ {{ &A + [0..--],0%4 }}
< B ∈ {{ &B + [0..--],0%4 }}
---
> A ∈ {{ &A + [0..36],0%4 }}
> B ∈ {{ &B + [0..36],0%4 }}
-786c890
+804c914
< i ∈ {45; 46; 47; 48; 49; 50; 51}
---
> i ∈ {45; 46; 47; 48}
-792c896
+810c920
< i ∈ {-59; -58; -57; -56; -55; -54; -53}
---
> i ∈ {-58; -57; -56; -55; -54; -53}
-812c916
+830c940
< p ∈ {{ &u + [0..--],0%4 }}
---
> p ∈ {{ &u + [0..400],0%4 }}
-814c918
+832c942
< k ∈ [0..2147483647]
---
> k ∈ [0..390]
-819c923
+837c947
< i ∈ [0..2147483647]
---
> i ∈ [0..21]
-830,831c934,936
+848,849c958,960
< [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] }}
-842c947
+860c971
< p ∈ {{ &T + [--..396],0%4 }}
---
> p ∈ {{ &T + [-4..396],0%4 }}
-977,978c1082,1083
+995,996c1106,1107
< 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]
-1056c1161
+1074c1185
< p; A[0..9]; B[0..9]
---
> p; A[0..8]; B[0..8]
@@ -460,6 +466,15 @@ diff tests/value/oracle/loop_wvar.1.res.oracle tests/value/oracle_gauges/loop_wv
---
> 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
99a100
> [eva] tests/value/memexec.c:98: starting to merge loop iterations
--
GitLab