diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index fc546c883ccd75cee7a4ca1ba01d5dfebbd4736c..6122bee211191d97655a817059895e23256e5f06 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/src/plugins/eva/engine/iterator.ml
@@ -122,12 +122,6 @@ module Make_Dataflow
let active_behaviors = Logic.create AnalysisParam.initial_state kf
- (* Compute the locals that we must enter in scope when we start the analysis
- of [block]. The other ones will be introduced on the fly, when we
- encounter a [Local_init] instruction. *)
- let block_toplevel_locals block =
- List.filter (fun vi -> not vi.vdefined) block.blocals
-
let initial_states =
let state = AnalysisParam.initial_state
and call_kinstr = AnalysisParam.call_kinstr
@@ -267,8 +261,15 @@ module Make_Dataflow
: transfer_function =
lift' (fun s -> Transfer.assign s (Kstmt stmt) dest exp)
+ (* All variables local to a block are introduced in domain states when
+ entering the block. Variables explicitly initialized at declaration time
+ (for which vi.vdefined is true) enter the scope too early, as they should
+ be introduced on the fly when encountering their [Local_init] instruction.
+ However, goto statements can skip their declaration/initialization, so it
+ is safer to always introduce all local variables (without initialize them)
+ when entering a block. *)
let transfer_enter (block : block) : transfer_function =
- let vars = block_toplevel_locals block in
+ let vars = block.blocals in
if vars = [] then id else lift (Transfer.enter_scope kf vars)
let transfer_leave (block : block) : transfer_function =
@@ -289,20 +290,12 @@ module Make_Dataflow
let transfer_instr (stmt : stmt) (instr : instr) : transfer_function =
match instr with
| Local_init (vi, AssignInit exp, _loc) ->
- let kind = Abstract_domain.Local kf in
let transfer state =
- let state = Domain.enter_scope kind [vi] state in
Init.initialize_local_variable stmt vi exp state
in
lift' transfer
| Local_init (vi, ConsInit (f, args, k), loc) ->
- let kind = Abstract_domain.Local kf in
let as_func dest callee args _loc (key, state) =
- (* This variable enters the scope too early, as it should
- be introduced after the call to [f] but before the assignment
- to [v]. This is currently not possible, at least without
- splitting Transfer.call in two. *)
- let state = Domain.enter_scope kind [vi] state in
transfer_call stmt dest callee args (key, state)
in
Cil.treat_constructor_as_func as_func vi f args k loc
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/builtins/oracle_gauges/realloc.res.oracle b/tests/builtins/oracle_gauges/realloc.res.oracle
index 7db5bb2855581132216cb4aff783b868c8fd005b..317aba47d1df8261a94c9a7e59085491fc885220 100644
--- a/tests/builtins/oracle_gauges/realloc.res.oracle
+++ b/tests/builtins/oracle_gauges/realloc.res.oracle
@@ -1,4 +1,4 @@
-627a628,964
+632a633,969
> [eva] realloc.c:152: Call to builtin realloc
> [eva:malloc] bases_to_realloc: {__realloc_w_main10_l152}
> [eva:malloc] realloc.c:152: weak free on bases: {__realloc_w_main10_l152}
@@ -336,7 +336,7 @@
> __realloc_w_main10_l152[0] ∈ {4}
> [1] ∈ UNINITIALIZED
> ==END OF DUMP==
-694a1032,1096
+699a1037,1101
> [eva] realloc.c:167: Call to builtin reallocarray
> [eva] realloc.c:167: Call to builtin reallocarray
> [eva] computing for function Frama_C_interval <- main11 <- main.
@@ -402,7 +402,7 @@
> [eva:malloc] bases_to_realloc: {}
> [eva:malloc] realloc.c:171: strong free on bases: {}
> [eva] realloc.c:172: Frama_C_show_each_p: {{ NULL ; &__realloc_w_main11_l171 }}
-762,763c1164,1166
+767,768c1169,1171
< p ∈ {{ NULL ; &__malloc_main11_l160 ; (int *)&__realloc_main11_l171 }}
< q ∈ {0} or UNINITIALIZED or ESCAPINGADDR
---
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/float/oracle_equality/alarms.0.res.oracle b/tests/float/oracle_equality/alarms.0.res.oracle
index c0293cdd68b29be5e867b6afaa1bccb8c09fcc49..e275d378fa4aed2db5affd0abed177d49e5a6ac8 100644
--- a/tests/float/oracle_equality/alarms.0.res.oracle
+++ b/tests/float/oracle_equality/alarms.0.res.oracle
@@ -1,4 +1,4 @@
-137,139c137,138
+142,144c142,143
< u1{.l[bits 0 to 31]; .f; .d[bits 0 to 31]} ∈
< [-3.40282346639e+38 .. 3.40282346639e+38]
< {.l[bits 32 to 63]; .f[bits 32 to 63]; .d[bits 32 to 63]} ∈ [--..--]
diff --git a/tests/float/oracle_equality/alarms.1.res.oracle b/tests/float/oracle_equality/alarms.1.res.oracle
index 1ab35c18d93d2826bb86fc25efd9510bf94f38f1..2e54149d2b56ed8663050f77934d34fdee4b76ab 100644
--- a/tests/float/oracle_equality/alarms.1.res.oracle
+++ b/tests/float/oracle_equality/alarms.1.res.oracle
@@ -1,4 +1,4 @@
-120,121c120,121
+125,126c125,126
< u1{.l[bits 0 to 31]; .f; .d[bits 0 to 31]} ∈ [-inf .. inf]
< {.l[bits 32 to 63]; .f[bits 32 to 63]; .d[bits 32 to 63]} ∈ [--..--]
---
diff --git a/tests/float/oracle_equality/const3.1.res.oracle b/tests/float/oracle_equality/const3.1.res.oracle
index 7de759db47189f2c50ea83d7845623fa5994f43e..f13fa4f815ce32defdc347ec00f3a6b4e6d6f9a8 100644
--- a/tests/float/oracle_equality/const3.1.res.oracle
+++ b/tests/float/oracle_equality/const3.1.res.oracle
@@ -1,4 +1,4 @@
-25c25
+26c26
< d1 ∈ [0x1.16c2000000000p-133 .. 0x1.16c3000000000p-133]
---
> d1 ∈ {0x1.16c2000000000p-133}
diff --git a/tests/libc/oracle/poll.res.oracle b/tests/libc/oracle/poll.res.oracle
index 470eb611711b0cc9b9fa4e42581fe3683b321bb1..58d6b858e0834253897e1d3f8413b54bbc2b681b 100644
--- a/tests/libc/oracle/poll.res.oracle
+++ b/tests/libc/oracle/poll.res.oracle
@@ -25,7 +25,7 @@
.events ∈ {3}
.revents ∈ [--..--]
r ∈ {-1; 0; 1}
- can_read ∈ {0; 1}
- can_read_out_of_band ∈ {0; 2}
- invalid_fd ∈ {0; 32}
+ can_read ∈ {0; 1} or UNINITIALIZED
+ can_read_out_of_band ∈ {0; 2} or UNINITIALIZED
+ invalid_fd ∈ {0; 32} or UNINITIALIZED
__retres ∈ [0..127]
diff --git a/tests/libc/oracle/signal_h.res.oracle b/tests/libc/oracle/signal_h.res.oracle
index efade1922a061ad31e4bdcaa1ff5ad0f22ace360..e9c90019070b8c9ab29975147149c33539fd4379 100644
--- a/tests/libc/oracle/signal_h.res.oracle
+++ b/tests/libc/oracle/signal_h.res.oracle
@@ -289,7 +289,7 @@
s ∈ [--..--]
uninit ∈ UNINITIALIZED
old ∈ [--..--] or UNINITIALIZED
- kill_res ∈ {-1; 0}
+ kill_res ∈ {-1; 0} or UNINITIALIZED
sa1 ∈
{{ garbled mix of &{__fc_sigaction}
(origin: Library function {signal_h.c:45}) }} or UNINITIALIZED
diff --git a/tests/libc/oracle/socket.0.res.oracle b/tests/libc/oracle/socket.0.res.oracle
index 99635468b5f16ccf760bd70d5fed0ea3c85f3cd9..d721e0304f9f78829d017736c8c5013885e14fcb 100644
--- a/tests/libc/oracle/socket.0.res.oracle
+++ b/tests/libc/oracle/socket.0.res.oracle
@@ -257,10 +257,10 @@
__fc_socket_counter ∈ [--..--]
fd ∈ [-1..1023]
addr ∈ [--..--] or UNINITIALIZED
- addrlen ∈ {8}
- client_fd ∈ [-1..1023]
+ addrlen ∈ {8} or UNINITIALIZED
+ client_fd ∈ [-1..1023] or UNINITIALIZED
buf[0..63] ∈ [--..--] or UNINITIALIZED
- r ∈ [-1..64]
+ r ∈ [-1..64] or UNINITIALIZED
__retres ∈ {0; 1; 5; 20; 100; 200; 300; 400}
[eva:final-states] Values at end of function main:
__fc_fds[0..1023] ∈ [--..--]
diff --git a/tests/libc/oracle/socket.1.res.oracle b/tests/libc/oracle/socket.1.res.oracle
index 8f908c607936382b0b3797665fb94079fd895b78..543a28a7fba79583e5ea35c553c0c1b21314d5eb 100644
--- a/tests/libc/oracle/socket.1.res.oracle
+++ b/tests/libc/oracle/socket.1.res.oracle
@@ -259,10 +259,10 @@
__fc_socket_counter ∈ [--..--]
fd ∈ [-1..1023]
addr ∈ [--..--] or UNINITIALIZED
- addrlen ∈ {8}
- client_fd ∈ [-1..1023]
+ addrlen ∈ {8} or UNINITIALIZED
+ client_fd ∈ [-1..1023] or UNINITIALIZED
buf[0..63] ∈ [--..--] or UNINITIALIZED
- r ∈ [-1..64]
+ r ∈ [-1..64] or UNINITIALIZED
__retres ∈ {0; 1; 5; 20; 100; 200; 300; 400}
[eva:final-states] Values at end of function main:
__fc_fds[0..1023] ∈ [--..--]
diff --git a/tests/libc/oracle/stdio_c.res.oracle b/tests/libc/oracle/stdio_c.res.oracle
index f8f6bfd4cf10fd229513ad04118032b1104e4a79..3be99d222c709984ed1d9613c00e86b7c5aa5961 100644
--- a/tests/libc/oracle/stdio_c.res.oracle
+++ b/tests/libc/oracle/stdio_c.res.oracle
@@ -361,7 +361,7 @@
[eva:final-states] Values at end of function fgets:
Frama_C_entropy_source ∈ [--..--]
__fc_errno ∈ [--..--]
- i ∈ [0..9]
+ i ∈ [0..9] or UNINITIALIZED
buf[0..8] ∈ [--..--] or UNINITIALIZED
[9] ∈ {0} or UNINITIALIZED
__retres ∈ {{ NULL ; &buf[0] }}
@@ -389,7 +389,7 @@
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__fc_errno ∈ [--..--]
- cur ∈ [0..2147483647]
+ cur ∈ [0..2147483647] or UNINITIALIZED
line ∈
{{ NULL ; &__malloc_w_getline_l73[0] ; &__realloc_w_getline_l104[0] }}
len ∈ [0..2147483647]
@@ -410,10 +410,10 @@
len ∈ [0..2147483647]
total_len ∈ [--..--]
read ∈ {-1} or UNINITIALIZED
- c ∈ [-1..255]
+ c ∈ [-1..255] or UNINITIALIZED
buf[0..8] ∈ [--..--] or UNINITIALIZED
[9] ∈ {0} or UNINITIALIZED
- r_1 ∈ {{ NULL ; &buf[0] }}
+ r_1 ∈ {{ NULL ; &buf[0] }} or UNINITIALIZED
__retres ∈ {0; 1}
__malloc_w_getline_l73[0..1] ∈ [--..--] or UNINITIALIZED
__realloc_w_getline_l104[0..2147483645] ∈ [--..--] or UNINITIALIZED
diff --git a/tests/libc/oracle/stdio_h.res.oracle b/tests/libc/oracle/stdio_h.res.oracle
index 8d5fe316aa1d5626a2165cfa25ecec40bc30f211..1757917375ac3a89a698ac499ebff3729f37a62d 100644
--- a/tests/libc/oracle/stdio_h.res.oracle
+++ b/tests/libc/oracle/stdio_h.res.oracle
@@ -172,14 +172,14 @@
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
f ∈ {{ NULL ; &__fc_fopen + [0..120],0%8 }}
- r ∈ [--..--]
- tmp_2 ∈ {{ NULL ; &__fc_fopen + [0..120],0%8 }}
- told ∈ [-1..2147483647]
- toldo ∈ [-1..2147483647]
- redirected ∈ {{ NULL ; &__fc_fopen + [0..120],0%8 }}
+ r ∈ [--..--] or UNINITIALIZED
+ tmp_2 ∈ {{ NULL ; &__fc_fopen + [0..120],0%8 }} or UNINITIALIZED
+ told ∈ [-1..2147483647] or UNINITIALIZED
+ toldo ∈ [-1..2147483647] or UNINITIALIZED
+ redirected ∈ {{ NULL ; &__fc_fopen + [0..120],0%8 }} or UNINITIALIZED
fgets_buf0[0] ∈ [--..--] or UNINITIALIZED
- fgets_res ∈ {{ NULL ; &fgets_buf0[0] }}
+ fgets_res ∈ {{ NULL ; &fgets_buf0[0] }} or UNINITIALIZED
pos ∈ [--..--] or UNINITIALIZED
- res_fclose ∈ {-1; 0}
+ res_fclose ∈ {-1; 0} or UNINITIALIZED
__retres ∈ {0; 1; 2; 3}
S___fc_stdout[0..1] ∈ [--..--]
diff --git a/tests/libc/oracle/stdlib_c.0.res.oracle b/tests/libc/oracle/stdlib_c.0.res.oracle
index 276e662d50c399250dce2614e96308566c68c36b..6e7d8414d9bfec2d30151afdd104223983bdef11 100644
--- a/tests/libc/oracle/stdlib_c.0.res.oracle
+++ b/tests/libc/oracle/stdlib_c.0.res.oracle
@@ -256,7 +256,7 @@
resolved_name ∈
{{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] ;
&__malloc_realpath_l224_0[0] }}
- realpath_len ∈ [1..4096]
+ realpath_len ∈ [1..4096] or UNINITIALIZED
__retres ∈
{{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] ;
&__malloc_realpath_l224_0[0] }}
@@ -285,8 +285,8 @@
p_memal_res ∈ {0; 12}
p_memal_res2 ∈ {0; 12}
resolved_name ∈ {{ NULL ; &__malloc_main_l44[0] }}
- realpath_res ∈ {{ NULL ; &__malloc_realpath_l224[0] }}
- canon ∈ {{ NULL ; &__malloc_realpath_l224_0[0] }}
+ realpath_res ∈ {{ NULL ; &__malloc_realpath_l224[0] }} or UNINITIALIZED
+ canon ∈ {{ NULL ; &__malloc_realpath_l224_0[0] }} or UNINITIALIZED
__retres ∈ {0; 1}
__calloc_w_main_l33[0..1073741823] ∈ {0; 42}
__malloc_main_l44[0..4095] ∈ [--..--] or UNINITIALIZED
diff --git a/tests/libc/oracle/stdlib_c.1.res.oracle b/tests/libc/oracle/stdlib_c.1.res.oracle
index 95a6a6d6b063be4bf82b8f17affcbf3e9e09f9fe..8268d02f205f892166fe3a4645898cbcf235fc75 100644
--- a/tests/libc/oracle/stdlib_c.1.res.oracle
+++ b/tests/libc/oracle/stdlib_c.1.res.oracle
@@ -274,7 +274,7 @@
resolved_name ∈
{{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] ;
&__malloc_realpath_l224_0[0] }}
- realpath_len ∈ [1..4096]
+ realpath_len ∈ [1..4096] or UNINITIALIZED
__retres ∈
{{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] ;
&__malloc_realpath_l224_0[0] }}
diff --git a/tests/libc/oracle/stdlib_c.2.res.oracle b/tests/libc/oracle/stdlib_c.2.res.oracle
index 8090933af98958cc3fd154206444496df7d62a26..2dad09f22b8979bdfa7c27c7d7b0de76d0d17d1d 100644
--- a/tests/libc/oracle/stdlib_c.2.res.oracle
+++ b/tests/libc/oracle/stdlib_c.2.res.oracle
@@ -208,7 +208,7 @@
l ∈ [0..4294967292],0%4
p ∈
{{ NULL ; &__malloc_calloc_l72[0] ; &__malloc_calloc_l72_0[0] ;
- &__malloc_w_calloc_l72_1[0] }}
+ &__malloc_w_calloc_l72_1[0] }} or UNINITIALIZED
__retres ∈
{{ NULL ; (void *)&__malloc_calloc_l72 ;
(void *)&__malloc_calloc_l72_0 ;
@@ -228,7 +228,7 @@
resolved_name ∈
{{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] ;
&__malloc_realpath_l224_0[0] }}
- realpath_len ∈ [1..4096]
+ realpath_len ∈ [1..4096] or UNINITIALIZED
__retres ∈
{{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] ;
&__malloc_realpath_l224_0[0] }}
@@ -254,8 +254,8 @@
p_memal_res ∈ {0; 12}
p_memal_res2 ∈ {0; 12}
resolved_name ∈ {{ NULL ; &__malloc_main_l44[0] }}
- realpath_res ∈ {{ NULL ; &__malloc_realpath_l224[0] }}
- canon ∈ {{ NULL ; &__malloc_realpath_l224_0[0] }}
+ realpath_res ∈ {{ NULL ; &__malloc_realpath_l224[0] }} or UNINITIALIZED
+ canon ∈ {{ NULL ; &__malloc_realpath_l224_0[0] }} or UNINITIALIZED
__retres ∈ {0; 1}
__malloc_calloc_l72[0..3] ∈ [--..--] or UNINITIALIZED
__malloc_calloc_l72_0[0..4294967291] ∈ [--..--] or UNINITIALIZED
diff --git a/tests/libc/oracle/stdlib_c_env.res.oracle b/tests/libc/oracle/stdlib_c_env.res.oracle
index 54a82b9cccb4eb9a4b3fdbe277fce4ba362608a6..6c927c63c406cec5304736c2c1d03891621f516a 100644
--- a/tests/libc/oracle/stdlib_c_env.res.oracle
+++ b/tests/libc/oracle/stdlib_c_env.res.oracle
@@ -291,7 +291,7 @@
__fc_env[0..4095] ∈
{{ NULL ; &s[0] ; &__fc_env_strings + [0..63] ; "BLA=1" }}
Frama_C_entropy_source ∈ [--..--]
- namelen ∈ [0..63]
+ namelen ∈ [0..63] or UNINITIALIZED
__fc_env_strings[0..62] ∈ [--..--]
[63] ∈ {0}
__retres ∈ {-1; 0}
@@ -299,7 +299,7 @@
__fc_env[0..4095] ∈
{{ NULL ; &s[0] ; &__fc_env_strings + [0..63] ; "BLA=1" }}
Frama_C_entropy_source ∈ [--..--]
- namelen ∈ [0..63]
+ namelen ∈ [0..63] or UNINITIALIZED
__retres ∈ {-1; 0}
[eva:final-states] Values at end of function main:
__fc_env[0..4095] ∈
diff --git a/tests/libc/oracle/sys_sendfile_h.res.oracle b/tests/libc/oracle/sys_sendfile_h.res.oracle
index a77a6d78706e75bc12d5c497f8ab3a3595aadd83..b214dddf4a669a0b9b00116eb551a3ad6404f598 100644
--- a/tests/libc/oracle/sys_sendfile_h.res.oracle
+++ b/tests/libc/oracle/sys_sendfile_h.res.oracle
@@ -73,8 +73,8 @@
__fc_fds[0..1023] ∈ [--..--]
out_fd ∈ [-1..1023] or UNINITIALIZED
in_fd ∈ [-1..1023]
- offset ∈ [--..--]
+ offset ∈ [--..--] or UNINITIALIZED
r1 ∈ [-1..42] or UNINITIALIZED
r3 ∈ [-1..42] or UNINITIALIZED
- r ∈ {-1; 0}
+ r ∈ {-1; 0} or UNINITIALIZED
__retres ∈ {0; 1}
diff --git a/tests/libc/oracle/sys_socket_h.res.oracle b/tests/libc/oracle/sys_socket_h.res.oracle
index bd668507be702ce8fb2db931063de1a8cea31f2a..916cb12aab73ea390d49446a7d751126a79c1e28 100644
--- a/tests/libc/oracle/sys_socket_h.res.oracle
+++ b/tests/libc/oracle/sys_socket_h.res.oracle
@@ -61,5 +61,5 @@
.msg_iovlen ∈ {5; 6}
{.msg_control; .msg_controllen; .msg_flags} ∈ UNINITIALIZED
sockfd ∈ [-1..1023]
- r ∈ [-1..2147483647]
+ r ∈ [-1..2147483647] or UNINITIALIZED
__retres ∈ {0; 1}
diff --git a/tests/libc/oracle/sys_stat_h.res.oracle b/tests/libc/oracle/sys_stat_h.res.oracle
index edb2f90be28452d72fa2645a8b131995f355ded9..8ee1daff1c0849cf02deee1acf713362f0983e0e 100644
--- a/tests/libc/oracle/sys_stat_h.res.oracle
+++ b/tests/libc/oracle/sys_stat_h.res.oracle
@@ -113,16 +113,16 @@
__fc_fds[0..1023] ∈ [--..--]
fd ∈ [-1..1023]
st ∈ [--..--] or UNINITIALIZED
- r ∈ {-1; 0}
- r_mkdir ∈ {-1; 0}
- old_mask ∈ [--..--]
- r2 ∈ {-1; 0}
- r3 ∈ {-1; 0}
- r4 ∈ {-1; 0}
- r5 ∈ {-1; 0}
- r6 ∈ {-1; 0}
- r7 ∈ {-1; 0}
+ r ∈ {-1; 0} or UNINITIALIZED
+ r_mkdir ∈ {-1; 0} or UNINITIALIZED
+ old_mask ∈ [--..--] or UNINITIALIZED
+ r2 ∈ {-1; 0} or UNINITIALIZED
+ r3 ∈ {-1; 0} or UNINITIALIZED
+ r4 ∈ {-1; 0} or UNINITIALIZED
+ r5 ∈ {-1; 0} or UNINITIALIZED
+ r6 ∈ {-1; 0} or UNINITIALIZED
+ r7 ∈ {-1; 0} or UNINITIALIZED
buf ∈ [--..--] or UNINITIALIZED
- r8 ∈ {-1; 0}
- r9 ∈ {-1; 0}
+ r8 ∈ {-1; 0} or UNINITIALIZED
+ r9 ∈ {-1; 0} or UNINITIALIZED
__retres ∈ {-1; 0; 1; 2; 3}
diff --git a/tests/libc/oracle/sys_uio_h.res.oracle b/tests/libc/oracle/sys_uio_h.res.oracle
index b19e97d241f4703fe0cf1811e4b5e03c67f8b0d2..35c0c56e12390bfb59a0337eef1d87b048eb2d68 100644
--- a/tests/libc/oracle/sys_uio_h.res.oracle
+++ b/tests/libc/oracle/sys_uio_h.res.oracle
@@ -103,6 +103,6 @@
[3].iov_base ∈ {{ (void *)&buf2 }}
[3].iov_len ∈ {14}
fd ∈ [-1..1023]
- w ∈ [-1..2147483647]
- r ∈ [-1..2147483647]
+ w ∈ [-1..2147483647] or UNINITIALIZED
+ r ∈ [-1..2147483647] or UNINITIALIZED
__retres ∈ [-2..2147483647]
diff --git a/tests/libc/oracle/termios.res.oracle b/tests/libc/oracle/termios.res.oracle
index 799c219eaa98136c7c028bfaab8990f86edede99..c37ece069c778bbece4c9d262f1a6c157894df79 100644
--- a/tests/libc/oracle/termios.res.oracle
+++ b/tests/libc/oracle/termios.res.oracle
@@ -70,6 +70,6 @@
fd ∈ [-1..1023]
tio ∈ [--..--] or UNINITIALIZED
res ∈ {-1; 0}
- sp1 ∈ [--..--]
- sp2 ∈ [--..--]
+ sp1 ∈ [--..--] or UNINITIALIZED
+ sp2 ∈ [--..--] or UNINITIALIZED
__retres ∈ {-1; 0; 1; 8}
diff --git a/tests/libc/oracle/time_h.res.oracle b/tests/libc/oracle/time_h.res.oracle
index a32b98d7871f1de7738a4e07da647fc39b86cf35..e2c79167c90417685953eeb91b4ac0efb4f8f344 100644
--- a/tests/libc/oracle/time_h.res.oracle
+++ b/tests/libc/oracle/time_h.res.oracle
@@ -263,12 +263,12 @@
r ∈ {-1; 0; 4; 22}
creq.tv_sec ∈ [--..--] or UNINITIALIZED
.tv_nsec ∈ [0..999999999] or UNINITIALIZED
- tt ∈ {42}
- time_str ∈ {{ &__fc_ctime[0] }}
- mytime ∈ [--..--]
- t ∈ [--..--]
+ tt ∈ {42} or UNINITIALIZED
+ time_str ∈ {{ &__fc_ctime[0] }} or UNINITIALIZED
+ mytime ∈ [--..--] or UNINITIALIZED
+ t ∈ [--..--] or UNINITIALIZED
res_time ∈ {{ NULL ; &mytime2 }} or UNINITIALIZED
mytime2 ∈ [--..--] or UNINITIALIZED
- localp ∈ {{ NULL ; &localr }}
+ localp ∈ {{ NULL ; &localr }} or UNINITIALIZED
localr ∈ [--..--] or UNINITIALIZED
__retres ∈ {0; 1; 2}
diff --git a/tests/libc/oracle/unistd_h.0.res.oracle b/tests/libc/oracle/unistd_h.0.res.oracle
index 69911d84a7244a5f0a797b6dfe46824a5ca3c93b..5290754d8d489a081d47cdd8a12bb28370890be2 100644
--- a/tests/libc/oracle/unistd_h.0.res.oracle
+++ b/tests/libc/oracle/unistd_h.0.res.oracle
@@ -621,24 +621,24 @@
r ∈ {-1; 0}
hostname[0..255] ∈ [--..--] or UNINITIALIZED
fd ∈ [-1..1023]
- offset ∈ [-1..2147483647]
- fd2 ∈ [-1..1023]
- pid ∈ [-1..2147483647]
- l ∈ [--..--]
+ offset ∈ [-1..2147483647] or UNINITIALIZED
+ fd2 ∈ [-1..1023] or UNINITIALIZED
+ pid ∈ [-1..2147483647] or UNINITIALIZED
+ l ∈ [--..--] or UNINITIALIZED
cwd[0..63] ∈ [--..--] or UNINITIALIZED
- res_getcwd ∈ {{ NULL ; &cwd[0] }}
- pconf ∈ [--..--]
+ res_getcwd ∈ {{ NULL ; &cwd[0] }} or UNINITIALIZED
+ pconf ∈ [--..--] or UNINITIALIZED
ruid ∈ [--..--] or UNINITIALIZED
euid ∈ [--..--] or UNINITIALIZED
suid ∈ [--..--] or UNINITIALIZED
rgid ∈ [--..--] or UNINITIALIZED
egid ∈ [--..--] or UNINITIALIZED
sgid ∈ [--..--] or UNINITIALIZED
- p ∈ [--..--]
- tty ∈ {{ NULL ; &__fc_ttyname[0] }}
+ p ∈ [--..--] or UNINITIALIZED
+ tty ∈ {{ NULL ; &__fc_ttyname[0] }} or UNINITIALIZED
halfpipe ∈ UNINITIALIZED
pipefd[0..1] ∈ [0..1023] or UNINITIALIZED
- unslept ∈ [0..42]
+ unslept ∈ [0..42] or UNINITIALIZED
buf[0..4294967294] ∈ [--..--] or UNINITIALIZED
- rread ∈ [--..--]
+ rread ∈ [--..--] or UNINITIALIZED
__retres ∈ {0; 1}
diff --git a/tests/libc/oracle/unistd_h.1.res.oracle b/tests/libc/oracle/unistd_h.1.res.oracle
index 85607de98dd75b610ec922e97d6186922ef614cc..68dbe4ab19c2f105825affd2569f87495687327e 100644
--- a/tests/libc/oracle/unistd_h.1.res.oracle
+++ b/tests/libc/oracle/unistd_h.1.res.oracle
@@ -621,24 +621,24 @@
r ∈ {-1; 0}
hostname[0..255] ∈ [--..--] or UNINITIALIZED
fd ∈ [-1..1023]
- offset ∈ [-1..2147483647]
- fd2 ∈ [-1..1023]
- pid ∈ [-1..2147483647]
- l ∈ [--..--]
+ offset ∈ [-1..2147483647] or UNINITIALIZED
+ fd2 ∈ [-1..1023] or UNINITIALIZED
+ pid ∈ [-1..2147483647] or UNINITIALIZED
+ l ∈ [--..--] or UNINITIALIZED
cwd[0..63] ∈ [--..--] or UNINITIALIZED
- res_getcwd ∈ {{ NULL ; &cwd[0] }}
- pconf ∈ [--..--]
+ res_getcwd ∈ {{ NULL ; &cwd[0] }} or UNINITIALIZED
+ pconf ∈ [--..--] or UNINITIALIZED
ruid ∈ [--..--] or UNINITIALIZED
euid ∈ [--..--] or UNINITIALIZED
suid ∈ [--..--] or UNINITIALIZED
rgid ∈ [--..--] or UNINITIALIZED
egid ∈ [--..--] or UNINITIALIZED
sgid ∈ [--..--] or UNINITIALIZED
- p ∈ [--..--]
- tty ∈ {{ NULL ; &__fc_ttyname[0] }}
+ p ∈ [--..--] or UNINITIALIZED
+ tty ∈ {{ NULL ; &__fc_ttyname[0] }} or UNINITIALIZED
halfpipe ∈ UNINITIALIZED
pipefd[0..1] ∈ [0..1023] or UNINITIALIZED
- unslept ∈ [0..42]
+ unslept ∈ [0..42] or UNINITIALIZED
buf[0..4294967294] ∈ [--..--] or UNINITIALIZED
- rread ∈ [--..--]
+ rread ∈ [--..--] or UNINITIALIZED
__retres ∈ {0; 1}
diff --git a/tests/libc/oracle/wchar_c_h.0.res.oracle b/tests/libc/oracle/wchar_c_h.0.res.oracle
index e9e310ee417d1524c5e016661bcbad7ee654197e..7974bac0fc9ad3f3e83b11495623c5f36d11b5f5 100644
--- a/tests/libc/oracle/wchar_c_h.0.res.oracle
+++ b/tests/libc/oracle/wchar_c_h.0.res.oracle
@@ -307,12 +307,13 @@
r ∈ [--..--] or UNINITIALIZED
i ∈ [--..--]
res ∈ {{ NULL ; &buf[0] ; L"Needle" + [0..--],0%4 }}
- wc_0 ∈ {{ L"ABC" }}
- p ∈ {{ L"ABC" + {4} }}
- wcr ∈ {{ L"ABC" + {8} }}
- wmr1 ∈ {0}
- wmr2 ∈ {{ L"ABC" + {8} }}
- dupbuf ∈ {{ NULL ; &__malloc_wcsdup_l99_0[0] }} or ESCAPINGADDR
+ wc_0 ∈ {{ L"ABC" }} or UNINITIALIZED
+ p ∈ {{ L"ABC" + {4} }} or UNINITIALIZED
+ wcr ∈ {{ L"ABC" + {8} }} or UNINITIALIZED
+ wmr1 ∈ {0} or UNINITIALIZED
+ wmr2 ∈ {{ L"ABC" + {8} }} or UNINITIALIZED
+ dupbuf ∈
+ {{ NULL ; &__malloc_wcsdup_l99_0[0] }} or UNINITIALIZED or ESCAPINGADDR
__retres ∈ {0}
__malloc_wcsdup_l99[0] ∈ {65}
[1] ∈ {66}
diff --git a/tests/libc/oracle/wchar_c_h.1.res.oracle b/tests/libc/oracle/wchar_c_h.1.res.oracle
index 1d03e1b33af9b398bdd1645f1c9b1dac1647cd1a..3c6efb2a6ee2b20d4222a4cb41a63f4a12ffeeb5 100644
--- a/tests/libc/oracle/wchar_c_h.1.res.oracle
+++ b/tests/libc/oracle/wchar_c_h.1.res.oracle
@@ -224,9 +224,9 @@
r ∈ [--..--] or UNINITIALIZED
i ∈ [--..--]
res ∈ {{ NULL ; &buf[0] ; L"Needle" + [0..--],0%4 }}
- wc_0 ∈ {{ L"ABC" }}
- p ∈ {{ L"ABC" + {4} }}
- wcr ∈ {{ L"ABC" + {8} }}
- wmr1 ∈ {0}
- wmr2 ∈ {{ L"ABC" + {8} }}
+ wc_0 ∈ {{ L"ABC" }} or UNINITIALIZED
+ p ∈ {{ L"ABC" + {4} }} or UNINITIALIZED
+ wcr ∈ {{ L"ABC" + {8} }} or UNINITIALIZED
+ wmr1 ∈ {0} or UNINITIALIZED
+ wmr2 ∈ {{ L"ABC" + {8} }} or UNINITIALIZED
__retres ∈ {0}
diff --git a/tests/libc/oracle/wchar_h.res.oracle b/tests/libc/oracle/wchar_h.res.oracle
index a58e0252f356cfb46334eaf577744d07b643d2e9..4e50f74af67f626a0e7ee94e1b57298845c2b7fd 100644
--- a/tests/libc/oracle/wchar_h.res.oracle
+++ b/tests/libc/oracle/wchar_h.res.oracle
@@ -199,14 +199,14 @@
fd ∈ {{ NULL ; &__fc_fopen + [0..120],0%8 }}
buf[0..28] ∈ [--..--] or UNINITIALIZED
[29] ∈ UNINITIALIZED
- res ∈ {{ NULL ; &buf[0] }}
+ res ∈ {{ NULL ; &buf[0] }} or UNINITIALIZED
buf2[0] ∈ {97} or UNINITIALIZED
[1] ∈ {98} or UNINITIALIZED
- r ∈ {{ &wdst[0] }}
- wsrc ∈ {{ L"wide thing" }}
+ r ∈ {{ &wdst[0] }} or UNINITIALIZED
+ wsrc ∈ {{ L"wide thing" }} or UNINITIALIZED
wdst[0..9] ∈ [--..--] or UNINITIALIZED
- wdst2[0..9] ∈ {65}
- [10] ∈ {0}
- [11..19] ∈ [--..--]
- ir ∈ [--..--]
+ wdst2[0..9] ∈ {65} or UNINITIALIZED
+ [10] ∈ {0} or UNINITIALIZED
+ [11..19] ∈ [--..--] or UNINITIALIZED
+ ir ∈ [--..--] or UNINITIALIZED
__retres ∈ {0; 1}
diff --git a/tests/value/goto.i b/tests/value/goto.i
index 9a2430a1ea5d4a1b921525accb73c3fdead213bb..d4f59d0f5f204915b4a34d746c742d066a7661a2 100644
--- a/tests/value/goto.i
+++ b/tests/value/goto.i
@@ -1,6 +1,28 @@
+/* run.config*
+ STDOPT: +""
+*/
+
+volatile int nondet;
+
int stop () {
L: goto L;
+}
+void skip_declaration(void) {
+ int y, r;
+ if (nondet) {
+ goto l; // This goto skips the declaration of variable x below.
+ }
+ int x = 1;
+ y = 2;
+ l: // x and y are both uninitialized when coming from the goto
+ //@ check unknown: \initialized(&x);
+ //@ check unknown: x > 0;
+ //@ check unknown: \initialized(&y);
+ //@ check unknown: y > 0;
+ r = x + 1; // An initialization alarm must be emitted.
+ r = y + 1; // An initialization alarm must be emitted.
+ return;
}
int main() {
@@ -9,4 +31,5 @@ int main() {
if (c) stop ();
+ skip_declaration ();
}
diff --git a/tests/value/oracle/goto.res.oracle b/tests/value/oracle/goto.res.oracle
index 0a9dd76826c68ef0f40dc613d3f63b92164468c9..d258a57ce28334b1b75d3f60ccc672bdaa19745f 100644
--- a/tests/value/oracle/goto.res.oracle
+++ b/tests/value/oracle/goto.res.oracle
@@ -3,19 +3,37 @@
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-
+ nondet ∈ [--..--]
[eva] computing for function stop <- main.
- Called from goto.i:10.
+ Called from goto.i:32.
[eva] Recording results for stop
[eva] Done for function stop
+[eva] computing for function skip_declaration <- main.
+ Called from goto.i:34.
+[eva:alarm] goto.i:19: Warning: check 'unknown' got status unknown.
+[eva:alarm] goto.i:20: Warning: check 'unknown' got status unknown.
+[eva:alarm] goto.i:21: Warning: check 'unknown' got status unknown.
+[eva:alarm] goto.i:22: Warning: check 'unknown' got status unknown.
+[eva:alarm] goto.i:23: Warning:
+ accessing uninitialized left-value. assert \initialized(&x);
+[eva:alarm] goto.i:24: Warning:
+ accessing uninitialized left-value. assert \initialized(&y);
+[eva] Recording results for skip_declaration
+[eva] Done for function skip_declaration
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function skip_declaration:
+ y ∈ {2}
+ r ∈ {3}
+ x ∈ {1}
[eva:final-states] Values at end of function stop:
NON TERMINATING FUNCTION
[eva:final-states] Values at end of function main:
c ∈ [--..--]
__retres ∈ {0}
+[from] Computing for function skip_declaration
+[from] Done for function skip_declaration
[from] Computing for function stop
[from] Non-terminating function stop (no dependencies)
[from] Done for function stop
@@ -23,11 +41,17 @@
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
+[from] Function skip_declaration:
+ NO EFFECTS
[from] Function stop:
NON TERMINATING - NO EFFECTS
[from] Function main:
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function skip_declaration:
+ y; r; x
+[inout] Inputs for function skip_declaration:
+ nondet
[inout] Out (internal) for function stop:
\nothing
[inout] Inputs for function stop:
@@ -35,4 +59,4 @@
[inout] Out (internal) for function main:
c; __retres
[inout] Inputs for function main:
- \nothing
+ nondet
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/oracle_apron/relations2.res.oracle b/tests/value/oracle_apron/relations2.res.oracle
index 826838be9fa828494778a91aa0b0b45ae7026db1..529a4f0974996512fd0f6d58ff7601c9c945a29e 100644
--- a/tests/value/oracle_apron/relations2.res.oracle
+++ b/tests/value/oracle_apron/relations2.res.oracle
@@ -6,26 +6,26 @@
< [eva] relations2.i:17: Frama_C_show_each_end: [0..4294967295], [0..64]
---
> [eva] relations2.i:17: Frama_C_show_each_end: [0..1023], [0..64]
-68,70d67
+69,71d68
< [eva:alarm] relations2.i:34: Warning:
< accessing out of bounds index.
< assert (unsigned int)(i - (unsigned int)(t + 1)) < 514;
-123,124d119
+127,128d123
< [eva:alarm] relations2.i:35: Warning:
< signed overflow. assert s + b3 ≤ 2147483647;
-139c134
+143c138
< len ∈ [--..--]
---
> len ∈ [0..1023]
-182c177
+186c181
< \result FROM a[0..513]
---
> \result FROM a[0..511]
-198c193
+202c197
< a[0..513]
---
> a[0..511]
-202c197
+206c201
< sv; a[0..513]; T[0..6]
---
> sv; a[0..511]; T[0..6]
diff --git a/tests/value/oracle_equality/period.res.oracle b/tests/value/oracle_equality/period.res.oracle
index 208bb785c666f3d05fd6161dba406ac1cf4ae010..3cc5b3eeaf65b71667a3736906ec69e7ac2eedb5 100644
--- a/tests/value/oracle_equality/period.res.oracle
+++ b/tests/value/oracle_equality/period.res.oracle
@@ -1,9 +1,9 @@
-87,92d86
+89,94d88
< [eva:alarm] period.c:53: Warning:
< pointer downcast. assert (unsigned int)(&g) ≤ 2147483647;
< [eva] period.c:53:
< Assigning imprecise value to p.
< The imprecision originates from Arithmetic {period.c:53}
< [eva:alarm] period.c:54: Warning: out of bounds read. assert \valid_read(p);
-97d90
+99d92
< [scope:rm_asserts] removing 1 assertion(s)
diff --git a/tests/value/oracle_equality/relations2.res.oracle b/tests/value/oracle_equality/relations2.res.oracle
index f28c7db295829a43b3ea15839fda057ad54c22b5..c4950d71433bcd95ffcca1ceb9f583bab746e94c 100644
--- a/tests/value/oracle_equality/relations2.res.oracle
+++ b/tests/value/oracle_equality/relations2.res.oracle
@@ -2,5 +2,5 @@
< n ∈ [0..512]
---
> n ∈ [1..512]
-132d131
+136d135
< [eva] relations2.i:57: Frama_C_show_each_NO2:
diff --git a/tests/value/oracle_octagon/relations2.res.oracle b/tests/value/oracle_octagon/relations2.res.oracle
index a250063ee008db59cb92ba3ce23ff4eb5bfd0ad8..8f7073190ffa96e9117aa9e657a6bbae0ccc8a3b 100644
--- a/tests/value/oracle_octagon/relations2.res.oracle
+++ b/tests/value/oracle_octagon/relations2.res.oracle
@@ -10,35 +10,35 @@
< n ∈ [0..512]
---
> n ∈ [1..512]
-68,70d67
+69,71d68
< [eva:alarm] relations2.i:34: Warning:
< accessing out of bounds index.
< assert (unsigned int)(i - (unsigned int)(t + 1)) < 514;
-79c76
+80c77
< n ∈ [0..512]
---
> n ∈ [1..512]
-96c93
+98c95
< n ∈ [0..512]
---
> n ∈ [1..512]
-113c110
+116c113
< n ∈ [0..512]
---
> n ∈ [1..512]
-139c136
+143c140
< len ∈ [--..--]
---
> len ∈ [0..1023]
-182c179
+186c183
< \result FROM a[0..513]
---
> \result FROM a[0..511]
-198c195
+202c199
< a[0..513]
---
> a[0..511]
-202c199
+206c203
< sv; a[0..513]; T[0..6]
---
> sv; a[0..511]; T[0..6]
diff --git a/tests/value/oracle_symblocs/relations2.res.oracle b/tests/value/oracle_symblocs/relations2.res.oracle
index c58e8b748b82010d71f12f9f376e3ff067b60777..5c2ddb21fb2be059c5739d24c65a1b29be90b79c 100644
--- a/tests/value/oracle_symblocs/relations2.res.oracle
+++ b/tests/value/oracle_symblocs/relations2.res.oracle
@@ -1,2 +1,2 @@
-132d131
+136d135
< [eva] relations2.i:57: Frama_C_show_each_NO2:
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