From 267a2df5fbe9978afae36768a98c59f82cfaa734 Mon Sep 17 00:00:00 2001
From: Bouillaguet Quentin <quentin.bouillaguet@cea.fr>
Date: Thu, 22 Nov 2018 11:46:49 +0100
Subject: [PATCH] [Eva] Check and update oracles
Verified by comparing pre and post rebase generated dots.
Inversion of generated nodes seems to be the result of now different
order of calling assume (with true or false).
---
tests/value/traces/oracle/test1.res.oracle | 114 +--
tests/value/traces/oracle/test2.res.oracle | 168 ++--
tests/value/traces/oracle/test3.res.oracle | 38 +-
tests/value/traces/oracle/test4.res.oracle | 457 ++++-----
tests/value/traces/oracle/test5.res.oracle | 1011 ++++++++++----------
5 files changed, 913 insertions(+), 875 deletions(-)
diff --git a/tests/value/traces/oracle/test1.res.oracle b/tests/value/traces/oracle/test1.res.oracle
index fb550f92c6d..011f6645879 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 b855d5a7819..963ee92ec44 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 a5b57bde5ac..f773988a12d 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 f8b7c0adf4e..58d76d12376 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 9c6a9068b06..44b41790709 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.
--
GitLab