diff --git a/tests/value/traces/oracle/test1.res.oracle b/tests/value/traces/oracle/test1.res.oracle
index fb550f92c6ddb17fd2c0dd399f71bccabdba4219..011f6645879b2f33794ba38f1a6e4aff01c49281 100644
--- a/tests/value/traces/oracle/test1.res.oracle
+++ b/tests/value/traces/oracle/test1.res.oracle
@@ -1,17 +1,17 @@
[kernel] Parsing tests/value/traces/test1.c (with preprocessing)
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value:initial-state] Values of globals at initialization
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
entropy_source ∈ [--..--]
g ∈ {42}
-[value] Recording results for main
-[value] done for function main
-[value] ====== VALUES COMPUTED ======
-[value:final-states] Values at end of function main:
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
g ∈ {5; 45}
tmp ∈ {5; 45}
-[value:d-traces] Trace domains:
+[eva:d-traces] Trace domains:
start: 0; globals = g, entropy_source; main_formals = c;
{[ 0 -> initialize variable: entropy_source -> 1
1 -> initialize variable using type Library_Global
@@ -22,64 +22,66 @@ entropy_source -> 2
c -> 5
5 -> EnterScope: tmp -> 6
6 -> Assign: tmp = 0 -> 7
- 7 -> Assume: c false -> 8; Assume: c true -> 9
- 8 -> Assign: tmp = 2 -> 12
- 9 -> Assign: tmp = g -> 11
- 11 -> EnterScope: i -> 17
- 12 -> EnterScope: i -> 14
- 14 -> initialize variable: i -> 15
- 15 -> Assign: i = 0 -> 16
- 16 -> enter_loop -> 22
- 17 -> initialize variable: i -> 18
- 18 -> Assign: i = 0 -> 19
- 19 -> enter_loop -> 21
- 21 -> Assume: i < 3 true -> 24
- 22 -> Assume: i < 3 true -> 25
- 24 -> Assign: tmp = tmp + 1 -> 27
- 25 -> Assign: tmp = tmp + 1 -> 26
- 26 -> Assign: i = i + 1 -> 28
- 27 -> Assign: i = i + 1 -> 29
- 28 -> Assume: i < 3 true -> 34
- 29 -> Assume: i < 3 true -> 33
- 33 -> Assign: tmp = tmp + 1 -> 36
- 34 -> Assign: tmp = tmp + 1 -> 35
- 35 -> Assign: i = i + 1 -> 38
- 36 -> Assign: i = i + 1 -> 37
- 37 -> Assume: i < 3 true -> 44
- 38 -> Assume: i < 3 true -> 43
- 43 -> Assign: tmp = tmp + 1 -> 46
- 44 -> Assign: tmp = tmp + 1 -> 45
- 45 -> Assign: i = i + 1 -> 48
- 46 -> Assign: i = i + 1 -> 47
- 47 -> Assume: i < 3 false -> 54
- 48 -> Assume: i < 3 false -> 53
- 53 -> LeaveScope: i -> 55
- 54 -> LeaveScope: i -> 56
- 55 -> Assign: g = tmp -> 58
- 56 -> Assign: g = tmp -> 57
- 57 -> join -> 59
- 58 -> join -> 59 ]} at 59
+ 7 -> Assume: c true -> 8; Assume: c false -> 10
+ 8 -> Assign: tmp = g -> 9
+ 9 -> EnterScope: i -> 15
+ 10 -> Assign: tmp = 2 -> 11
+ 11 -> EnterScope: i -> 12
+ 12 -> initialize variable: i -> 13
+ 13 -> Assign: i = 0 -> 14
+ 14 -> enter_loop -> 19
+ 15 -> initialize variable: i -> 16
+ 16 -> Assign: i = 0 -> 17
+ 17 -> enter_loop -> 18
+ 18 -> Assume: i < 3 true -> 20
+ 19 -> Assume: i < 3 true -> 21
+ 20 -> Assign: tmp = tmp + 1 -> 23
+ 21 -> Assign: tmp = tmp + 1 -> 22
+ 22 -> Assign: i = i + 1 -> 24
+ 23 -> Assign: i = i + 1 -> 25
+ 24 -> Assume: i < 3 true -> 27
+ 25 -> Assume: i < 3 true -> 26
+ 26 -> Assign: tmp = tmp + 1 -> 29
+ 27 -> Assign: tmp = tmp + 1 -> 28
+ 28 -> Assign: i = i + 1 -> 30
+ 29 -> Assign: i = i + 1 -> 31
+ 30 -> Assume: i < 3 true -> 33
+ 31 -> Assume: i < 3 true -> 32
+ 32 -> Assign: tmp = tmp + 1 -> 35
+ 33 -> Assign: tmp = tmp + 1 -> 34
+ 34 -> Assign: i = i + 1 -> 36
+ 35 -> Assign: i = i + 1 -> 37
+ 36 -> Assume: i < 3 false -> 39
+ 37 -> Assume: i < 3 false -> 38
+ 38 -> LeaveScope: i -> 40
+ 39 -> LeaveScope: i -> 41
+ 40 -> LeaveScope: i -> 42
+ 41 -> LeaveScope: i -> 43
+ 42 -> Assign: g = tmp -> 45
+ 43 -> Assign: g = tmp -> 44
+ 44 -> join -> 46
+ 45 -> join -> 46 ]} at 46
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
+ These dependencies hold at termination for the executions that terminate:
[from] Function main:
g FROM g; c
\result FROM g; c
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
- g; tmp; i
+ g; tmp; i
[inout] Inputs for function main:
- g
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value:initial-state] Values of globals at initialization
+ g
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
entropy_source ∈ [--..--]
g ∈ {42}
-[value] done for function main
-[value] ====== VALUES COMPUTED ======
-[value:final-states] Values at end of function main:
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
g ∈ {5; 45}
__traces_domain_return ∈ {5; 45}
/* Generated by Frama-C */
diff --git a/tests/value/traces/oracle/test2.res.oracle b/tests/value/traces/oracle/test2.res.oracle
index b855d5a78193a13bdf03f4fd99d2c83ae5902ceb..963ee92ec44b1f6a9de50e1a4d8d4929ce75452e 100644
--- a/tests/value/traces/oracle/test2.res.oracle
+++ b/tests/value/traces/oracle/test2.res.oracle
@@ -1,110 +1,112 @@
[kernel] Parsing tests/value/traces/test2.i (no preprocessing)
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value:initial-state] Values of globals at initialization
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
-[value] computing for function loop <- main.
- Called from tests/value/traces/test2.i:18.
-[value] Recording results for loop
-[value] Done for function loop
-[value] computing for function loop <- main.
- Called from tests/value/traces/test2.i:18.
-[value] Recording results for loop
-[value] Done for function loop
-[value] Recording results for main
-[value] done for function main
-[value] ====== VALUES COMPUTED ======
-[value:final-states] Values at end of function loop:
+[eva] computing for function loop <- main.
+ Called from tests/value/traces/test2.i:18.
+[eva] Recording results for loop
+[eva] Done for function loop
+[eva] computing for function loop <- main.
+ Called from tests/value/traces/test2.i:18.
+[eva] Recording results for loop
+[eva] Done for function loop
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function loop:
j ∈ {4; 5}
-[value:final-states] Values at end of function main:
+[eva:final-states] Values at end of function main:
tmp ∈ {4; 5}
-[value:d-traces] Trace domains:
+[eva:d-traces] Trace domains:
start: 0; globals = ; main_formals = c;
{[ 0 -> initialize variable using type Main_Formal
c -> 1
1 -> EnterScope: tmp -> 2
2 -> Assign: tmp = 0 -> 3
- 3 -> Assume: c false -> 4; Assume: c true -> 5
- 4 -> Assign: tmp = 2 -> 8
- 5 -> Assign: tmp = 1 -> 7
- 7 -> start_call: loop (true) -> 9
- 8 -> start_call: loop (true) -> 45
- 9 -> EnterScope: j -> 10
- 10 -> Assign: j = tmp -> 11
- 11 -> EnterScope: i -> 12
- 12 -> initialize variable: i -> 13
- 13 -> Assign: i = 0 -> 14
- 14 -> enter_loop -> 15
- 15 -> Assume: i < 3 true -> 16
- 16 -> Assign: j = j + 1 -> 17
- 17 -> Assign: i = i + 1 -> 18
- 18 -> Assume: i < 3 true -> 20
- 20 -> Assign: j = j + 1 -> 21
- 21 -> Assign: i = i + 1 -> 22
- 22 -> Assume: i < 3 true -> 25
- 25 -> Assign: j = j + 1 -> 26
- 26 -> Assign: i = i + 1 -> 27
- 27 -> Assume: i < 3 false -> 30
- 30 -> LeaveScope: i -> 31
- 31 -> EnterScope: \result<loop> -> 32
- 32 -> Assign: \result<loop> = j -> 33
- 33 -> LeaveScope: j -> 41
- 41 -> finalize_call: loop -> 42
- 42 -> Assign: tmp = \result<loop> -> 43
- 43 -> LeaveScope: \result<loop> -> 44
- 44 -> join -> 90
- 45 -> EnterScope: j -> 46
- 46 -> Assign: j = tmp -> 47
- 47 -> EnterScope: i -> 49
- 49 -> initialize variable: i -> 50
- 50 -> Assign: i = 0 -> 51
- 51 -> enter_loop -> 52
- 52 -> Assume: i < 3 true -> 53
- 53 -> Assign: j = j + 1 -> 54
- 54 -> Assign: i = i + 1 -> 55
- 55 -> Assume: i < 3 true -> 57
- 57 -> Assign: j = j + 1 -> 58
- 58 -> Assign: i = i + 1 -> 59
- 59 -> Assume: i < 3 true -> 62
- 62 -> Assign: j = j + 1 -> 63
- 63 -> Assign: i = i + 1 -> 64
- 64 -> Assume: i < 3 false -> 67
- 67 -> LeaveScope: i -> 68
- 68 -> EnterScope: \result<loop> -> 69
- 69 -> Assign: \result<loop> = j -> 70
- 70 -> LeaveScope: j -> 86
- 86 -> finalize_call: loop -> 87
- 87 -> Assign: tmp = \result<loop> -> 88
- 88 -> LeaveScope: \result<loop> -> 89
- 89 -> join -> 90 ]} at 90
+ 3 -> Assume: c true -> 4; Assume: c false -> 6
+ 4 -> Assign: tmp = 1 -> 5
+ 5 -> start_call: loop (true) -> 8
+ 6 -> Assign: tmp = 2 -> 7
+ 7 -> start_call: loop (true) -> 40
+ 8 -> EnterScope: j -> 9
+ 9 -> Assign: j = tmp -> 10
+ 10 -> EnterScope: i -> 11
+ 11 -> initialize variable: i -> 12
+ 12 -> Assign: i = 0 -> 13
+ 13 -> enter_loop -> 14
+ 14 -> Assume: i < 3 true -> 15
+ 15 -> Assign: j = j + 1 -> 16
+ 16 -> Assign: i = i + 1 -> 17
+ 17 -> Assume: i < 3 true -> 18
+ 18 -> Assign: j = j + 1 -> 19
+ 19 -> Assign: i = i + 1 -> 20
+ 20 -> Assume: i < 3 true -> 21
+ 21 -> Assign: j = j + 1 -> 22
+ 22 -> Assign: i = i + 1 -> 23
+ 23 -> Assume: i < 3 false -> 24
+ 24 -> LeaveScope: i -> 25
+ 25 -> LeaveScope: i -> 26
+ 26 -> EnterScope: \result<loop> -> 27
+ 27 -> Assign: \result<loop> = j -> 28
+ 28 -> LeaveScope: j -> 36
+ 36 -> finalize_call: loop -> 37
+ 37 -> Assign: tmp = \result<loop> -> 38
+ 38 -> LeaveScope: \result<loop> -> 39
+ 39 -> join -> 79
+ 40 -> EnterScope: j -> 41
+ 41 -> Assign: j = tmp -> 42
+ 42 -> EnterScope: i -> 44
+ 44 -> initialize variable: i -> 45
+ 45 -> Assign: i = 0 -> 46
+ 46 -> enter_loop -> 47
+ 47 -> Assume: i < 3 true -> 48
+ 48 -> Assign: j = j + 1 -> 49
+ 49 -> Assign: i = i + 1 -> 50
+ 50 -> Assume: i < 3 true -> 51
+ 51 -> Assign: j = j + 1 -> 52
+ 52 -> Assign: i = i + 1 -> 53
+ 53 -> Assume: i < 3 true -> 54
+ 54 -> Assign: j = j + 1 -> 55
+ 55 -> Assign: i = i + 1 -> 56
+ 56 -> Assume: i < 3 false -> 57
+ 57 -> LeaveScope: i -> 58
+ 58 -> LeaveScope: i -> 59
+ 59 -> EnterScope: \result<loop> -> 60
+ 60 -> Assign: \result<loop> = j -> 61
+ 61 -> LeaveScope: j -> 75
+ 75 -> finalize_call: loop -> 76
+ 76 -> Assign: tmp = \result<loop> -> 77
+ 77 -> LeaveScope: \result<loop> -> 78
+ 78 -> join -> 79 ]} at 79
[from] Computing for function loop
[from] Done for function loop
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
+ These dependencies hold at termination for the executions that terminate:
[from] Function loop:
\result FROM j
[from] Function main:
\result FROM c
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function loop:
- j; i
+ j; i
[inout] Inputs for function loop:
- \nothing
+ \nothing
[inout] Out (internal) for function main:
- tmp
+ tmp
[inout] Inputs for function main:
- \nothing
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value:initial-state] Values of globals at initialization
+ \nothing
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
-[value] done for function main
-[value] ====== VALUES COMPUTED ======
-[value:final-states] Values at end of function main:
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
__traces_domain_return ∈ {4; 5}
/* Generated by Frama-C */
int main(int c)
diff --git a/tests/value/traces/oracle/test3.res.oracle b/tests/value/traces/oracle/test3.res.oracle
index a5b57bde5acf7d84a5c476dbb1a5189d34493629..f773988a12d52fc2da93b1de8d6c5128169f9529 100644
--- a/tests/value/traces/oracle/test3.res.oracle
+++ b/tests/value/traces/oracle/test3.res.oracle
@@ -1,17 +1,17 @@
[kernel] Parsing tests/value/traces/test3.i (no preprocessing)
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value:initial-state] Values of globals at initialization
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
g ∈ {0}
-[value] Recording results for main
-[value] done for function main
-[value] ====== VALUES COMPUTED ======
-[value:final-states] Values at end of function main:
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
g ∈ {4}
tmp ∈ {4}
__retres ∈ {5}
-[value:d-traces] Trace domains:
+[eva:d-traces] Trace domains:
start: 0; globals = g; main_formals = c;
{[ 0 -> initialize variable: g -> 1
1 -> initialize variable using type Main_Formal
@@ -26,23 +26,23 @@ c -> 2
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
+ These dependencies hold at termination for the executions that terminate:
[from] Function main:
g FROM \nothing
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
- g; tmp; __retres
+ g; tmp; __retres
[inout] Inputs for function main:
- g
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value:initial-state] Values of globals at initialization
+ g
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
g ∈ {0}
-[value] done for function main
-[value] ====== VALUES COMPUTED ======
-[value:final-states] Values at end of function main:
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
g ∈ {4}
__traces_domain_return ∈ {5}
/* Generated by Frama-C */
diff --git a/tests/value/traces/oracle/test4.res.oracle b/tests/value/traces/oracle/test4.res.oracle
index f8b7c0adf4e3b670b9ac1ebd202c72f91e5c44c7..58d76d1237695a1dc97a49ef367b042c67f254ce 100644
--- a/tests/value/traces/oracle/test4.res.oracle
+++ b/tests/value/traces/oracle/test4.res.oracle
@@ -1,22 +1,28 @@
[kernel] Parsing tests/value/traces/test4.i (no preprocessing)
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value:initial-state] Values of globals at initialization
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
-tests/value/traces/test4.i:9:[value] entering loop for the first time
-tests/value/traces/test4.i:11:[value] warning: signed overflow. assert tmp + 1 ≤ 2147483647;
-tests/value/traces/test4.i:14:[value] warning: signed overflow. assert tmp + 1 ≤ 2147483647;
-tests/value/traces/test4.i:17:[value] warning: signed overflow. assert tmp + 1 ≤ 2147483647;
-tests/value/traces/test4.i:20:[value] warning: signed overflow. assert tmp + 1 ≤ 2147483647;
-tests/value/traces/test4.i:23:[value] warning: signed overflow. assert tmp + 1 ≤ 2147483647;
-tests/value/traces/test4.i:25:[value] warning: signed overflow. assert tmp + 1 ≤ 2147483647;
-[value] Recording results for main
-[value] done for function main
-[value] ====== VALUES COMPUTED ======
-[value:final-states] Values at end of function main:
+[eva] tests/value/traces/test4.i:9: starting to merge loop iterations
+[eva:alarm] tests/value/traces/test4.i:11: Warning:
+ signed overflow. assert tmp + 1 ≤ 2147483647;
+[eva:alarm] tests/value/traces/test4.i:14: Warning:
+ signed overflow. assert tmp + 1 ≤ 2147483647;
+[eva:alarm] tests/value/traces/test4.i:17: Warning:
+ signed overflow. assert tmp + 1 ≤ 2147483647;
+[eva:alarm] tests/value/traces/test4.i:20: Warning:
+ signed overflow. assert tmp + 1 ≤ 2147483647;
+[eva:alarm] tests/value/traces/test4.i:23: Warning:
+ signed overflow. assert tmp + 1 ≤ 2147483647;
+[eva:alarm] tests/value/traces/test4.i:25: Warning:
+ signed overflow. assert tmp + 1 ≤ 2147483647;
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
tmp ∈ [46..2147483647]
-[value:d-traces] Trace domains:
+[eva:d-traces] Trace domains:
start: 0; globals = ; main_formals = c;
{[ 0 -> initialize variable using type Main_Formal
c -> 1
@@ -35,233 +41,234 @@ c -> 1
13 -> Assume: i % 11 false -> 14
14 -> Assign: tmp = tmp + 1 -> 15
15 -> Assign: i = i + 1 -> 16
- 16 -> Assume: i < 100 true -> 18
- 18 -> Assume: i % 2 true -> 19
- 19 -> Assign: tmp = tmp + 1 -> 20
- 20 -> Assume: i % 3 true -> 21
- 21 -> Assign: tmp = tmp + 1 -> 22
- 22 -> Assume: i % 5 true -> 23
- 23 -> Assign: tmp = tmp + 1 -> 24
- 24 -> Assume: i % 7 true -> 25
- 25 -> Assign: tmp = tmp + 1 -> 26
- 26 -> Assume: i % 11 true -> 27
+ 16 -> Assume: i < 100 true -> 17
+ 17 -> Assume: i % 2 true -> 18
+ 18 -> Assign: tmp = tmp + 1 -> 19
+ 19 -> Assume: i % 3 true -> 20
+ 20 -> Assign: tmp = tmp + 1 -> 21
+ 21 -> Assume: i % 5 true -> 22
+ 22 -> Assign: tmp = tmp + 1 -> 23
+ 23 -> Assume: i % 7 true -> 24
+ 24 -> Assign: tmp = tmp + 1 -> 25
+ 25 -> Assume: i % 11 true -> 26
+ 26 -> Assign: tmp = tmp + 1 -> 27
27 -> Assign: tmp = tmp + 1 -> 28
- 28 -> Assign: tmp = tmp + 1 -> 29
- 29 -> Assign: i = i + 1 -> 30
- 30 -> Assume: i < 100 true -> 33
- 33 -> Assume: i % 2 false -> 34
- 34 -> Assume: i % 3 true -> 35
- 35 -> Assign: tmp = tmp + 1 -> 36
- 36 -> Assume: i % 5 true -> 38
+ 28 -> Assign: i = i + 1 -> 29
+ 29 -> Assume: i < 100 true -> 30
+ 30 -> Assume: i % 2 false -> 31
+ 31 -> Assume: i % 3 true -> 32
+ 32 -> Assign: tmp = tmp + 1 -> 33
+ 33 -> Assume: i % 5 true -> 34
+ 34 -> Assign: tmp = tmp + 1 -> 35
+ 35 -> Assume: i % 7 true -> 36
+ 36 -> Assign: tmp = tmp + 1 -> 37
+ 37 -> Assume: i % 11 true -> 38
38 -> Assign: tmp = tmp + 1 -> 39
- 39 -> Assume: i % 7 true -> 41
- 41 -> Assign: tmp = tmp + 1 -> 42
- 42 -> Assume: i % 11 true -> 44
- 44 -> Assign: tmp = tmp + 1 -> 45
- 45 -> Assign: tmp = tmp + 1 -> 47
- 47 -> Assign: i = i + 1 -> 48
- 48 -> Assume: i < 100 true -> 51
- 51 -> Assume: i % 2 true -> 52
- 52 -> Assign: tmp = tmp + 1 -> 53
- 53 -> Assume: i % 3 false -> 55
- 55 -> Assume: i % 5 true -> 56
+ 39 -> Assign: tmp = tmp + 1 -> 40
+ 40 -> Assign: i = i + 1 -> 41
+ 41 -> Assume: i < 100 true -> 42
+ 42 -> Assume: i % 2 true -> 43
+ 43 -> Assign: tmp = tmp + 1 -> 44
+ 44 -> Assume: i % 3 false -> 45
+ 45 -> Assume: i % 5 true -> 46
+ 46 -> Assign: tmp = tmp + 1 -> 47
+ 47 -> Assume: i % 7 true -> 48
+ 48 -> Assign: tmp = tmp + 1 -> 49
+ 49 -> Assume: i % 11 true -> 50
+ 50 -> Assign: tmp = tmp + 1 -> 51
+ 51 -> Assign: tmp = tmp + 1 -> 52
+ 52 -> Assign: i = i + 1 -> 53
+ 53 -> Assume: i < 100 true -> 54
+ 54 -> Assume: i % 2 false -> 55
+ 55 -> Assume: i % 3 true -> 56
56 -> Assign: tmp = tmp + 1 -> 57
- 57 -> Assume: i % 7 true -> 59
- 59 -> Assign: tmp = tmp + 1 -> 60
- 60 -> Assume: i % 11 true -> 62
+ 57 -> Assume: i % 5 true -> 58
+ 58 -> Assign: tmp = tmp + 1 -> 59
+ 59 -> Assume: i % 7 true -> 60
+ 60 -> Assign: tmp = tmp + 1 -> 61
+ 61 -> Assume: i % 11 true -> 62
62 -> Assign: tmp = tmp + 1 -> 63
- 63 -> Assign: tmp = tmp + 1 -> 65
- 65 -> Assign: i = i + 1 -> 66
- 66 -> Assume: i < 100 true -> 69
- 69 -> Assume: i % 2 false -> 70
- 70 -> Assume: i % 3 true -> 71
- 71 -> Assign: tmp = tmp + 1 -> 72
- 72 -> Assume: i % 5 true -> 74
+ 63 -> Assign: tmp = tmp + 1 -> 64
+ 64 -> Assign: i = i + 1 -> 65
+ 65 -> Assume: i < 100 true -> 66
+ 66 -> Assume: i % 2 true -> 67
+ 67 -> Assign: tmp = tmp + 1 -> 68
+ 68 -> Assume: i % 3 true -> 69
+ 69 -> Assign: tmp = tmp + 1 -> 70
+ 70 -> Assume: i % 5 false -> 71
+ 71 -> Assume: i % 7 true -> 72
+ 72 -> Assign: tmp = tmp + 1 -> 73
+ 73 -> Assume: i % 11 true -> 74
74 -> Assign: tmp = tmp + 1 -> 75
- 75 -> Assume: i % 7 true -> 77
- 77 -> Assign: tmp = tmp + 1 -> 78
- 78 -> Assume: i % 11 true -> 80
- 80 -> Assign: tmp = tmp + 1 -> 81
- 81 -> Assign: tmp = tmp + 1 -> 83
- 83 -> Assign: i = i + 1 -> 84
- 84 -> Assume: i < 100 true -> 87
- 87 -> Assume: i % 2 true -> 88
- 88 -> Assign: tmp = tmp + 1 -> 89
- 89 -> Assume: i % 3 true -> 91
- 91 -> Assign: tmp = tmp + 1 -> 92
- 92 -> Assume: i % 5 false -> 94
- 94 -> Assume: i % 7 true -> 95
- 95 -> Assign: tmp = tmp + 1 -> 96
- 96 -> Assume: i % 11 true -> 98
+ 75 -> Assign: tmp = tmp + 1 -> 76
+ 76 -> Assign: i = i + 1 -> 77
+ 77 -> Assume: i < 100 true -> 78
+ 78 -> Assume: i % 2 false -> 79
+ 79 -> Assume: i % 3 false -> 80
+ 80 -> Assume: i % 5 true -> 81
+ 81 -> Assign: tmp = tmp + 1 -> 82
+ 82 -> Assume: i % 7 true -> 83
+ 83 -> Assign: tmp = tmp + 1 -> 84
+ 84 -> Assume: i % 11 true -> 85
+ 85 -> Assign: tmp = tmp + 1 -> 86
+ 86 -> Assign: tmp = tmp + 1 -> 87
+ 87 -> Assign: i = i + 1 -> 88
+ 88 -> Assume: i < 100 true -> 89
+ 89 -> Assume: i % 2 true -> 90
+ 90 -> Assign: tmp = tmp + 1 -> 91
+ 91 -> Assume: i % 3 true -> 92
+ 92 -> Assign: tmp = tmp + 1 -> 93
+ 93 -> Assume: i % 5 true -> 94
+ 94 -> Assign: tmp = tmp + 1 -> 95
+ 95 -> Assume: i % 7 false -> 96
+ 96 -> Assume: i % 11 true -> 97
+ 97 -> Assign: tmp = tmp + 1 -> 98
98 -> Assign: tmp = tmp + 1 -> 99
- 99 -> Assign: tmp = tmp + 1 -> 101
- 101 -> Assign: i = i + 1 -> 102
- 102 -> Assume: i < 100 true -> 105
- 105 -> Assume: i % 2 false -> 106
- 106 -> Assume: i % 3 false -> 107
- 107 -> Assume: i % 5 true -> 108
- 108 -> Assign: tmp = tmp + 1 -> 109
- 109 -> Assume: i % 7 true -> 111
- 111 -> Assign: tmp = tmp + 1 -> 112
- 112 -> Assume: i % 11 true -> 114
+ 99 -> Assign: i = i + 1 -> 100
+ 100 -> Assume: i < 100 true -> 101
+ 101 -> Assume: i % 2 false -> 102
+ 102 -> Assume: i % 3 true -> 103
+ 103 -> Assign: tmp = tmp + 1 -> 104
+ 104 -> Assume: i % 5 true -> 105
+ 105 -> Assign: tmp = tmp + 1 -> 106
+ 106 -> Assume: i % 7 true -> 107
+ 107 -> Assign: tmp = tmp + 1 -> 108
+ 108 -> Assume: i % 11 true -> 109
+ 109 -> Assign: tmp = tmp + 1 -> 110
+ 110 -> Assign: tmp = tmp + 1 -> 111
+ 111 -> Assign: i = i + 1 -> 112
+ 112 -> Assume: i < 100 true -> 113
+ 113 -> Assume: i % 2 true -> 114
114 -> Assign: tmp = tmp + 1 -> 115
- 115 -> Assign: tmp = tmp + 1 -> 117
- 117 -> Assign: i = i + 1 -> 118
- 118 -> Assume: i < 100 true -> 121
- 121 -> Assume: i % 2 true -> 122
+ 115 -> Assume: i % 3 false -> 116
+ 116 -> Assume: i % 5 true -> 117
+ 117 -> Assign: tmp = tmp + 1 -> 118
+ 118 -> Assume: i % 7 true -> 119
+ 119 -> Assign: tmp = tmp + 1 -> 120
+ 120 -> Assume: i % 11 true -> 121
+ 121 -> Assign: tmp = tmp + 1 -> 122
122 -> Assign: tmp = tmp + 1 -> 123
- 123 -> Assume: i % 3 true -> 125
- 125 -> Assign: tmp = tmp + 1 -> 126
- 126 -> Assume: i % 5 true -> 128
- 128 -> Assign: tmp = tmp + 1 -> 129
- 129 -> Assume: i % 7 false -> 131
- 131 -> Assume: i % 11 true -> 132
+ 123 -> Assign: i = i + 1 -> 124
+ 124 -> Assume: i < 100 true -> 125; join -> 136
+ 125 -> Assume: i % 2 false -> 126; join -> 138
+ 126 -> Assume: i % 3 true -> 127; join -> 143
+ 127 -> Assign: tmp = tmp + 1 -> 128
+ 128 -> Assume: i % 5 false -> 129; join -> 146
+ 129 -> Assume: i % 7 true -> 130; join -> 151
+ 130 -> Assign: tmp = tmp + 1 -> 131
+ 131 -> Assume: i % 11 true -> 132; join -> 154
132 -> Assign: tmp = tmp + 1 -> 133
- 133 -> Assign: tmp = tmp + 1 -> 135
- 135 -> Assign: i = i + 1 -> 136
- 136 -> Assume: i < 100 true -> 139
- 139 -> Assume: i % 2 false -> 140
- 140 -> Assume: i % 3 true -> 141
- 141 -> Assign: tmp = tmp + 1 -> 142
- 142 -> Assume: i % 5 true -> 144
+ 133 -> Assign: tmp = tmp + 1 -> 134; join -> 159
+ 134 -> Assign: i = i + 1 -> 135; join -> 161
+ 135 -> join -> 136
+ 136 -> Assume: i < 100 true -> 137; join -> 163
+ 137 -> join -> 138
+ 138 -> Assume: i % 2 true -> 139; Assume: i % 2 false -> 141; join -> 165
+ 139 -> Assign: tmp = tmp + 1 -> 140
+ 140 -> join -> 142
+ 141 -> join -> 142
+ 142 -> join -> 143
+ 143 -> Assume: i % 3 true -> 144; join -> 170
144 -> Assign: tmp = tmp + 1 -> 145
- 145 -> Assume: i % 7 true -> 147
+ 145 -> join -> 146
+ 146 -> Assume: i % 5 true -> 147; Assume: i % 5 false -> 149; join -> 175
147 -> Assign: tmp = tmp + 1 -> 148
- 148 -> Assume: i % 11 true -> 150
- 150 -> Assign: tmp = tmp + 1 -> 151
- 151 -> Assign: tmp = tmp + 1 -> 153
- 153 -> Assign: i = i + 1 -> 154
- 154 -> Assume: i < 100 true -> 157
- 157 -> Assume: i % 2 true -> 158
- 158 -> Assign: tmp = tmp + 1 -> 159
- 159 -> Assume: i % 3 false -> 161
- 161 -> Assume: i % 5 true -> 162
- 162 -> Assign: tmp = tmp + 1 -> 163
- 163 -> Assume: i % 7 true -> 165
- 165 -> Assign: tmp = tmp + 1 -> 166
- 166 -> Assume: i % 11 true -> 168
- 168 -> Assign: tmp = tmp + 1 -> 169
- 169 -> Assign: tmp = tmp + 1 -> 171
- 171 -> Assign: i = i + 1 -> 172
- 172 -> Assume: i < 100 true -> 175; join -> 190
- 175 -> Assume: i % 2 false -> 176; join -> 193
- 176 -> Assume: i % 3 true -> 177; join -> 199
- 177 -> Assign: tmp = tmp + 1 -> 178
- 178 -> Assume: i % 5 false -> 180; join -> 203
- 180 -> Assume: i % 7 true -> 181; join -> 209
- 181 -> Assign: tmp = tmp + 1 -> 182
- 182 -> Assume: i % 11 true -> 184; join -> 213
- 184 -> Assign: tmp = tmp + 1 -> 185
- 185 -> Assign: tmp = tmp + 1 -> 187; join -> 219
- 187 -> Assign: i = i + 1 -> 188; join -> 221
- 188 -> join -> 190
- 190 -> Assume: i < 100 true -> 192; join -> 224
+ 148 -> join -> 150
+ 149 -> join -> 150
+ 150 -> join -> 151
+ 151 -> Assume: i % 7 true -> 152; join -> 180
+ 152 -> Assign: tmp = tmp + 1 -> 153
+ 153 -> join -> 154
+ 154 -> Assume: i % 11 true -> 155; Assume: i % 11 false -> 157;
+ join -> 183
+ 155 -> Assign: tmp = tmp + 1 -> 156; join -> 185
+ 156 -> join -> 158
+ 157 -> join -> 158
+ 158 -> join -> 159
+ 159 -> Assign: tmp = tmp + 1 -> 160; join -> 189
+ 160 -> join -> 161
+ 161 -> Assign: i = i + 1 -> 162; join -> 191
+ 162 -> join -> 163
+ 163 -> Assume: i < 100 true -> 164; join -> 193
+ 164 -> join -> 165
+ 165 -> Assume: i % 2 true -> 166; Assume: i % 2 false -> 168; join -> 196
+ 166 -> Assign: tmp = tmp + 1 -> 167
+ 167 -> join -> 169
+ 168 -> join -> 169
+ 169 -> join -> 170
+ 170 -> Assume: i % 3 true -> 171; Assume: i % 3 false -> 173; join -> 201
+ 171 -> Assign: tmp = tmp + 1 -> 172
+ 172 -> join -> 174
+ 173 -> join -> 174
+ 174 -> join -> 175
+ 175 -> Assume: i % 5 true -> 176; Assume: i % 5 false -> 178; join -> 206
+ 176 -> Assign: tmp = tmp + 1 -> 177
+ 177 -> join -> 179
+ 178 -> join -> 179
+ 179 -> join -> 180
+ 180 -> Assume: i % 7 true -> 181; join -> 211
+ 181 -> Assign: tmp = tmp + 1 -> 182; join -> 213
+ 182 -> join -> 183
+ 183 -> Assume: i % 11 true -> 184; Assume: i % 11 false -> 187;
+ join -> 217
+ 184 -> join -> 185
+ 185 -> Assign: tmp = tmp + 1 -> 186; join -> 219
+ 186 -> join -> 188
+ 187 -> join -> 188
+ 188 -> join -> 189
+ 189 -> Assign: tmp = tmp + 1 -> 190; join -> 223
+ 190 -> join -> 191
+ 191 -> Assign: i = i + 1 -> 192; join -> 225
192 -> join -> 193
- 193 -> Assume: i % 2 false -> 194; Assume: i % 2 true -> 195; join -> 227
- 194 -> join -> 198
- 195 -> Assign: tmp = tmp + 1 -> 196
- 196 -> join -> 198
- 198 -> join -> 199
- 199 -> Assume: i % 3 true -> 200; join -> 233
- 200 -> Assign: tmp = tmp + 1 -> 201
- 201 -> join -> 203
- 203 -> Assume: i % 5 false -> 204; Assume: i % 5 true -> 205; join -> 239
- 204 -> join -> 208
- 205 -> Assign: tmp = tmp + 1 -> 206
- 206 -> join -> 208
- 208 -> join -> 209
- 209 -> Assume: i % 7 true -> 210; join -> 245
- 210 -> Assign: tmp = tmp + 1 -> 211
+ 193 -> join -> 196
+ 196 -> join -> 201
+ 201 -> join -> 206
+ 206 -> join -> 211
211 -> join -> 213
- 213 -> Assume: i % 11 false -> 214; Assume: i % 11 true -> 215;
- join -> 249
- 214 -> join -> 218
- 215 -> Assign: tmp = tmp + 1 -> 216; join -> 252
- 216 -> join -> 218
- 218 -> join -> 219
- 219 -> Assign: tmp = tmp + 1 -> 220; join -> 256
- 220 -> join -> 221
- 221 -> Assign: i = i + 1 -> 222; join -> 258
- 222 -> join -> 224
- 224 -> Assume: i < 100 true -> 226; join -> 261
- 226 -> join -> 227
- 227 -> Assume: i % 2 false -> 228; Assume: i % 2 true -> 229; join -> 265
- 228 -> join -> 232
- 229 -> Assign: tmp = tmp + 1 -> 230
- 230 -> join -> 232
- 232 -> join -> 233
- 233 -> Assume: i % 3 false -> 234; Assume: i % 3 true -> 235; join -> 271
- 234 -> join -> 238
- 235 -> Assign: tmp = tmp + 1 -> 236
- 236 -> join -> 238
- 238 -> join -> 239
- 239 -> Assume: i % 5 false -> 240; Assume: i % 5 true -> 241; join -> 277
- 240 -> join -> 244
- 241 -> Assign: tmp = tmp + 1 -> 242
- 242 -> join -> 244
- 244 -> join -> 245
- 245 -> Assume: i % 7 true -> 246; join -> 283
- 246 -> Assign: tmp = tmp + 1 -> 247; join -> 286
- 247 -> join -> 249
- 249 -> Assume: i % 11 false -> 250; Assume: i % 11 true -> 251;
- join -> 290
- 250 -> join -> 255
- 251 -> join -> 252
- 252 -> Assign: tmp = tmp + 1 -> 253; join -> 293
- 253 -> join -> 255
- 255 -> join -> 256
- 256 -> Assign: tmp = tmp + 1 -> 257; join -> 297
- 257 -> join -> 258
- 258 -> Assign: i = i + 1 -> 259; join -> 299
- 259 -> join -> 261
- 261 -> join -> 265
- 265 -> join -> 271
- 271 -> join -> 277
- 277 -> join -> 283
- 283 -> join -> 286
- 286 -> join -> 290
- 290 -> join -> 293
- 293 -> join -> 297
- 297 -> join -> 299
- 299 -> Loop(4) 262 {[ 262 -> Assume: i < 100 true -> 264
- 264 -> Assume: i % 2 false -> 266;
- Assume: i % 2 true -> 267
- 266 -> join -> 270
- 267 -> Assign: tmp = tmp + 1 -> 268
- 268 -> join -> 270
- 270 -> Assume: i % 3 false -> 272;
- Assume: i % 3 true -> 273
- 272 -> join -> 276
- 273 -> Assign: tmp = tmp + 1 -> 274
- 274 -> join -> 276
- 276 -> Assume: i % 5 false -> 278;
- Assume: i % 5 true -> 279
- 278 -> join -> 282
- 279 -> Assign: tmp = tmp + 1 -> 280
- 280 -> join -> 282
- 282 -> Assume: i % 7 false -> 284;
- Assume: i % 7 true -> 285
- 284 -> join -> 289
- 285 -> Assign: tmp = tmp + 1 -> 287
- 287 -> join -> 289
- 289 -> Assume: i % 11 false -> 291;
- Assume: i % 11 true -> 292
- 291 -> join -> 296
- 292 -> Assign: tmp = tmp + 1 -> 294
- 294 -> join -> 296
- 296 -> Assign: tmp = tmp + 1 -> 298
- 298 -> Assign: i = i + 1 -> 300 ]} -> 304
- 304 -> Assume: i < 100 false -> 305
- 305 -> leave_loop -> 306
- 306 -> LeaveScope: i -> 312 ]} at 312
+ 213 -> join -> 217
+ 217 -> join -> 219
+ 219 -> join -> 223
+ 223 -> join -> 225
+ 225 -> Loop(4) 194 {[ 194 -> Assume: i < 100 true -> 195
+ 195 -> Assume: i % 2 true -> 197;
+ Assume: i % 2 false -> 199
+ 197 -> Assign: tmp = tmp + 1 -> 198
+ 198 -> join -> 200
+ 199 -> join -> 200
+ 200 -> Assume: i % 3 true -> 202;
+ Assume: i % 3 false -> 204
+ 202 -> Assign: tmp = tmp + 1 -> 203
+ 203 -> join -> 205
+ 204 -> join -> 205
+ 205 -> Assume: i % 5 true -> 207;
+ Assume: i % 5 false -> 209
+ 207 -> Assign: tmp = tmp + 1 -> 208
+ 208 -> join -> 210
+ 209 -> join -> 210
+ 210 -> Assume: i % 7 true -> 212;
+ Assume: i % 7 false -> 215
+ 212 -> Assign: tmp = tmp + 1 -> 214
+ 214 -> join -> 216
+ 215 -> join -> 216
+ 216 -> Assume: i % 11 true -> 218;
+ Assume: i % 11 false -> 221
+ 218 -> Assign: tmp = tmp + 1 -> 220
+ 220 -> join -> 222
+ 221 -> join -> 222
+ 222 -> Assign: tmp = tmp + 1 -> 224
+ 224 -> Assign: i = i + 1 -> 226 ]} -> 228
+ 228 -> Assume: i < 100 false -> 229
+ 229 -> leave_loop -> 230
+ 230 -> LeaveScope: i -> 231
+ 231 -> LeaveScope: i -> 232 ]} at 232
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
+ These dependencies hold at termination for the executions that terminate:
[from] Function main:
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
- tmp; i
+ tmp; i
[inout] Inputs for function main:
- \nothing
+ \nothing
diff --git a/tests/value/traces/oracle/test5.res.oracle b/tests/value/traces/oracle/test5.res.oracle
index 9c6a9068b068c513efbad3a6cee95e95b61341f4..44b41790709aaacdddb7a1205dace5c258bcf91a 100644
--- a/tests/value/traces/oracle/test5.res.oracle
+++ b/tests/value/traces/oracle/test5.res.oracle
@@ -1,98 +1,102 @@
[kernel] Parsing tests/value/traces/test5.i (no preprocessing)
-tests/value/traces/test5.i:21:[kernel] warning: Calling undeclared function my_switch. Old style K&R code?
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value:initial-state] Values of globals at initialization
+[kernel:typing:implicit-function-declaration] tests/value/traces/test5.i:21: Warning:
+ Calling undeclared function my_switch. Old style K&R code?
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-tests/value/traces/test5.i:21:[kernel] warning: Neither code nor specification for function my_switch, generating default assigns from the prototype
-[value] using specification for function my_switch
-[value] Done for function my_switch
-tests/value/traces/test5.i:21:[value] warning: signed overflow.
- assert tmp_0 + tmp ≤ 2147483647;
- (tmp_0 from my_switch(tmp))
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-tests/value/traces/test5.i:21:[value] warning: signed overflow.
- assert -2147483648 ≤ tmp_0 + tmp;
- (tmp_0 from my_switch(tmp))
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-tests/value/traces/test5.i:20:[value] entering loop for the first time
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-tests/value/traces/test5.i:19:[value] entering loop for the first time
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-[value] computing for function my_switch <- main.
- Called from tests/value/traces/test5.i:21.
-[value] Done for function my_switch
-[value] Recording results for main
-[value] done for function main
-[value] ====== VALUES COMPUTED ======
-[value:final-states] Values at end of function main:
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[kernel:annot:missing-spec] tests/value/traces/test5.i:21: Warning:
+ Neither code nor specification for function my_switch, generating default assigns from the prototype
+[eva] using specification for function my_switch
+[eva] Done for function my_switch
+[eva:alarm] tests/value/traces/test5.i:21: Warning:
+ signed overflow.
+ assert tmp_0 + tmp ≤ 2147483647;
+ (tmp_0 from my_switch(tmp))
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva:alarm] tests/value/traces/test5.i:21: Warning:
+ signed overflow.
+ assert -2147483648 ≤ tmp_0 + tmp;
+ (tmp_0 from my_switch(tmp))
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] tests/value/traces/test5.i:20: starting to merge loop iterations
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] tests/value/traces/test5.i:19: starting to merge loop iterations
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] computing for function my_switch <- main.
+ Called from tests/value/traces/test5.i:21.
+[eva] Done for function my_switch
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
tmp ∈ [--..--]
-[value:d-traces] Trace domains:
+[eva:d-traces] Trace domains:
start: 0; globals = ; main_formals = c;
{[ 0 -> initialize variable using type Main_Formal
c -> 1
@@ -117,440 +121,463 @@ c -> 1
19 -> Assign: tmp = tmp_0 + tmp -> 20
20 -> LeaveScope: tmp_0 -> 21
21 -> Assign: j = j + 1 -> 22
- 22 -> Assume: j < 10 true -> 24
- 24 -> EnterScope: tmp_0 -> 25
- 25 -> EnterScope: \result<my_switch> -> 26
- 26 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 27
- 27 -> Assign: tmp_0 = \result<my_switch> -> 29
- 29 -> LeaveScope: \result<my_switch> -> 30
- 30 -> Assign: tmp = tmp_0 + tmp -> 31
- 31 -> LeaveScope: tmp_0 -> 33
- 33 -> Assign: j = j + 1 -> 34
- 34 -> Assume: j < 10 true -> 37
- 37 -> EnterScope: tmp_0 -> 38
- 38 -> EnterScope: \result<my_switch> -> 39
- 39 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 40
- 40 -> Assign: tmp_0 = \result<my_switch> -> 42
- 42 -> LeaveScope: \result<my_switch> -> 43
- 43 -> Assign: tmp = tmp_0 + tmp -> 44
- 44 -> LeaveScope: tmp_0 -> 46
- 46 -> Assign: j = j + 1 -> 47
- 47 -> Assume: j < 10 true -> 50
- 50 -> EnterScope: tmp_0 -> 51
- 51 -> EnterScope: \result<my_switch> -> 52
- 52 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 53
- 53 -> Assign: tmp_0 = \result<my_switch> -> 55
- 55 -> LeaveScope: \result<my_switch> -> 56
- 56 -> Assign: tmp = tmp_0 + tmp -> 57
- 57 -> LeaveScope: tmp_0 -> 59
- 59 -> Assign: j = j + 1 -> 60
- 60 -> Assume: j < 10 true -> 63
+ 22 -> Assume: j < 10 true -> 23
+ 23 -> EnterScope: tmp_0 -> 24
+ 24 -> EnterScope: \result<my_switch> -> 25
+ 25 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 26
+ 26 -> Assign: tmp_0 = \result<my_switch> -> 28
+ 28 -> LeaveScope: \result<my_switch> -> 29
+ 29 -> Assign: tmp = tmp_0 + tmp -> 30
+ 30 -> LeaveScope: tmp_0 -> 31
+ 31 -> Assign: j = j + 1 -> 32
+ 32 -> Assume: j < 10 true -> 33
+ 33 -> EnterScope: tmp_0 -> 34
+ 34 -> EnterScope: \result<my_switch> -> 35
+ 35 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 36
+ 36 -> Assign: tmp_0 = \result<my_switch> -> 38
+ 38 -> LeaveScope: \result<my_switch> -> 39
+ 39 -> Assign: tmp = tmp_0 + tmp -> 40
+ 40 -> LeaveScope: tmp_0 -> 41
+ 41 -> Assign: j = j + 1 -> 42
+ 42 -> Assume: j < 10 true -> 43
+ 43 -> EnterScope: tmp_0 -> 44
+ 44 -> EnterScope: \result<my_switch> -> 45
+ 45 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 46
+ 46 -> Assign: tmp_0 = \result<my_switch> -> 48
+ 48 -> LeaveScope: \result<my_switch> -> 49
+ 49 -> Assign: tmp = tmp_0 + tmp -> 50
+ 50 -> LeaveScope: tmp_0 -> 51
+ 51 -> Assign: j = j + 1 -> 52
+ 52 -> Assume: j < 10 true -> 53
+ 53 -> EnterScope: tmp_0 -> 54
+ 54 -> EnterScope: \result<my_switch> -> 55
+ 55 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 56
+ 56 -> Assign: tmp_0 = \result<my_switch> -> 58
+ 58 -> LeaveScope: \result<my_switch> -> 59
+ 59 -> Assign: tmp = tmp_0 + tmp -> 60
+ 60 -> LeaveScope: tmp_0 -> 61
+ 61 -> Assign: j = j + 1 -> 62
+ 62 -> Assume: j < 10 true -> 63
63 -> EnterScope: tmp_0 -> 64
64 -> EnterScope: \result<my_switch> -> 65
65 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 66
66 -> Assign: tmp_0 = \result<my_switch> -> 68
68 -> LeaveScope: \result<my_switch> -> 69
69 -> Assign: tmp = tmp_0 + tmp -> 70
- 70 -> LeaveScope: tmp_0 -> 72
- 72 -> Assign: j = j + 1 -> 73
- 73 -> Assume: j < 10 true -> 76
- 76 -> EnterScope: tmp_0 -> 77
- 77 -> EnterScope: \result<my_switch> -> 78
- 78 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 79
- 79 -> Assign: tmp_0 = \result<my_switch> -> 81
- 81 -> LeaveScope: \result<my_switch> -> 82
- 82 -> Assign: tmp = tmp_0 + tmp -> 83
- 83 -> LeaveScope: tmp_0 -> 85
- 85 -> Assign: j = j + 1 -> 86
- 86 -> Assume: j < 10 true -> 89
- 89 -> EnterScope: tmp_0 -> 90
- 90 -> EnterScope: \result<my_switch> -> 91
- 91 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 92
- 92 -> Assign: tmp_0 = \result<my_switch> -> 94
- 94 -> LeaveScope: \result<my_switch> -> 95
- 95 -> Assign: tmp = tmp_0 + tmp -> 96
- 96 -> LeaveScope: tmp_0 -> 98
- 98 -> Assign: j = j + 1 -> 99
- 99 -> Assume: j < 10 true -> 102
- 102 -> EnterScope: tmp_0 -> 103
- 103 -> EnterScope: \result<my_switch> -> 104
- 104 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 105
- 105 -> Assign: tmp_0 = \result<my_switch> -> 107
- 107 -> LeaveScope: \result<my_switch> -> 108
- 108 -> Assign: tmp = tmp_0 + tmp -> 109
- 109 -> LeaveScope: tmp_0 -> 111
+ 70 -> LeaveScope: tmp_0 -> 71
+ 71 -> Assign: j = j + 1 -> 72
+ 72 -> Assume: j < 10 true -> 73
+ 73 -> EnterScope: tmp_0 -> 74
+ 74 -> EnterScope: \result<my_switch> -> 75
+ 75 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 76
+ 76 -> Assign: tmp_0 = \result<my_switch> -> 78
+ 78 -> LeaveScope: \result<my_switch> -> 79
+ 79 -> Assign: tmp = tmp_0 + tmp -> 80
+ 80 -> LeaveScope: tmp_0 -> 81
+ 81 -> Assign: j = j + 1 -> 82
+ 82 -> Assume: j < 10 true -> 83
+ 83 -> EnterScope: tmp_0 -> 84
+ 84 -> EnterScope: \result<my_switch> -> 85
+ 85 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 86
+ 86 -> Assign: tmp_0 = \result<my_switch> -> 88
+ 88 -> LeaveScope: \result<my_switch> -> 89
+ 89 -> Assign: tmp = tmp_0 + tmp -> 90
+ 90 -> LeaveScope: tmp_0 -> 91
+ 91 -> Assign: j = j + 1 -> 92
+ 92 -> Assume: j < 10 true -> 93
+ 93 -> EnterScope: tmp_0 -> 94
+ 94 -> EnterScope: \result<my_switch> -> 95
+ 95 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 96
+ 96 -> Assign: tmp_0 = \result<my_switch> -> 98
+ 98 -> LeaveScope: \result<my_switch> -> 99
+ 99 -> Assign: tmp = tmp_0 + tmp -> 100
+ 100 -> LeaveScope: tmp_0 -> 101
+ 101 -> Assign: j = j + 1 -> 102
+ 102 -> Assume: j < 10 true -> 103
+ 103 -> EnterScope: tmp_0 -> 104
+ 104 -> EnterScope: \result<my_switch> -> 105
+ 105 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 106
+ 106 -> Assign: tmp_0 = \result<my_switch> -> 108
+ 108 -> LeaveScope: \result<my_switch> -> 109
+ 109 -> Assign: tmp = tmp_0 + tmp -> 110
+ 110 -> LeaveScope: tmp_0 -> 111
111 -> Assign: j = j + 1 -> 112
- 112 -> Assume: j < 10 true -> 115
- 115 -> EnterScope: tmp_0 -> 116
- 116 -> EnterScope: \result<my_switch> -> 117
- 117 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 118
- 118 -> Assign: tmp_0 = \result<my_switch> -> 120
- 120 -> LeaveScope: \result<my_switch> -> 121
- 121 -> Assign: tmp = tmp_0 + tmp -> 122
- 122 -> LeaveScope: tmp_0 -> 124
- 124 -> Assign: j = j + 1 -> 125
- 125 -> Assume: j < 10 true -> 128
- 128 -> EnterScope: tmp_0 -> 129
- 129 -> EnterScope: \result<my_switch> -> 130
- 130 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 131
- 131 -> Assign: tmp_0 = \result<my_switch> -> 133
- 133 -> LeaveScope: \result<my_switch> -> 134
- 134 -> Assign: tmp = tmp_0 + tmp -> 135
- 135 -> LeaveScope: tmp_0 -> 137
- 137 -> Assign: j = j + 1 -> 138
- 138 -> Assume: j < 10 false -> 141; join -> 151
- 141 -> LeaveScope: j -> 142
- 142 -> Assign: i = i + 1 -> 143
- 143 -> Assume: i < 10 true -> 145
- 145 -> EnterScope: j -> 146
- 146 -> initialize variable: j -> 147
- 147 -> Assign: j = 0 -> 148
- 148 -> enter_loop -> 150
- 150 -> join -> 151
- 151 -> Assume: j < 10 false -> 153; Assume: j < 10 true -> 154;
- join -> 166
- 153 -> LeaveScope: j -> 213
- 154 -> EnterScope: tmp_0 -> 155; join -> 170
- 155 -> EnterScope: \result<my_switch> -> 156; join -> 172
- 156 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 157
- 157 -> Assign: tmp_0 = \result<my_switch> -> 159
- 159 -> LeaveScope: \result<my_switch> -> 160
- 160 -> Assign: tmp = tmp_0 + tmp -> 161; join -> 178
- 161 -> LeaveScope: tmp_0 -> 163
- 163 -> Assign: j = j + 1 -> 164; join -> 182
- 164 -> join -> 166
- 166 -> Assume: j < 10 false -> 168; Assume: j < 10 true -> 169;
- join -> 185
- 168 -> LeaveScope: j -> 214
- 169 -> join -> 170
- 170 -> EnterScope: tmp_0 -> 171; join -> 192
- 171 -> join -> 172
- 172 -> EnterScope: \result<my_switch> -> 173; join -> 194
- 173 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 174
- 174 -> Assign: tmp_0 = \result<my_switch> -> 176
- 176 -> LeaveScope: \result<my_switch> -> 177
- 177 -> join -> 178
- 178 -> Assign: tmp = tmp_0 + tmp -> 179; join -> 200
- 179 -> LeaveScope: tmp_0 -> 181
- 181 -> join -> 182
- 182 -> Assign: j = j + 1 -> 183; join -> 204
- 183 -> join -> 185
- 185 -> Assume: j < 10 false -> 190; join -> 192
- 190 -> leave_loop -> 191
- 191 -> LeaveScope: j -> 215
- 192 -> join -> 194
- 194 -> join -> 200
- 200 -> join -> 204
- 204 -> join -> 256;
- Loop(16) 186 {[ 186 -> Assume: j < 10 true -> 189
- 189 -> EnterScope: tmp_0 -> 193
- 193 -> EnterScope: \result<my_switch> -> 195
- 195 -> CallDeclared:
+ 112 -> Assume: j < 10 false -> 113; join -> 122
+ 113 -> LeaveScope: j -> 114
+ 114 -> LeaveScope: j -> 115
+ 115 -> Assign: i = i + 1 -> 116
+ 116 -> Assume: i < 10 true -> 117
+ 117 -> EnterScope: j -> 118
+ 118 -> initialize variable: j -> 119
+ 119 -> Assign: j = 0 -> 120
+ 120 -> enter_loop -> 121
+ 121 -> join -> 122
+ 122 -> Assume: j < 10 true -> 123; Assume: j < 10 false -> 167;
+ join -> 133
+ 123 -> EnterScope: tmp_0 -> 124; join -> 135
+ 124 -> EnterScope: \result<my_switch> -> 125; join -> 137
+ 125 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 126
+ 126 -> Assign: tmp_0 = \result<my_switch> -> 128
+ 128 -> LeaveScope: \result<my_switch> -> 129
+ 129 -> Assign: tmp = tmp_0 + tmp -> 130; join -> 143
+ 130 -> LeaveScope: tmp_0 -> 131
+ 131 -> Assign: j = j + 1 -> 132; join -> 146
+ 132 -> join -> 133
+ 133 -> Assume: j < 10 true -> 134; Assume: j < 10 false -> 166;
+ join -> 148
+ 134 -> join -> 135
+ 135 -> EnterScope: tmp_0 -> 136; join -> 151
+ 136 -> join -> 137
+ 137 -> EnterScope: \result<my_switch> -> 138; join -> 153
+ 138 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 139
+ 139 -> Assign: tmp_0 = \result<my_switch> -> 141
+ 141 -> LeaveScope: \result<my_switch> -> 142
+ 142 -> join -> 143
+ 143 -> Assign: tmp = tmp_0 + tmp -> 144; join -> 159
+ 144 -> LeaveScope: tmp_0 -> 145
+ 145 -> join -> 146
+ 146 -> Assign: j = j + 1 -> 147; join -> 162
+ 147 -> join -> 148
+ 148 -> Assume: j < 10 false -> 168; join -> 151
+ 151 -> join -> 153
+ 153 -> join -> 159
+ 159 -> join -> 162
+ 162 -> join -> 208;
+ Loop(16) 149 {[ 149 -> Assume: j < 10 true -> 150
+ 150 -> EnterScope: tmp_0 -> 152
+ 152 -> EnterScope: \result<my_switch> -> 154
+ 154 -> CallDeclared:
\result<my_switch> =
- my_switch(tmp) -> 196
- 196 -> Assign: tmp_0 = \result<my_switch> -> 198
- 198 -> LeaveScope: \result<my_switch> -> 199
- 199 -> Assign: tmp = tmp_0 + tmp -> 201
- 201 -> LeaveScope: tmp_0 -> 203
- 203 -> Assign: j = j + 1 -> 205 ]} -> 208
- 208 -> Assume: j < 10 false -> 209
- 209 -> leave_loop -> 210
- 210 -> LeaveScope: j -> 216
- 213 -> Assign: i = i + 1 -> 217
- 214 -> Assign: i = i + 1 -> 218
- 215 -> Assign: i = i + 1 -> 219
- 216 -> Assign: i = i + 1 -> 220
- 217 -> Assume: i < 10 true -> 232
- 218 -> Assume: i < 10 true -> 231
- 219 -> Assume: i < 10 true -> 230
- 220 -> Assume: i < 10 true -> 229
- 229 -> EnterScope: j -> 242
- 230 -> EnterScope: j -> 239
- 231 -> EnterScope: j -> 236
- 232 -> EnterScope: j -> 233
- 233 -> initialize variable: j -> 234
- 234 -> Assign: j = 0 -> 235
- 235 -> enter_loop -> 252
- 236 -> initialize variable: j -> 237
- 237 -> Assign: j = 0 -> 238
- 238 -> enter_loop -> 251
- 239 -> initialize variable: j -> 240
- 240 -> Assign: j = 0 -> 241
- 241 -> enter_loop -> 250
- 242 -> initialize variable: j -> 243
- 243 -> Assign: j = 0 -> 244
- 244 -> enter_loop -> 249
- 249 -> join -> 253
- 250 -> join -> 253
- 251 -> join -> 254
- 252 -> join -> 255
- 253 -> join -> 254
- 254 -> join -> 255
- 255 -> join -> 256
- 256 -> join -> 275;
- Loop(16) 186 {[ 186 -> Assume: j < 10 true -> 189
- 189 -> EnterScope: tmp_0 -> 193
- 193 -> EnterScope: \result<my_switch> -> 195
- 195 -> CallDeclared:
+ my_switch(tmp) -> 155
+ 155 -> Assign: tmp_0 = \result<my_switch> -> 157
+ 157 -> LeaveScope: \result<my_switch> -> 158
+ 158 -> Assign: tmp = tmp_0 + tmp -> 160
+ 160 -> LeaveScope: tmp_0 -> 161
+ 161 -> Assign: j = j + 1 -> 163 ]} -> 170
+ 166 -> LeaveScope: j -> 175
+ 167 -> LeaveScope: j -> 176
+ 168 -> leave_loop -> 169
+ 169 -> LeaveScope: j -> 174
+ 170 -> Assume: j < 10 false -> 171
+ 171 -> leave_loop -> 172
+ 172 -> LeaveScope: j -> 173
+ 173 -> LeaveScope: j -> 177
+ 174 -> LeaveScope: j -> 178
+ 175 -> LeaveScope: j -> 179
+ 176 -> LeaveScope: j -> 180
+ 177 -> Assign: i = i + 1 -> 184
+ 178 -> Assign: i = i + 1 -> 183
+ 179 -> Assign: i = i + 1 -> 182
+ 180 -> Assign: i = i + 1 -> 181
+ 181 -> Assume: i < 10 true -> 188
+ 182 -> Assume: i < 10 true -> 187
+ 183 -> Assume: i < 10 true -> 186
+ 184 -> Assume: i < 10 true -> 185
+ 185 -> EnterScope: j -> 198
+ 186 -> EnterScope: j -> 195
+ 187 -> EnterScope: j -> 192
+ 188 -> EnterScope: j -> 189
+ 189 -> initialize variable: j -> 190
+ 190 -> Assign: j = 0 -> 191
+ 191 -> enter_loop -> 204
+ 192 -> initialize variable: j -> 193
+ 193 -> Assign: j = 0 -> 194
+ 194 -> enter_loop -> 203
+ 195 -> initialize variable: j -> 196
+ 196 -> Assign: j = 0 -> 197
+ 197 -> enter_loop -> 202
+ 198 -> initialize variable: j -> 199
+ 199 -> Assign: j = 0 -> 200
+ 200 -> enter_loop -> 201
+ 201 -> join -> 207
+ 202 -> join -> 206
+ 203 -> join -> 205
+ 204 -> join -> 205
+ 205 -> join -> 206
+ 206 -> join -> 207
+ 207 -> join -> 208
+ 208 -> join -> 221;
+ Loop(16) 149 {[ 149 -> Assume: j < 10 true -> 150
+ 150 -> EnterScope: tmp_0 -> 152
+ 152 -> EnterScope: \result<my_switch> -> 154
+ 154 -> CallDeclared:
\result<my_switch> =
- my_switch(tmp) -> 196
- 196 -> Assign: tmp_0 = \result<my_switch> -> 198
- 198 -> LeaveScope: \result<my_switch> -> 199
- 199 -> Assign: tmp = tmp_0 + tmp -> 201
- 201 -> LeaveScope: tmp_0 -> 203
- 203 -> Assign: j = j + 1 -> 205 ]} -> 258
- 258 -> Assume: j < 10 false -> 259
- 259 -> leave_loop -> 260
- 260 -> LeaveScope: j -> 264
- 264 -> Assign: i = i + 1 -> 265
- 265 -> Assume: i < 10 false -> 268; Assume: i < 10 true -> 269
- 268 -> LeaveScope: i -> 443
- 269 -> EnterScope: j -> 270
- 270 -> initialize variable: j -> 271
- 271 -> Assign: j = 0 -> 272
- 272 -> enter_loop -> 274
- 274 -> join -> 275
- 275 -> join -> 294;
- Loop(16) 186 {[ 186 -> Assume: j < 10 true -> 189
- 189 -> EnterScope: tmp_0 -> 193
- 193 -> EnterScope: \result<my_switch> -> 195
- 195 -> CallDeclared:
+ my_switch(tmp) -> 155
+ 155 -> Assign: tmp_0 = \result<my_switch> -> 157
+ 157 -> LeaveScope: \result<my_switch> -> 158
+ 158 -> Assign: tmp = tmp_0 + tmp -> 160
+ 160 -> LeaveScope: tmp_0 -> 161
+ 161 -> Assign: j = j + 1 -> 163 ]} -> 210
+ 210 -> Assume: j < 10 false -> 211
+ 211 -> leave_loop -> 212
+ 212 -> LeaveScope: j -> 213
+ 213 -> LeaveScope: j -> 214
+ 214 -> Assign: i = i + 1 -> 215
+ 215 -> Assume: i < 10 true -> 216; Assume: i < 10 false -> 341
+ 216 -> EnterScope: j -> 217
+ 217 -> initialize variable: j -> 218
+ 218 -> Assign: j = 0 -> 219
+ 219 -> enter_loop -> 220
+ 220 -> join -> 221
+ 221 -> join -> 234;
+ Loop(16) 149 {[ 149 -> Assume: j < 10 true -> 150
+ 150 -> EnterScope: tmp_0 -> 152
+ 152 -> EnterScope: \result<my_switch> -> 154
+ 154 -> CallDeclared:
\result<my_switch> =
- my_switch(tmp) -> 196
- 196 -> Assign: tmp_0 = \result<my_switch> -> 198
- 198 -> LeaveScope: \result<my_switch> -> 199
- 199 -> Assign: tmp = tmp_0 + tmp -> 201
- 201 -> LeaveScope: tmp_0 -> 203
- 203 -> Assign: j = j + 1 -> 205 ]} -> 277
- 277 -> Assume: j < 10 false -> 278
- 278 -> leave_loop -> 279
- 279 -> LeaveScope: j -> 283
- 283 -> Assign: i = i + 1 -> 284
- 284 -> Assume: i < 10 false -> 287; Assume: i < 10 true -> 288
- 287 -> LeaveScope: i -> 444
- 288 -> EnterScope: j -> 289
- 289 -> initialize variable: j -> 290
- 290 -> Assign: j = 0 -> 291
- 291 -> enter_loop -> 293
- 293 -> join -> 294
- 294 -> join -> 313;
- Loop(16) 186 {[ 186 -> Assume: j < 10 true -> 189
- 189 -> EnterScope: tmp_0 -> 193
- 193 -> EnterScope: \result<my_switch> -> 195
- 195 -> CallDeclared:
+ my_switch(tmp) -> 155
+ 155 -> Assign: tmp_0 = \result<my_switch> -> 157
+ 157 -> LeaveScope: \result<my_switch> -> 158
+ 158 -> Assign: tmp = tmp_0 + tmp -> 160
+ 160 -> LeaveScope: tmp_0 -> 161
+ 161 -> Assign: j = j + 1 -> 163 ]} -> 223
+ 223 -> Assume: j < 10 false -> 224
+ 224 -> leave_loop -> 225
+ 225 -> LeaveScope: j -> 226
+ 226 -> LeaveScope: j -> 227
+ 227 -> Assign: i = i + 1 -> 228
+ 228 -> Assume: i < 10 true -> 229; Assume: i < 10 false -> 340
+ 229 -> EnterScope: j -> 230
+ 230 -> initialize variable: j -> 231
+ 231 -> Assign: j = 0 -> 232
+ 232 -> enter_loop -> 233
+ 233 -> join -> 234
+ 234 -> join -> 247;
+ Loop(16) 149 {[ 149 -> Assume: j < 10 true -> 150
+ 150 -> EnterScope: tmp_0 -> 152
+ 152 -> EnterScope: \result<my_switch> -> 154
+ 154 -> CallDeclared:
\result<my_switch> =
- my_switch(tmp) -> 196
- 196 -> Assign: tmp_0 = \result<my_switch> -> 198
- 198 -> LeaveScope: \result<my_switch> -> 199
- 199 -> Assign: tmp = tmp_0 + tmp -> 201
- 201 -> LeaveScope: tmp_0 -> 203
- 203 -> Assign: j = j + 1 -> 205 ]} -> 296
- 296 -> Assume: j < 10 false -> 297
- 297 -> leave_loop -> 298
- 298 -> LeaveScope: j -> 302
- 302 -> Assign: i = i + 1 -> 303
- 303 -> Assume: i < 10 false -> 306; Assume: i < 10 true -> 307
- 306 -> LeaveScope: i -> 445
- 307 -> EnterScope: j -> 308
- 308 -> initialize variable: j -> 309
- 309 -> Assign: j = 0 -> 310
- 310 -> enter_loop -> 312
- 312 -> join -> 313
- 313 -> join -> 332;
- Loop(16) 186 {[ 186 -> Assume: j < 10 true -> 189
- 189 -> EnterScope: tmp_0 -> 193
- 193 -> EnterScope: \result<my_switch> -> 195
- 195 -> CallDeclared:
+ my_switch(tmp) -> 155
+ 155 -> Assign: tmp_0 = \result<my_switch> -> 157
+ 157 -> LeaveScope: \result<my_switch> -> 158
+ 158 -> Assign: tmp = tmp_0 + tmp -> 160
+ 160 -> LeaveScope: tmp_0 -> 161
+ 161 -> Assign: j = j + 1 -> 163 ]} -> 236
+ 236 -> Assume: j < 10 false -> 237
+ 237 -> leave_loop -> 238
+ 238 -> LeaveScope: j -> 239
+ 239 -> LeaveScope: j -> 240
+ 240 -> Assign: i = i + 1 -> 241
+ 241 -> Assume: i < 10 true -> 242; Assume: i < 10 false -> 339
+ 242 -> EnterScope: j -> 243
+ 243 -> initialize variable: j -> 244
+ 244 -> Assign: j = 0 -> 245
+ 245 -> enter_loop -> 246
+ 246 -> join -> 247
+ 247 -> join -> 260;
+ Loop(16) 149 {[ 149 -> Assume: j < 10 true -> 150
+ 150 -> EnterScope: tmp_0 -> 152
+ 152 -> EnterScope: \result<my_switch> -> 154
+ 154 -> CallDeclared:
\result<my_switch> =
- my_switch(tmp) -> 196
- 196 -> Assign: tmp_0 = \result<my_switch> -> 198
- 198 -> LeaveScope: \result<my_switch> -> 199
- 199 -> Assign: tmp = tmp_0 + tmp -> 201
- 201 -> LeaveScope: tmp_0 -> 203
- 203 -> Assign: j = j + 1 -> 205 ]} -> 315
- 315 -> Assume: j < 10 false -> 316
- 316 -> leave_loop -> 317
- 317 -> LeaveScope: j -> 321
- 321 -> Assign: i = i + 1 -> 322
- 322 -> Assume: i < 10 false -> 325; Assume: i < 10 true -> 326
- 325 -> LeaveScope: i -> 446
- 326 -> EnterScope: j -> 327
- 327 -> initialize variable: j -> 328
- 328 -> Assign: j = 0 -> 329
- 329 -> enter_loop -> 331
- 331 -> join -> 332
- 332 -> join -> 351;
- Loop(16) 186 {[ 186 -> Assume: j < 10 true -> 189
- 189 -> EnterScope: tmp_0 -> 193
- 193 -> EnterScope: \result<my_switch> -> 195
- 195 -> CallDeclared:
+ my_switch(tmp) -> 155
+ 155 -> Assign: tmp_0 = \result<my_switch> -> 157
+ 157 -> LeaveScope: \result<my_switch> -> 158
+ 158 -> Assign: tmp = tmp_0 + tmp -> 160
+ 160 -> LeaveScope: tmp_0 -> 161
+ 161 -> Assign: j = j + 1 -> 163 ]} -> 249
+ 249 -> Assume: j < 10 false -> 250
+ 250 -> leave_loop -> 251
+ 251 -> LeaveScope: j -> 252
+ 252 -> LeaveScope: j -> 253
+ 253 -> Assign: i = i + 1 -> 254
+ 254 -> Assume: i < 10 true -> 255; Assume: i < 10 false -> 338
+ 255 -> EnterScope: j -> 256
+ 256 -> initialize variable: j -> 257
+ 257 -> Assign: j = 0 -> 258
+ 258 -> enter_loop -> 259
+ 259 -> join -> 260
+ 260 -> join -> 273;
+ Loop(16) 149 {[ 149 -> Assume: j < 10 true -> 150
+ 150 -> EnterScope: tmp_0 -> 152
+ 152 -> EnterScope: \result<my_switch> -> 154
+ 154 -> CallDeclared:
\result<my_switch> =
- my_switch(tmp) -> 196
- 196 -> Assign: tmp_0 = \result<my_switch> -> 198
- 198 -> LeaveScope: \result<my_switch> -> 199
- 199 -> Assign: tmp = tmp_0 + tmp -> 201
- 201 -> LeaveScope: tmp_0 -> 203
- 203 -> Assign: j = j + 1 -> 205 ]} -> 334
- 334 -> Assume: j < 10 false -> 335
- 335 -> leave_loop -> 336
- 336 -> LeaveScope: j -> 340
- 340 -> Assign: i = i + 1 -> 341
- 341 -> Assume: i < 10 false -> 344; Assume: i < 10 true -> 345;
- join -> 362
- 344 -> LeaveScope: i -> 447
- 345 -> EnterScope: j -> 346; join -> 366
- 346 -> initialize variable: j -> 347
- 347 -> Assign: j = 0 -> 348
- 348 -> enter_loop -> 350
- 350 -> join -> 351
- 351 -> join -> 372;
- Loop(16) 186 {[ 186 -> Assume: j < 10 true -> 189
- 189 -> EnterScope: tmp_0 -> 193
- 193 -> EnterScope: \result<my_switch> -> 195
- 195 -> CallDeclared:
+ my_switch(tmp) -> 155
+ 155 -> Assign: tmp_0 = \result<my_switch> -> 157
+ 157 -> LeaveScope: \result<my_switch> -> 158
+ 158 -> Assign: tmp = tmp_0 + tmp -> 160
+ 160 -> LeaveScope: tmp_0 -> 161
+ 161 -> Assign: j = j + 1 -> 163 ]} -> 262
+ 262 -> Assume: j < 10 false -> 263
+ 263 -> leave_loop -> 264
+ 264 -> LeaveScope: j -> 265
+ 265 -> LeaveScope: j -> 266
+ 266 -> Assign: i = i + 1 -> 267
+ 267 -> Assume: i < 10 true -> 268; Assume: i < 10 false -> 337;
+ join -> 281
+ 268 -> EnterScope: j -> 269; join -> 283
+ 269 -> initialize variable: j -> 270
+ 270 -> Assign: j = 0 -> 271
+ 271 -> enter_loop -> 272
+ 272 -> join -> 273
+ 273 -> join -> 288;
+ Loop(16) 149 {[ 149 -> Assume: j < 10 true -> 150
+ 150 -> EnterScope: tmp_0 -> 152
+ 152 -> EnterScope: \result<my_switch> -> 154
+ 154 -> CallDeclared:
\result<my_switch> =
- my_switch(tmp) -> 196
- 196 -> Assign: tmp_0 = \result<my_switch> -> 198
- 198 -> LeaveScope: \result<my_switch> -> 199
- 199 -> Assign: tmp = tmp_0 + tmp -> 201
- 201 -> LeaveScope: tmp_0 -> 203
- 203 -> Assign: j = j + 1 -> 205 ]} -> 353
- 353 -> Assume: j < 10 false -> 354
- 354 -> leave_loop -> 355
- 355 -> LeaveScope: j -> 359; join -> 380
- 359 -> Assign: i = i + 1 -> 360; join -> 382
- 360 -> join -> 362
- 362 -> Assume: i < 10 false -> 364; Assume: i < 10 true -> 365;
- join -> 385
- 364 -> LeaveScope: i -> 448
- 365 -> join -> 366
- 366 -> EnterScope: j -> 367; join -> 389
- 367 -> initialize variable: j -> 368
- 368 -> Assign: j = 0 -> 369
- 369 -> enter_loop -> 371
- 371 -> join -> 372
- 372 -> join -> 395;
- Loop(16) 186 {[ 186 -> Assume: j < 10 true -> 189
- 189 -> EnterScope: tmp_0 -> 193
- 193 -> EnterScope: \result<my_switch> -> 195
- 195 -> CallDeclared:
+ my_switch(tmp) -> 155
+ 155 -> Assign: tmp_0 = \result<my_switch> -> 157
+ 157 -> LeaveScope: \result<my_switch> -> 158
+ 158 -> Assign: tmp = tmp_0 + tmp -> 160
+ 160 -> LeaveScope: tmp_0 -> 161
+ 161 -> Assign: j = j + 1 -> 163 ]} -> 275
+ 275 -> Assume: j < 10 false -> 276
+ 276 -> leave_loop -> 277
+ 277 -> LeaveScope: j -> 278; join -> 293
+ 278 -> LeaveScope: j -> 279
+ 279 -> Assign: i = i + 1 -> 280; join -> 296
+ 280 -> join -> 281
+ 281 -> Assume: i < 10 true -> 282; Assume: i < 10 false -> 336;
+ join -> 298
+ 282 -> join -> 283
+ 283 -> EnterScope: j -> 284; join -> 300
+ 284 -> initialize variable: j -> 285
+ 285 -> Assign: j = 0 -> 286
+ 286 -> enter_loop -> 287
+ 287 -> join -> 288
+ 288 -> join -> 305;
+ Loop(16) 149 {[ 149 -> Assume: j < 10 true -> 150
+ 150 -> EnterScope: tmp_0 -> 152
+ 152 -> EnterScope: \result<my_switch> -> 154
+ 154 -> CallDeclared:
\result<my_switch> =
- my_switch(tmp) -> 196
- 196 -> Assign: tmp_0 = \result<my_switch> -> 198
- 198 -> LeaveScope: \result<my_switch> -> 199
- 199 -> Assign: tmp = tmp_0 + tmp -> 201
- 201 -> LeaveScope: tmp_0 -> 203
- 203 -> Assign: j = j + 1 -> 205 ]} -> 374
- 374 -> Assume: j < 10 false -> 375
- 375 -> leave_loop -> 376
- 376 -> join -> 380
- 380 -> LeaveScope: j -> 381; join -> 403
- 381 -> join -> 382
- 382 -> Assign: i = i + 1 -> 383; join -> 405
- 383 -> join -> 385
- 385 -> Assume: i < 10 false -> 387; Assume: i < 10 true -> 388;
- join -> 408
- 387 -> LeaveScope: i -> 449
- 388 -> join -> 389
- 389 -> EnterScope: j -> 390; join -> 415
- 390 -> initialize variable: j -> 391
- 391 -> Assign: j = 0 -> 392
- 392 -> enter_loop -> 394
- 394 -> join -> 395
- 395 -> join -> 421;
- Loop(16) 186 {[ 186 -> Assume: j < 10 true -> 189
- 189 -> EnterScope: tmp_0 -> 193
- 193 -> EnterScope: \result<my_switch> -> 195
- 195 -> CallDeclared:
+ my_switch(tmp) -> 155
+ 155 -> Assign: tmp_0 = \result<my_switch> -> 157
+ 157 -> LeaveScope: \result<my_switch> -> 158
+ 158 -> Assign: tmp = tmp_0 + tmp -> 160
+ 160 -> LeaveScope: tmp_0 -> 161
+ 161 -> Assign: j = j + 1 -> 163 ]} -> 290
+ 290 -> Assume: j < 10 false -> 291
+ 291 -> leave_loop -> 292
+ 292 -> join -> 293
+ 293 -> LeaveScope: j -> 294; join -> 310
+ 294 -> LeaveScope: j -> 295
+ 295 -> join -> 296
+ 296 -> Assign: i = i + 1 -> 297; join -> 313
+ 297 -> join -> 298
+ 298 -> Assume: i < 10 true -> 299; Assume: i < 10 false -> 335;
+ join -> 315
+ 299 -> join -> 300
+ 300 -> EnterScope: j -> 301; join -> 318
+ 301 -> initialize variable: j -> 302
+ 302 -> Assign: j = 0 -> 303
+ 303 -> enter_loop -> 304
+ 304 -> join -> 305
+ 305 -> join -> 323;
+ Loop(16) 149 {[ 149 -> Assume: j < 10 true -> 150
+ 150 -> EnterScope: tmp_0 -> 152
+ 152 -> EnterScope: \result<my_switch> -> 154
+ 154 -> CallDeclared:
\result<my_switch> =
- my_switch(tmp) -> 196
- 196 -> Assign: tmp_0 = \result<my_switch> -> 198
- 198 -> LeaveScope: \result<my_switch> -> 199
- 199 -> Assign: tmp = tmp_0 + tmp -> 201
- 201 -> LeaveScope: tmp_0 -> 203
- 203 -> Assign: j = j + 1 -> 205 ]} -> 397
- 397 -> Assume: j < 10 false -> 398
- 398 -> leave_loop -> 399
- 399 -> join -> 403
- 403 -> LeaveScope: j -> 404; join -> 429
- 404 -> join -> 405
- 405 -> Assign: i = i + 1 -> 406; join -> 431
- 406 -> join -> 408
- 408 -> Assume: i < 10 false -> 413; join -> 415
- 413 -> leave_loop -> 414
- 414 -> LeaveScope: i -> 450
- 415 -> join -> 421
- 421 -> join -> 429
- 429 -> join -> 431
- 431 -> Loop(10) 409 {[ 409 -> Assume: i < 10 true -> 412
- 412 -> EnterScope: j -> 416
- 416 -> initialize variable: j -> 417
- 417 -> Assign: j = 0 -> 418
- 418 -> enter_loop -> 420
- 420 -> Loop(16) 186 {[ 186 -> Assume:
+ my_switch(tmp) -> 155
+ 155 -> Assign: tmp_0 = \result<my_switch> -> 157
+ 157 -> LeaveScope: \result<my_switch> -> 158
+ 158 -> Assign: tmp = tmp_0 + tmp -> 160
+ 160 -> LeaveScope: tmp_0 -> 161
+ 161 -> Assign: j = j + 1 -> 163 ]} -> 307
+ 307 -> Assume: j < 10 false -> 308
+ 308 -> leave_loop -> 309
+ 309 -> join -> 310
+ 310 -> LeaveScope: j -> 311; join -> 328
+ 311 -> LeaveScope: j -> 312
+ 312 -> join -> 313
+ 313 -> Assign: i = i + 1 -> 314; join -> 331
+ 314 -> join -> 315
+ 315 -> Assume: i < 10 false -> 342; join -> 318
+ 318 -> join -> 323
+ 323 -> join -> 328
+ 328 -> join -> 331
+ 331 -> Loop(10) 316 {[ 316 -> Assume: i < 10 true -> 317
+ 317 -> EnterScope: j -> 319
+ 319 -> initialize variable: j -> 320
+ 320 -> Assign: j = 0 -> 321
+ 321 -> enter_loop -> 322
+ 322 -> Loop(16) 149 {[ 149 -> Assume:
j < 10 true
- -> 189
- 189 -> EnterScope:
- tmp_0 -> 193
- 193 -> EnterScope:
+ -> 150
+ 150 -> EnterScope:
+ tmp_0 -> 152
+ 152 -> EnterScope:
\result<my_switch>
- -> 195
- 195 -> CallDeclared:
+ -> 154
+ 154 -> CallDeclared:
\result<my_switch> =
my_switch(
- tmp) -> 196
- 196 -> Assign:
+ tmp) -> 155
+ 155 -> Assign:
tmp_0 = \result<my_switch>
- -> 198
- 198 -> LeaveScope:
+ -> 157
+ 157 -> LeaveScope:
\result<my_switch>
- -> 199
- 199 -> Assign:
+ -> 158
+ 158 -> Assign:
tmp = tmp_0 + tmp
- -> 201
- 201 -> LeaveScope:
- tmp_0 -> 203
- 203 -> Assign:
+ -> 160
+ 160 -> LeaveScope:
+ tmp_0 -> 161
+ 161 -> Assign:
j = j + 1
- -> 205 ]}
- -> 423
- 423 -> Assume: j < 10 false -> 424
- 424 -> leave_loop -> 425
- 425 -> LeaveScope: j -> 430
- 430 -> Assign: i = i + 1 -> 432 ]} -> 435
- 435 -> Assume: i < 10 false -> 436
- 436 -> leave_loop -> 437
- 437 -> LeaveScope: i -> 451
- 443 -> join -> 459
- 444 -> join -> 458
- 445 -> join -> 457
- 446 -> join -> 456
- 447 -> join -> 455
- 448 -> join -> 454
- 449 -> join -> 453
- 450 -> join -> 452
- 451 -> join -> 452
- 452 -> join -> 453
- 453 -> join -> 454
- 454 -> join -> 455
- 455 -> join -> 456
- 456 -> join -> 457
- 457 -> join -> 458
- 458 -> join -> 459 ]} at 459
+ -> 163 ]}
+ -> 325
+ 325 -> Assume: j < 10 false -> 326
+ 326 -> leave_loop -> 327
+ 327 -> LeaveScope: j -> 329
+ 329 -> LeaveScope: j -> 330
+ 330 -> Assign: i = i + 1 -> 332 ]} -> 344
+ 335 -> LeaveScope: i -> 349
+ 336 -> LeaveScope: i -> 350
+ 337 -> LeaveScope: i -> 351
+ 338 -> LeaveScope: i -> 352
+ 339 -> LeaveScope: i -> 353
+ 340 -> LeaveScope: i -> 354
+ 341 -> LeaveScope: i -> 355
+ 342 -> leave_loop -> 343
+ 343 -> LeaveScope: i -> 348
+ 344 -> Assume: i < 10 false -> 345
+ 345 -> leave_loop -> 346
+ 346 -> LeaveScope: i -> 347
+ 347 -> LeaveScope: i -> 356
+ 348 -> LeaveScope: i -> 357
+ 349 -> LeaveScope: i -> 358
+ 350 -> LeaveScope: i -> 359
+ 351 -> LeaveScope: i -> 360
+ 352 -> LeaveScope: i -> 361
+ 353 -> LeaveScope: i -> 362
+ 354 -> LeaveScope: i -> 363
+ 355 -> LeaveScope: i -> 364
+ 356 -> join -> 372
+ 357 -> join -> 371
+ 358 -> join -> 370
+ 359 -> join -> 369
+ 360 -> join -> 368
+ 361 -> join -> 367
+ 362 -> join -> 366
+ 363 -> join -> 365
+ 364 -> join -> 365
+ 365 -> join -> 366
+ 366 -> join -> 367
+ 367 -> join -> 368
+ 368 -> join -> 369
+ 369 -> join -> 370
+ 370 -> join -> 371
+ 371 -> join -> 372 ]} at 372
[from] Computing for function main
[from] Computing for function my_switch <-main
[from] Done for function my_switch
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
+ These dependencies hold at termination for the executions that terminate:
[from] Function my_switch:
\result FROM x_0
[from] Function main:
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
- tmp; i; j; tmp_0
+ tmp; i; j; tmp_0
[inout] Inputs for function main:
- \nothing
-[kernel] user error: no known last created project.
+ \nothing
+[kernel] User Error: no known last created project.
[kernel] Frama-C aborted: invalid user input.