diff --git a/tests/builtins/oracle/calloc.0.res.oracle b/tests/builtins/oracle/calloc.0.res.oracle
index 624317db33a6e4832109ecfe41dac48485c58ed8..810c06e4d77a5f803e9070f9357d5b5964b972c3 100644
--- a/tests/builtins/oracle/calloc.0.res.oracle
+++ b/tests/builtins/oracle/calloc.0.res.oracle
@@ -40,11 +40,11 @@
[eva:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
p1 ∈ [--..--]
- p2 ∈ [--..--]
- p3 ∈ [--..--]
- p4 ∈ [--..--]
- p5 ∈ [--..--]
- p9001 ∈ {0}
+ p2 ∈ [--..--] or UNINITIALIZED
+ p3 ∈ [--..--] or UNINITIALIZED
+ p4 ∈ [--..--] or UNINITIALIZED
+ p5 ∈ [--..--] or UNINITIALIZED
+ p9001 ∈ {0} or UNINITIALIZED
__retres ∈ {0; 1}
[from] Computing for function main
[from] Computing for function calloc <-main
diff --git a/tests/builtins/oracle/free.res.oracle b/tests/builtins/oracle/free.res.oracle
index 4f5cb6ae56f07cb9ca6b0984d705f3d7a0d5965f..080c1e9f72247363a280721aa3077c1789cd44c2 100644
--- a/tests/builtins/oracle/free.res.oracle
+++ b/tests/builtins/oracle/free.res.oracle
@@ -30,6 +30,9 @@
q ∈ {{ &__malloc_main1_l10[0] }}
r ∈ {{ &__malloc_main1_l8[0] ; &__malloc_main1_l10[0] }}
tmp_1 ∈ {{ &__malloc_main1_l8[0] ; &__malloc_main1_l10[0] }}
+ u ∈ UNINITIALIZED
+ t ∈ UNINITIALIZED
+ s ∈ UNINITIALIZED
S_0___fc_env[0..1] ∈ [--..--]
S_1___fc_env[0..1] ∈ [--..--]
__malloc_main1_l8[0] ∈ UNINITIALIZED
diff --git a/tests/builtins/oracle/realloc.res.oracle b/tests/builtins/oracle/realloc.res.oracle
index df107558a522d428e7c910802a4affbe07f80eb3..c2e751d30bbc889be7a576a4a1a0ea288c4c91a4 100644
--- a/tests/builtins/oracle/realloc.res.oracle
+++ b/tests/builtins/oracle/realloc.res.oracle
@@ -26,6 +26,7 @@
Frama_C_entropy_source ∈ [--..--]
p ∈ {{ &__malloc_main1_l12 }}
pp ∈ {{ &__malloc_main1_l12 }}
+ q ∈ UNINITIALIZED
v ∈ [--..--]
S_0___fc_env[0..1] ∈ [--..--]
S_1___fc_env[0..1] ∈ [--..--]
@@ -144,6 +145,7 @@
r ∈ {{ &__malloc_main3_l35[0] }}
p ∈ {{ &__malloc_main3_l32[0] ; &__malloc_main3_l35[0] }}
x ∈ {0; 1}
+ s ∈ UNINITIALIZED
v ∈ [--..--]
S_0___fc_env[0..1] ∈ [--..--]
S_1___fc_env[0..1] ∈ [--..--]
@@ -241,6 +243,8 @@
sizeq ∈ [0..10]
p ∈ {{ &__malloc_main4_l55[0] }}
q ∈ {{ &__malloc_main4_l56[0] }}
+ rp ∈ UNINITIALIZED
+ rq ∈ UNINITIALIZED
v ∈ [--..--]
S_0___fc_env[0..1] ∈ [--..--]
S_1___fc_env[0..1] ∈ [--..--]
@@ -356,6 +360,7 @@
p ∈ {{ &__malloc_main5_l76 }}
c ∈ {0; 1}
q ∈ {{ NULL ; &__malloc_main5_l76 }}
+ r ∈ UNINITIALIZED
v ∈ [--..--]
S_0___fc_env[0..1] ∈ [--..--]
S_1___fc_env[0..1] ∈ [--..--]
diff --git a/tests/builtins/oracle/realloc_multiple.0.res.oracle b/tests/builtins/oracle/realloc_multiple.0.res.oracle
index 5908db2b9e507a91de87ff057e31832be7b548e8..a45635beb983c3b71bc12573e69368c3668d105a 100644
--- a/tests/builtins/oracle/realloc_multiple.0.res.oracle
+++ b/tests/builtins/oracle/realloc_multiple.0.res.oracle
@@ -36,6 +36,7 @@
r ∈ {{ &__malloc_main1_l12[0] }}
p ∈ {{ &__malloc_main1_l9[0] ; &__malloc_main1_l12[0] }}
x ∈ {0; 1}
+ s ∈ UNINITIALIZED
v ∈ {1}
S_0___fc_env[0..1] ∈ [--..--]
S_1___fc_env[0..1] ∈ [--..--]
@@ -120,6 +121,7 @@
r ∈ {{ &__malloc_main2_l33[0] }}
p ∈ {{ NULL ; &__malloc_main2_l30[0] ; &__malloc_main2_l33[0] }}
x ∈ {0; 1; 2}
+ s ∈ UNINITIALIZED
v ∈ {2}
S_0___fc_env[0..1] ∈ [--..--]
S_1___fc_env[0..1] ∈ [--..--]
diff --git a/tests/builtins/oracle/realloc_multiple.1.res.oracle b/tests/builtins/oracle/realloc_multiple.1.res.oracle
index 052f0f273fa2a1f63c42e4ef5be7fa27b6c5d044..c9cedc5f77d6a92f51ed05c2e243b2e47c570e64 100644
--- a/tests/builtins/oracle/realloc_multiple.1.res.oracle
+++ b/tests/builtins/oracle/realloc_multiple.1.res.oracle
@@ -44,6 +44,7 @@
r ∈ {{ &__malloc_main1_l12[0] }}
p ∈ {{ &__malloc_main1_l9[0] ; &__malloc_main1_l12[0] }}
x ∈ {0; 1}
+ s ∈ UNINITIALIZED
v ∈ {1}
S_0___fc_env[0..1] ∈ [--..--]
S_1___fc_env[0..1] ∈ [--..--]
@@ -165,6 +166,7 @@
r ∈ {{ &__malloc_main2_l33[0] }}
p ∈ {{ NULL ; &__malloc_main2_l30[0] ; &__malloc_main2_l33[0] }}
x ∈ {0; 1; 2}
+ s ∈ UNINITIALIZED
v ∈ {2}
S_0___fc_env[0..1] ∈ [--..--]
S_1___fc_env[0..1] ∈ [--..--]
diff --git a/tests/float/oracle/alarms.0.res.oracle b/tests/float/oracle/alarms.0.res.oracle
index 8e964fd6c677d12e8068ca89de3c960044b80c11..2772f9227081cba003c033a6a70bb1f32b921e9c 100644
--- a/tests/float/oracle/alarms.0.res.oracle
+++ b/tests/float/oracle/alarms.0.res.oracle
@@ -29,7 +29,12 @@
ull ∈ {0}
rand ∈ [--..--]
l ∈ [--..--]
+ vf ∈ UNINITIALIZED
tmp ∈ UNINITIALIZED
+ vd ∈ UNINITIALIZED
+ i ∈ UNINITIALIZED
+ j ∈ UNINITIALIZED
+ mvd ∈ UNINITIALIZED
l ∈ [--..--]
==END OF DUMP==
[kernel:annot:missing-spec] alarms.i:21: Warning:
diff --git a/tests/float/oracle/alarms.1.res.oracle b/tests/float/oracle/alarms.1.res.oracle
index 95735134c42367149c53c4ba8502e4cc652e78e4..ebe72529a2011e39a98ad6da43b601abc1d697eb 100644
--- a/tests/float/oracle/alarms.1.res.oracle
+++ b/tests/float/oracle/alarms.1.res.oracle
@@ -26,7 +26,12 @@
ull ∈ {0}
rand ∈ [--..--]
l ∈ [--..--]
+ vf ∈ UNINITIALIZED
tmp ∈ UNINITIALIZED
+ vd ∈ UNINITIALIZED
+ i ∈ UNINITIALIZED
+ j ∈ UNINITIALIZED
+ mvd ∈ UNINITIALIZED
l ∈ [--..--]
==END OF DUMP==
[kernel:annot:missing-spec] alarms.i:21: Warning:
diff --git a/tests/float/oracle/alarms.2.res.oracle b/tests/float/oracle/alarms.2.res.oracle
index 6c47a9b44c57b387e173f5f380b9e47c2e794498..99a0bbe07d84ba84ee7a02a5673cff1fa6a6fec2 100644
--- a/tests/float/oracle/alarms.2.res.oracle
+++ b/tests/float/oracle/alarms.2.res.oracle
@@ -23,7 +23,12 @@
ull ∈ {0}
rand ∈ [--..--]
l ∈ [--..--]
+ vf ∈ UNINITIALIZED
tmp ∈ UNINITIALIZED
+ vd ∈ UNINITIALIZED
+ i ∈ UNINITIALIZED
+ j ∈ UNINITIALIZED
+ mvd ∈ UNINITIALIZED
l ∈ [--..--]
==END OF DUMP==
[kernel:annot:missing-spec] alarms.i:21: Warning:
diff --git a/tests/float/oracle/const3.0.res.oracle b/tests/float/oracle/const3.0.res.oracle
index 6f4eaebdd95a561893ca62ee3f8b956e4ad9a93f..7e8f509c45aca4a14fdec29d5924115bdea13517 100644
--- a/tests/float/oracle/const3.0.res.oracle
+++ b/tests/float/oracle/const3.0.res.oracle
@@ -14,6 +14,7 @@
# cvalue:
f1 ∈ {9.99994610111e-41}
d0 ∈ {1e-40}
+ d1 ∈ UNINITIALIZED
__retres ∈ UNINITIALIZED
==END OF DUMP==
[eva] Recording results for main
diff --git a/tests/float/oracle/const3.1.res.oracle b/tests/float/oracle/const3.1.res.oracle
index ade47d3bb883bc01da0dfebb79574f1cae5bd967..989c638425ec23473e424086ff5f18760e214deb 100644
--- a/tests/float/oracle/const3.1.res.oracle
+++ b/tests/float/oracle/const3.1.res.oracle
@@ -16,6 +16,7 @@
# cvalue:
f1 ∈ [0x1.16c2000000000p-133 .. 0x1.16c3000000000p-133]
d0 ∈ [0x1.16c262777579cp-133 .. 0x1.16c262777579dp-133]
+ d1 ∈ UNINITIALIZED
__retres ∈ UNINITIALIZED
==END OF DUMP==
[eva] Recording results for main
diff --git a/tests/float/oracle/const4.1.res.oracle b/tests/float/oracle/const4.1.res.oracle
index 8854b8b2448d6cd9fd7ec98ede98a3d0cbabde8b..90bb991ae7f4df63f44348f6ffc404915867806f 100644
--- a/tests/float/oracle/const4.1.res.oracle
+++ b/tests/float/oracle/const4.1.res.oracle
@@ -18,6 +18,7 @@
# cvalue:
f1 ∈ [3.39999995214e+38 .. 3.40000015497e+38]
f2 ∈ {3.40282346639e+38}
+ d2 ∈ UNINITIALIZED
__retres ∈ UNINITIALIZED
==END OF DUMP==
[eva] Recording results for main
diff --git a/tests/value/oracle/ilevel.1.res.oracle b/tests/value/oracle/ilevel.1.res.oracle
index af0704f7b5dc3605bcf5703ca05d7133098127fb..ed394c4de8468cfab8e6a4af5a3a2f280c3e1747 100644
--- a/tests/value/oracle/ilevel.1.res.oracle
+++ b/tests/value/oracle/ilevel.1.res.oracle
@@ -27,23 +27,23 @@
i_0 ∈ [0..10]
j_0 ∈ [-25..-15] ∪ [0..10]
k_0 ∈ [100..200]
- a[0] ∈ {53}
- [1] ∈ {17}
- [2] ∈ {64}
- [3] ∈ {99}
- [4] ∈ {25}
- [5] ∈ {12}
- [6] ∈ {72}
- [7] ∈ {81}
- [8] ∈ {404}
- [9] ∈ {303}
- [10] ∈ {-101}
- s2 ∈ {40; 41; 42}
- s1 ∈ {-101; 12; 17; 25; 53; 64; 72; 81; 99; 303; 404}
+ a[0] ∈ {53} or UNINITIALIZED
+ [1] ∈ {17} or UNINITIALIZED
+ [2] ∈ {64} or UNINITIALIZED
+ [3] ∈ {99} or UNINITIALIZED
+ [4] ∈ {25} or UNINITIALIZED
+ [5] ∈ {12} or UNINITIALIZED
+ [6] ∈ {72} or UNINITIALIZED
+ [7] ∈ {81} or UNINITIALIZED
+ [8] ∈ {404} or UNINITIALIZED
+ [9] ∈ {303} or UNINITIALIZED
+ [10] ∈ {-101} or UNINITIALIZED
+ s2 ∈ {40; 41; 42} or UNINITIALIZED
+ s1 ∈ {-101; 12; 17; 25; 53; 64; 72; 81; 99; 303; 404} or UNINITIALIZED
x ∈
{-101} ∪ [-25..-15] ∪ [0..10]
∪ {12; 17; 25; 40; 41; 42; 53; 64; 72; 81} ∪ [99..127] ∪ [129..200]
- ∪ {303; 404}
+ ∪ {303; 404} or UNINITIALIZED
[from] Computing for function large_ilevel
[from] Computing for function Frama_C_interval <-large_ilevel
[from] Done for function Frama_C_interval
diff --git a/tests/value/oracle/initialized.res.oracle b/tests/value/oracle/initialized.res.oracle
index 28313721c94409af21b570e0a043955e260d67e3..14418e31e5dafb8f716f7f0f49cebd248900d4a4 100644
--- a/tests/value/oracle/initialized.res.oracle
+++ b/tests/value/oracle/initialized.res.oracle
@@ -103,6 +103,7 @@
{[12][bits 24 to 31]#; [13][bits 0 to 23]#} ∈
{0x11111111; 0x22222222} or UNINITIALIZED
[13][bits 24 to 31] ∈ {0} or UNINITIALIZED
+ p_0 ∈ UNINITIALIZED
v1 ∈ {0}
i6 ∈ [--..--]
__retres ∈ UNINITIALIZED
diff --git a/tests/value/oracle/narrow_behaviors.res.oracle b/tests/value/oracle/narrow_behaviors.res.oracle
index 32fe99abc39f02de30c9f3480ff73dc9abb0f8f7..c7c34ba693151038032e7c479139f683623e7897 100644
--- a/tests/value/oracle/narrow_behaviors.res.oracle
+++ b/tests/value/oracle/narrow_behaviors.res.oracle
@@ -14,6 +14,7 @@
nondet ∈ [--..--]
p.x ∈ {2}
.y ∈ {1; 2}
+ q ∈ UNINITIALIZED
__retres ∈ UNINITIALIZED
==END OF DUMP==
[eva] narrow_behaviors.i:56:
@@ -21,6 +22,7 @@
# cvalue:
nondet ∈ {0}
p{.x; .y} ∈ {1}
+ q ∈ UNINITIALIZED
__retres ∈ UNINITIALIZED
==END OF DUMP==
[eva] computing for function f2 <- main.
@@ -83,6 +85,7 @@
# cvalue:
nondet ∈ {0}
r{.x; .y} ∈ {1}
+ s ∈ UNINITIALIZED
__retres ∈ UNINITIALIZED
==END OF DUMP==
[eva] narrow_behaviors.i:62:
@@ -90,6 +93,7 @@
# cvalue:
nondet ∈ {1}
r{.x; .y} ∈ {2}
+ s ∈ UNINITIALIZED
__retres ∈ UNINITIALIZED
==END OF DUMP==
[eva] computing for function f2 <- main.
diff --git a/tests/value/oracle/octagons-pointers-intermediate.res.oracle b/tests/value/oracle/octagons-pointers-intermediate.res.oracle
index f6f6928d4db7af08f6ab5ce3c73d7c426302cd10..cc794d3b969e2f6126394b392c2518ba8fdc2b25 100644
--- a/tests/value/oracle/octagons-pointers-intermediate.res.oracle
+++ b/tests/value/oracle/octagons-pointers-intermediate.res.oracle
@@ -30,10 +30,10 @@
elt1 ∈ {{ &buffer + [6..436] }}
elt2 ∈ {{ &buffer + [10..440] }}
elt3 ∈ {{ &buffer + [12..442] }}
- c ∈ [--..--]
- e1 ∈ [--..--]
- e2 ∈ [--..--]
- e3 ∈ [--..--]
+ c ∈ [--..--] or UNINITIALIZED
+ e1 ∈ [--..--] or UNINITIALIZED
+ e2 ∈ [--..--] or UNINITIALIZED
+ e3 ∈ [--..--] or UNINITIALIZED
[eva:final-states] Values at end of function init:
buffer[0..435] ∈ [--..--]
i ∈ {436}
diff --git a/tests/value/oracle/octagons-pointers-simple.res.oracle b/tests/value/oracle/octagons-pointers-simple.res.oracle
index b4ac5a0756733ff58a4a12d5a53b72dca2edf3a6..6051c069e6ad5299c640ecef86b415c4a847ff2e 100644
--- a/tests/value/oracle/octagons-pointers-simple.res.oracle
+++ b/tests/value/oracle/octagons-pointers-simple.res.oracle
@@ -46,10 +46,10 @@
elt1 ∈ {{ &buffer + [6..436] }}
elt2 ∈ {{ &buffer + [10..440] }}
elt3 ∈ {{ &buffer + [12..442] }}
- c ∈ [--..--]
- e1 ∈ [--..--]
- e2 ∈ [--..--]
- e3 ∈ [--..--]
+ c ∈ [--..--] or UNINITIALIZED
+ e1 ∈ [--..--] or UNINITIALIZED
+ e2 ∈ [--..--] or UNINITIALIZED
+ e3 ∈ [--..--] or UNINITIALIZED
[eva:final-states] Values at end of function init:
buffer[0..435] ∈ [--..--]
i ∈ {436}
diff --git a/tests/value/oracle/octagons-pointers.res.oracle b/tests/value/oracle/octagons-pointers.res.oracle
index dcc4c9fa9e70f408240e63200520b112956ebb1c..b3c686962e27573ab9306764637f890142d99ee8 100644
--- a/tests/value/oracle/octagons-pointers.res.oracle
+++ b/tests/value/oracle/octagons-pointers.res.oracle
@@ -90,10 +90,10 @@
elt1 ∈ {{ &buffer + [6..436] }}
elt2 ∈ {{ &buffer + [10..440] }}
elt3 ∈ {{ &buffer + [12..442] }}
- c ∈ [--..--]
- e1 ∈ [--..--]
- e2 ∈ [--..--]
- e3 ∈ [--..--]
+ c ∈ [--..--] or UNINITIALIZED
+ e1 ∈ [--..--] or UNINITIALIZED
+ e2 ∈ [--..--] or UNINITIALIZED
+ e3 ∈ [--..--] or UNINITIALIZED
[eva:final-states] Values at end of function init:
buffer[0..435] ∈ [--..--]
i ∈ {436}
diff --git a/tests/value/oracle/period.res.oracle b/tests/value/oracle/period.res.oracle
index 06bf41e67c2931c7ede6b776b660b06d2063853d..ffabad17985bafe2217dd6eaae24b6ad5f976aa4 100644
--- a/tests/value/oracle/period.res.oracle
+++ b/tests/value/oracle/period.res.oracle
@@ -77,6 +77,8 @@
Ft ∈ {2}
Gt ∈ {12}
Ht ∈ {1}
+ p ∈ UNINITIALIZED
+ vg ∈ UNINITIALIZED
==END OF DUMP==
[eva:alarm] period.c:51: Warning:
pointer downcast. assert (unsigned int)(&g) ≤ 2147483647;
diff --git a/tests/value/oracle/recursion.1.res.oracle b/tests/value/oracle/recursion.1.res.oracle
index fe28d193e06ce292c499fce259f11e0b4712d798..60fb835c758c13364113c0d52a999029bdfc65d5 100644
--- a/tests/value/oracle/recursion.1.res.oracle
+++ b/tests/value/oracle/recursion.1.res.oracle
@@ -127,7 +127,7 @@
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function alarm:
- res ∈ [2..2147483647]
+ res ∈ [2..2147483647] or UNINITIALIZED
__retres ∈ [1..2147483647]
[eva:final-states] Values at end of function decr:
@@ -147,7 +147,7 @@
x ∈ {0; 1}
b ∈ {0; 1}
[eva:final-states] Values at end of function factorial:
- res ∈ {2; 6; 24; 120}
+ res ∈ {2; 6; 24; 120} or UNINITIALIZED
__retres ∈ {1; 2; 6; 24; 120}
[eva:final-states] Values at end of function factorial_ptr:
y ∈ {91; 120}
@@ -179,7 +179,7 @@
[eva:final-states] Values at end of function precond:
y ∈ [-100..-6]
[eva:final-states] Values at end of function sum:
- res ∈ [3..91]
+ res ∈ [3..91] or UNINITIALIZED
__retres ∈ [1..91]
[eva:final-states] Values at end of function sum_and_fact:
x ∈ {11; 36}
diff --git a/tests/value/oracle/recursion.2.res.oracle b/tests/value/oracle/recursion.2.res.oracle
index 84f55cfe2e5abfe7f85dd8bc16592c62502637d0..a77a482b7f5837fed43cec25cb2e14fc1e4a543e 100644
--- a/tests/value/oracle/recursion.2.res.oracle
+++ b/tests/value/oracle/recursion.2.res.oracle
@@ -21,7 +21,7 @@
[eva] done for function main_fail
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function sum_nospec:
- res ∈ [--..--]
+ res ∈ [--..--] or UNINITIALIZED
__retres ∈ [--..--]
[eva:final-states] Values at end of function main_fail:
Frama_C_entropy_source ∈ [--..--]
diff --git a/tests/value/oracle/relations2.res.oracle b/tests/value/oracle/relations2.res.oracle
index 528534268000a5c8e8b2f177a4622b261ec7b417..30bebcad81d04ad51e45060c24564c5bf948459a 100644
--- a/tests/value/oracle/relations2.res.oracle
+++ b/tests/value/oracle/relations2.res.oracle
@@ -57,6 +57,7 @@
t ∈ [0..511]
n ∈ [0..512]
s ∈ {0}
+ b3 ∈ UNINITIALIZED
T[0] ∈ {0}
[1] ∈ {1}
[2] ∈ {42}
@@ -78,6 +79,7 @@
t ∈ [0..511]
n ∈ [0..512]
s ∈ {0; 1}
+ b3 ∈ UNINITIALIZED
T[0] ∈ {0}
[1] ∈ {1}
[2] ∈ {42}
@@ -95,6 +97,7 @@
t ∈ [0..511]
n ∈ [0..512]
s ∈ {0; 1; 2}
+ b3 ∈ UNINITIALIZED
T[0] ∈ {0}
[1] ∈ {1}
[2] ∈ {42}
@@ -112,6 +115,7 @@
t ∈ [0..511]
n ∈ [0..512]
s ∈ [0..2147483647]
+ b3 ∈ UNINITIALIZED
T[0] ∈ {0}
[1] ∈ {1}
[2] ∈ {42}
diff --git a/tests/value/traces/oracle/test1.res.oracle b/tests/value/traces/oracle/test1.res.oracle
index 687a3a1ceb615c098323649f6003c3d1315af5fd..ee037639517bec64c830931a00dcb666a0177f18 100644
--- a/tests/value/traces/oracle/test1.res.oracle
+++ b/tests/value/traces/oracle/test1.res.oracle
@@ -27,11 +27,11 @@ c -> 5
8 -> Assign: tmp = g -> 9
9 -> EnterScope: i -> 12
10 -> Assign: tmp = 2 -> 11
- 11 -> EnterScope: i -> 15
- 12 -> initialize variable: i -> 13
- 13 -> Assign: i = 0 -> 14
- 14 -> enter_loop -> 19
- 15 -> initialize variable: i -> 16
+ 11 -> EnterScope: i -> 13
+ 12 -> initialize variable: i -> 14
+ 13 -> initialize variable: i -> 16
+ 14 -> Assign: i = 0 -> 15
+ 15 -> enter_loop -> 19
16 -> Assign: i = 0 -> 17
17 -> enter_loop -> 18
18 -> Assume: i < 3 true -> 20
diff --git a/tests/value/traces/oracle/test2.res.oracle b/tests/value/traces/oracle/test2.res.oracle
index 05f84f4a876a3eb4e55d1c37823889630a3d12fa..95d7f650c02064982af9ea1947fb863ebe62726e 100644
--- a/tests/value/traces/oracle/test2.res.oracle
+++ b/tests/value/traces/oracle/test2.res.oracle
@@ -54,7 +54,7 @@ c -> 1
35 -> finalize_call: loop -> 36
36 -> Assign: tmp = \result<loop> -> 37
37 -> LeaveScope: \result<loop> -> 38
- 38 -> EnterScope: \result<main> -> 78
+ 38 -> EnterScope: \result<main> -> 79
39 -> EnterScope: j -> 40
40 -> Assign: j = tmp -> 41
41 -> EnterScope: i -> 43
@@ -74,15 +74,15 @@ c -> 1
56 -> LeaveScope: i -> 57
57 -> EnterScope: \result<loop> -> 58
58 -> Assign: \result<loop> = j -> 59
- 59 -> LeaveScope: j -> 74
- 74 -> finalize_call: loop -> 75
- 75 -> Assign: tmp = \result<loop> -> 76
- 76 -> LeaveScope: \result<loop> -> 77
- 77 -> EnterScope: \result<main> -> 80
- 78 -> Assign: \result<main> = tmp -> 79
- 79 -> join -> 82
- 80 -> Assign: \result<main> = tmp -> 81
- 81 -> join -> 82 ]} at 82
+ 59 -> LeaveScope: j -> 75
+ 75 -> finalize_call: loop -> 76
+ 76 -> Assign: tmp = \result<loop> -> 77
+ 77 -> LeaveScope: \result<loop> -> 78
+ 78 -> EnterScope: \result<main> -> 81
+ 79 -> Assign: \result<main> = tmp -> 80
+ 80 -> join -> 83
+ 81 -> Assign: \result<main> = tmp -> 82
+ 82 -> join -> 83 ]} at 83
[from] Computing for function loop
[from] Done for function loop
[from] Computing for function main
diff --git a/tests/value/traces/oracle/test3.res.oracle b/tests/value/traces/oracle/test3.res.oracle
index a8c3a78127eeeda83fc76a2c424715167708af8b..5b4cec9510857974d3dd70e8bcc965871eb4e2ac 100644
--- a/tests/value/traces/oracle/test3.res.oracle
+++ b/tests/value/traces/oracle/test3.res.oracle
@@ -17,15 +17,14 @@
{[ 0 -> initialize variable: g -> 1
1 -> initialize formal variable using type
c -> 2
- 2 -> EnterScope: __retres -> 3
- 3 -> EnterScope: tmp -> 4
- 4 -> initialize variable: tmp -> 5
- 5 -> Assign: tmp = 4 -> 6
- 6 -> Assume: tmp true -> 7
- 7 -> Assign: g = tmp -> 8
- 8 -> Assign: __retres = g + 1 -> 9
- 9 -> EnterScope: \result<main> -> 10
- 10 -> Assign: \result<main> = __retres -> 11 ]} at 11
+ 2 -> EnterScope: __retres tmp -> 3
+ 3 -> initialize variable: tmp -> 4
+ 4 -> Assign: tmp = 4 -> 5
+ 5 -> Assume: tmp true -> 6
+ 6 -> Assign: g = tmp -> 7
+ 7 -> Assign: __retres = g + 1 -> 8
+ 8 -> EnterScope: \result<main> -> 9
+ 9 -> Assign: \result<main> = __retres -> 10 ]} at 10
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
@@ -55,17 +54,15 @@ int main(int c)
int __traces_domain_return;
{
int __retres;
+ int tmp;
+ tmp = 4;
+ /*@ assert tmp ≢ 0; */
+ g = tmp;
+ __retres = g + 1;
{
- int tmp;
- tmp = 4;
- /*@ assert tmp ≢ 0; */
- g = tmp;
- __retres = g + 1;
- {
- int _result_main_;
- _result_main_ = __retres;
- __traces_domain_return = __retres;
- }
+ int _result_main_;
+ _result_main_ = __retres;
+ __traces_domain_return = __retres;
}
}
return __traces_domain_return;
diff --git a/tests/value/traces/oracle/test5.res.oracle b/tests/value/traces/oracle/test5.res.oracle
index 65e159b215ac3cdbfd7881b377f7c6fac1cd2d06..d80a1a070d8d66e05423708b843895fcffcf12e0 100644
--- a/tests/value/traces/oracle/test5.res.oracle
+++ b/tests/value/traces/oracle/test5.res.oracle
@@ -443,7 +443,7 @@ c -> 1
264 -> Assign: i = i + 1 -> 265
265 -> Assume: i < 10 true -> 266; join -> 278
266 -> EnterScope: j -> 267; join -> 280
- 267 -> initialize variable: j -> 268
+ 267 -> initialize variable: j -> 268; join -> 282
268 -> Assign: j = 0 -> 269
269 -> enter_loop -> 270
270 -> join -> 271
@@ -458,20 +458,21 @@ c -> 1
157 -> Assign: tmp = tmp_0 + tmp -> 159
159 -> LeaveScope: tmp_0 -> 160
160 -> Assign: j = j + 1 -> 162 ]} -> 273;
- join -> 285
+ join -> 286
273 -> Assume: j < 10 false -> 274
274 -> leave_loop -> 275
- 275 -> LeaveScope: j -> 276; join -> 290
- 276 -> Assign: i = i + 1 -> 277; join -> 292
+ 275 -> LeaveScope: j -> 276; join -> 291
+ 276 -> Assign: i = i + 1 -> 277; join -> 293
277 -> join -> 278
- 278 -> Assume: i < 10 true -> 279; join -> 294
+ 278 -> Assume: i < 10 true -> 279; join -> 295
279 -> join -> 280
- 280 -> EnterScope: j -> 281; join -> 296
- 281 -> initialize variable: j -> 282
- 282 -> Assign: j = 0 -> 283
- 283 -> enter_loop -> 284
- 284 -> join -> 285
- 285 -> Loop(16) 148 {[ 148 -> Assume: j < 10 true -> 149
+ 280 -> EnterScope: j -> 281; join -> 297
+ 281 -> join -> 282
+ 282 -> initialize variable: j -> 283; join -> 299
+ 283 -> Assign: j = 0 -> 284
+ 284 -> enter_loop -> 285
+ 285 -> join -> 286
+ 286 -> Loop(16) 148 {[ 148 -> Assume: j < 10 true -> 149
149 -> EnterScope: tmp_0 -> 151
151 -> EnterScope: \result<my_switch> -> 153
153 -> CallDeclared:
@@ -481,23 +482,24 @@ c -> 1
156 -> LeaveScope: \result<my_switch> -> 157
157 -> Assign: tmp = tmp_0 + tmp -> 159
159 -> LeaveScope: tmp_0 -> 160
- 160 -> Assign: j = j + 1 -> 162 ]} -> 287;
- join -> 301
- 287 -> Assume: j < 10 false -> 288
- 288 -> leave_loop -> 289
- 289 -> join -> 290
- 290 -> LeaveScope: j -> 291; join -> 306
- 291 -> join -> 292
- 292 -> Assign: i = i + 1 -> 293; join -> 308
- 293 -> join -> 294
- 294 -> Assume: i < 10 true -> 295; join -> 310
- 295 -> join -> 296
- 296 -> EnterScope: j -> 297; join -> 313
- 297 -> initialize variable: j -> 298
- 298 -> Assign: j = 0 -> 299
- 299 -> enter_loop -> 300
- 300 -> join -> 301
- 301 -> Loop(16) 148 {[ 148 -> Assume: j < 10 true -> 149
+ 160 -> Assign: j = j + 1 -> 162 ]} -> 288;
+ join -> 303
+ 288 -> Assume: j < 10 false -> 289
+ 289 -> leave_loop -> 290
+ 290 -> join -> 291
+ 291 -> LeaveScope: j -> 292; join -> 308
+ 292 -> join -> 293
+ 293 -> Assign: i = i + 1 -> 294; join -> 310
+ 294 -> join -> 295
+ 295 -> Assume: i < 10 true -> 296; join -> 312
+ 296 -> join -> 297
+ 297 -> EnterScope: j -> 298; join -> 315
+ 298 -> join -> 299
+ 299 -> initialize variable: j -> 300; join -> 317
+ 300 -> Assign: j = 0 -> 301
+ 301 -> enter_loop -> 302
+ 302 -> join -> 303
+ 303 -> Loop(16) 148 {[ 148 -> Assume: j < 10 true -> 149
149 -> EnterScope: tmp_0 -> 151
151 -> EnterScope: \result<my_switch> -> 153
153 -> CallDeclared:
@@ -507,25 +509,26 @@ c -> 1
156 -> LeaveScope: \result<my_switch> -> 157
157 -> Assign: tmp = tmp_0 + tmp -> 159
159 -> LeaveScope: tmp_0 -> 160
- 160 -> Assign: j = j + 1 -> 162 ]} -> 303;
- join -> 318
- 303 -> Assume: j < 10 false -> 304
- 304 -> leave_loop -> 305
- 305 -> join -> 306
- 306 -> LeaveScope: j -> 307; join -> 323
+ 160 -> Assign: j = j + 1 -> 162 ]} -> 305;
+ join -> 321
+ 305 -> Assume: j < 10 false -> 306
+ 306 -> leave_loop -> 307
307 -> join -> 308
- 308 -> Assign: i = i + 1 -> 309; join -> 325
+ 308 -> LeaveScope: j -> 309; join -> 326
309 -> join -> 310
- 310 -> join -> 313
- 313 -> join -> 318
- 318 -> join -> 323
- 323 -> join -> 325
- 325 -> Loop(10) 311 {[ 311 -> Assume: i < 10 true -> 312
- 312 -> EnterScope: j -> 314
- 314 -> initialize variable: j -> 315
- 315 -> Assign: j = 0 -> 316
- 316 -> enter_loop -> 317
- 317 -> Loop(16) 148 {[ 148 -> Assume:
+ 310 -> Assign: i = i + 1 -> 311; join -> 328
+ 311 -> join -> 312
+ 312 -> join -> 315
+ 315 -> join -> 317
+ 317 -> join -> 321
+ 321 -> join -> 326
+ 326 -> join -> 328
+ 328 -> Loop(10) 313 {[ 313 -> Assume: i < 10 true -> 314
+ 314 -> EnterScope: j -> 316
+ 316 -> initialize variable: j -> 318
+ 318 -> Assign: j = 0 -> 319
+ 319 -> enter_loop -> 320
+ 320 -> Loop(16) 148 {[ 148 -> Assume:
j < 10 true
-> 149
149 -> EnterScope:
@@ -551,16 +554,16 @@ c -> 1
160 -> Assign:
j = j + 1
-> 162 ]}
- -> 320
- 320 -> Assume: j < 10 false -> 321
- 321 -> leave_loop -> 322
- 322 -> LeaveScope: j -> 324
- 324 -> Assign: i = i + 1 -> 326 ]} -> 329
- 329 -> Assume: i < 10 false -> 330
- 330 -> leave_loop -> 331
- 331 -> LeaveScope: i -> 332
- 332 -> EnterScope: \result<main> -> 333
- 333 -> Assign: \result<main> = tmp -> 334 ]} at 334
+ -> 323
+ 323 -> Assume: j < 10 false -> 324
+ 324 -> leave_loop -> 325
+ 325 -> LeaveScope: j -> 327
+ 327 -> Assign: i = i + 1 -> 329 ]} -> 332
+ 332 -> Assume: i < 10 false -> 333
+ 333 -> leave_loop -> 334
+ 334 -> LeaveScope: i -> 335
+ 335 -> EnterScope: \result<main> -> 336
+ 336 -> Assign: \result<main> = tmp -> 337 ]} at 337
[from] Computing for function main
[from] Computing for function my_switch <-main
[from] Done for function my_switch