From 16e71c78821bc468502ce9e99a981ed0ff4284cd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 25 Jan 2021 21:18:31 +0100
Subject: [PATCH] [kernel] Interpreted automata: process break statements as
gotos.
---
.../analysis/interpreted_automata.ml | 9 +-
.../wp/oracle/stmtcompiler_test.res.oracle | 22 -
tests/value/traces/oracle/test1.res.oracle | 16 +-
tests/value/traces/oracle/test2.res.oracle | 72 +-
tests/value/traces/oracle/test4.res.oracle | 5 +-
tests/value/traces/oracle/test5.res.oracle | 667 +++++++++---------
6 files changed, 373 insertions(+), 418 deletions(-)
diff --git a/src/kernel_services/analysis/interpreted_automata.ml b/src/kernel_services/analysis/interpreted_automata.ml
index c9aaadb66a7..768ae178c5c 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/src/kernel_services/analysis/interpreted_automata.ml
@@ -145,7 +145,6 @@ type goto_list = (vertex * stmt * stmt) list ref
type control_points = {
src: vertex;
dest: vertex;
- break: vertex option;
continue: vertex option;
}
@@ -385,7 +384,9 @@ let build_automaton ~annotations kf =
control.src
| Break _ ->
- add_jump control.src (Option.get control.break) stmt;
+ assert (List.length stmt.succs = 1);
+ let dest_stmt = List.hd stmt.succs in
+ gotos := (control.src,stmt,dest_stmt) :: !gotos;
control.src
| Continue _ ->
@@ -414,7 +415,6 @@ let build_automaton ~annotations kf =
let block_control = {
control with
src = add_vertex ();
- break = Some control.dest;
} in
do_block block_control kinstr labels block;
(* Then link the cases *)
@@ -466,7 +466,6 @@ let build_automaton ~annotations kf =
then
{ src = control.src;
dest = control.src;
- break = Some control.dest;
continue = Some control.src; }
else
(* We separate loop head from first statement of the loop, otherwise
@@ -493,7 +492,6 @@ let build_automaton ~annotations kf =
in
add_edge loop_back loop_head_point kinstr Skip loc;
{ src=loop_start_body;
- break=Some control.dest;
dest=loop_end_point;
continue=Some loop_end_point; }
in
@@ -529,7 +527,6 @@ let build_automaton ~annotations kf =
let control = {
src = start_code;
dest = end_code;
- break = None;
continue = None;
}
in
diff --git a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
index d1946539852..f660536e9e2 100644
--- a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
@@ -411,7 +411,6 @@ zloop sequent:
Have: i_2 <= 10.
Have: i <= 10.
Have: 10 <= i.
- Have: 10 <= i.
Have: i = 10.
Have: 0 <= x.
Have: foo_1 = 0.
@@ -434,7 +433,6 @@ zloop sequent:
Have: i_1 <= 10.
Have: i_2 <= 10.
Have: 10 <= i_2.
- Have: 10 <= i_2.
Have: i_2 = 10.
}
Prove: 0 <= x.
@@ -454,7 +452,6 @@ zloop sequent:
Have: i_2 <= 10.
Have: i <= 10.
Have: 10 <= i.
- Have: 10 <= i.
}
Prove: i = 10.
@@ -462,24 +459,6 @@ Goal Assertion (file tests/wp/stmtcompiler_test.i, line 85):
Prove: true.
[Qed] Valid
-------------------------------------------------------------
-zloop sequent:
- Assume {
- Have: foo_0 = 42.
- Have: 0 <= x.
- Have: (ta_i_0=true) /\ (ta_i_1=false).
- Have: (Init_i_0=true) /\ (i_1 = 0).
- Have: (Init_i_1=true) /\ ((1 + i_1) = i_2).
- Have: i_2 <= 10.
- Have: i <= 10.
- Have: 10 <= i.
- }
-Prove: 10 <= i.
-
-Goal Assertion (file tests/wp/stmtcompiler_test.i, line 84):
-Prove: true.
-[Qed] Valid
-
------------------------------------------------------------
zloop sequent:
Assume {
@@ -526,7 +505,6 @@ zloop sequent:
Have: i_1 <= 10.
Have: i_2 <= 10.
Have: 10 <= i_2.
- Have: 10 <= i_2.
Have: i_2 = 10.
Have: 0 <= x.
If foo_1 = 0
diff --git a/tests/value/traces/oracle/test1.res.oracle b/tests/value/traces/oracle/test1.res.oracle
index c89a9da2b49..ab2f58b78fa 100644
--- a/tests/value/traces/oracle/test1.res.oracle
+++ b/tests/value/traces/oracle/test1.res.oracle
@@ -56,16 +56,14 @@ c -> 5
37 -> Assume: i < 3 false -> 38
38 -> LeaveScope: i -> 41
39 -> LeaveScope: i -> 40
- 40 -> LeaveScope: i -> 42
- 41 -> LeaveScope: i -> 43
- 42 -> Assign: g = tmp -> 44
- 43 -> Assign: g = tmp -> 45
- 44 -> EnterScope: \result<main> -> 46
- 45 -> EnterScope: \result<main> -> 48
+ 40 -> Assign: g = tmp -> 42
+ 41 -> Assign: g = tmp -> 43
+ 42 -> EnterScope: \result<main> -> 44
+ 43 -> EnterScope: \result<main> -> 46
+ 44 -> Assign: \result<main> = tmp -> 45
+ 45 -> join -> 48
46 -> Assign: \result<main> = tmp -> 47
- 47 -> join -> 50
- 48 -> Assign: \result<main> = tmp -> 49
- 49 -> join -> 50 ]} at 50
+ 47 -> join -> 48 ]} at 48
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
diff --git a/tests/value/traces/oracle/test2.res.oracle b/tests/value/traces/oracle/test2.res.oracle
index 3e1b821db9e..4461099a1ae 100644
--- a/tests/value/traces/oracle/test2.res.oracle
+++ b/tests/value/traces/oracle/test2.res.oracle
@@ -30,7 +30,7 @@ c -> 1
4 -> Assign: tmp = 1 -> 5
5 -> start_call: loop (true) -> 8
6 -> Assign: tmp = 2 -> 7
- 7 -> start_call: loop (true) -> 40
+ 7 -> start_call: loop (true) -> 39
8 -> EnterScope: j -> 9
9 -> Assign: j = tmp -> 10
10 -> EnterScope: i -> 11
@@ -48,43 +48,41 @@ c -> 1
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 -> EnterScope: \result<main> -> 80
- 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 -> 76
- 76 -> finalize_call: loop -> 77
- 77 -> Assign: tmp = \result<loop> -> 78
- 78 -> LeaveScope: \result<loop> -> 79
- 79 -> EnterScope: \result<main> -> 82
+ 25 -> EnterScope: \result<loop> -> 26
+ 26 -> Assign: \result<loop> = j -> 27
+ 27 -> LeaveScope: j -> 35
+ 35 -> finalize_call: loop -> 36
+ 36 -> Assign: tmp = \result<loop> -> 37
+ 37 -> LeaveScope: \result<loop> -> 38
+ 38 -> EnterScope: \result<main> -> 78
+ 39 -> EnterScope: j -> 40
+ 40 -> Assign: j = tmp -> 41
+ 41 -> EnterScope: i -> 43
+ 43 -> initialize variable: i -> 44
+ 44 -> Assign: i = 0 -> 45
+ 45 -> enter_loop -> 46
+ 46 -> Assume: i < 3 true -> 47
+ 47 -> Assign: j = j + 1 -> 48
+ 48 -> Assign: i = i + 1 -> 49
+ 49 -> Assume: i < 3 true -> 50
+ 50 -> Assign: j = j + 1 -> 51
+ 51 -> Assign: i = i + 1 -> 52
+ 52 -> Assume: i < 3 true -> 53
+ 53 -> Assign: j = j + 1 -> 54
+ 54 -> Assign: i = i + 1 -> 55
+ 55 -> Assume: i < 3 false -> 56
+ 56 -> LeaveScope: i -> 57
+ 57 -> EnterScope: \result<loop> -> 58
+ 58 -> Assign: \result<loop> = j -> 59
+ 59 -> LeaveScope: j -> 74
+ 74 -> finalize_call: loop -> 75
+ 75 -> Assign: tmp = \result<loop> -> 76
+ 76 -> LeaveScope: \result<loop> -> 77
+ 77 -> EnterScope: \result<main> -> 80
+ 78 -> Assign: \result<main> = tmp -> 79
+ 79 -> join -> 82
80 -> Assign: \result<main> = tmp -> 81
- 81 -> join -> 84
- 82 -> Assign: \result<main> = tmp -> 83
- 83 -> join -> 84 ]} at 84
+ 81 -> join -> 82 ]} at 82
[from] Computing for function loop
[from] Done for function loop
[from] Computing for function main
diff --git a/tests/value/traces/oracle/test4.res.oracle b/tests/value/traces/oracle/test4.res.oracle
index 45691fa981c..a115bd4a4c9 100644
--- a/tests/value/traces/oracle/test4.res.oracle
+++ b/tests/value/traces/oracle/test4.res.oracle
@@ -261,9 +261,8 @@ c -> 1
228 -> Assume: i < 100 false -> 229
229 -> leave_loop -> 230
230 -> LeaveScope: i -> 231
- 231 -> LeaveScope: i -> 232
- 232 -> EnterScope: \result<main> -> 233
- 233 -> Assign: \result<main> = tmp -> 234 ]} at 234
+ 231 -> EnterScope: \result<main> -> 232
+ 232 -> Assign: \result<main> = tmp -> 233 ]} at 233
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
diff --git a/tests/value/traces/oracle/test5.res.oracle b/tests/value/traces/oracle/test5.res.oracle
index 739104c81f0..03267cb12e6 100644
--- a/tests/value/traces/oracle/test5.res.oracle
+++ b/tests/value/traces/oracle/test5.res.oracle
@@ -212,370 +212,355 @@ c -> 1
109 -> Assign: tmp = tmp_0 + tmp -> 110
110 -> LeaveScope: tmp_0 -> 111
111 -> Assign: j = j + 1 -> 112
- 112 -> Assume: j < 10 false -> 113; join -> 122
+ 112 -> Assume: j < 10 false -> 113; join -> 121
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; 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; 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 -> join -> 151
- 151 -> join -> 153
- 153 -> join -> 159
- 159 -> join -> 162
- 162 -> Loop(16) 149 {[ 149 -> Assume: j < 10 true -> 150
- 150 -> EnterScope: tmp_0 -> 152
- 152 -> EnterScope: \result<my_switch> -> 154
- 154 -> CallDeclared:
+ 114 -> Assign: i = i + 1 -> 115
+ 115 -> Assume: i < 10 true -> 116
+ 116 -> EnterScope: j -> 117
+ 117 -> initialize variable: j -> 118
+ 118 -> Assign: j = 0 -> 119
+ 119 -> enter_loop -> 120
+ 120 -> join -> 121
+ 121 -> Assume: j < 10 true -> 122; join -> 132
+ 122 -> EnterScope: tmp_0 -> 123; join -> 134
+ 123 -> EnterScope: \result<my_switch> -> 124; join -> 136
+ 124 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 125
+ 125 -> Assign: tmp_0 = \result<my_switch> -> 127
+ 127 -> LeaveScope: \result<my_switch> -> 128
+ 128 -> Assign: tmp = tmp_0 + tmp -> 129; join -> 142
+ 129 -> LeaveScope: tmp_0 -> 130
+ 130 -> Assign: j = j + 1 -> 131; join -> 145
+ 131 -> join -> 132
+ 132 -> Assume: j < 10 true -> 133; join -> 147
+ 133 -> join -> 134
+ 134 -> EnterScope: tmp_0 -> 135; join -> 150
+ 135 -> join -> 136
+ 136 -> EnterScope: \result<my_switch> -> 137; join -> 152
+ 137 -> CallDeclared: \result<my_switch> = my_switch(tmp) -> 138
+ 138 -> Assign: tmp_0 = \result<my_switch> -> 140
+ 140 -> LeaveScope: \result<my_switch> -> 141
+ 141 -> join -> 142
+ 142 -> Assign: tmp = tmp_0 + tmp -> 143; join -> 158
+ 143 -> LeaveScope: tmp_0 -> 144
+ 144 -> join -> 145
+ 145 -> Assign: j = j + 1 -> 146; join -> 161
+ 146 -> join -> 147
+ 147 -> join -> 150
+ 150 -> join -> 152
+ 152 -> join -> 158
+ 158 -> join -> 161
+ 161 -> Loop(16) 148 {[ 148 -> Assume: j < 10 true -> 149
+ 149 -> EnterScope: tmp_0 -> 151
+ 151 -> EnterScope: \result<my_switch> -> 153
+ 153 -> CallDeclared:
\result<my_switch> =
- 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 ]} -> 166;
- join -> 177
- 166 -> Assume: j < 10 false -> 167
- 167 -> leave_loop -> 168
- 168 -> LeaveScope: j -> 169
- 169 -> LeaveScope: j -> 170
- 170 -> Assign: i = i + 1 -> 171
- 171 -> Assume: i < 10 true -> 172
- 172 -> EnterScope: j -> 173
- 173 -> initialize variable: j -> 174
- 174 -> Assign: j = 0 -> 175
- 175 -> enter_loop -> 176
- 176 -> join -> 177
- 177 -> Loop(16) 149 {[ 149 -> Assume: j < 10 true -> 150
- 150 -> EnterScope: tmp_0 -> 152
- 152 -> EnterScope: \result<my_switch> -> 154
- 154 -> CallDeclared:
+ my_switch(tmp) -> 154
+ 154 -> Assign: tmp_0 = \result<my_switch> -> 156
+ 156 -> LeaveScope: \result<my_switch> -> 157
+ 157 -> Assign: tmp = tmp_0 + tmp -> 159
+ 159 -> LeaveScope: tmp_0 -> 160
+ 160 -> Assign: j = j + 1 -> 162 ]} -> 165;
+ join -> 175
+ 165 -> Assume: j < 10 false -> 166
+ 166 -> leave_loop -> 167
+ 167 -> LeaveScope: j -> 168
+ 168 -> Assign: i = i + 1 -> 169
+ 169 -> Assume: i < 10 true -> 170
+ 170 -> EnterScope: j -> 171
+ 171 -> initialize variable: j -> 172
+ 172 -> Assign: j = 0 -> 173
+ 173 -> enter_loop -> 174
+ 174 -> join -> 175
+ 175 -> Loop(16) 148 {[ 148 -> Assume: j < 10 true -> 149
+ 149 -> EnterScope: tmp_0 -> 151
+ 151 -> EnterScope: \result<my_switch> -> 153
+ 153 -> CallDeclared:
\result<my_switch> =
- 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 ]} -> 179;
- join -> 190
- 179 -> Assume: j < 10 false -> 180
- 180 -> leave_loop -> 181
- 181 -> LeaveScope: j -> 182
- 182 -> LeaveScope: j -> 183
- 183 -> Assign: i = i + 1 -> 184
- 184 -> Assume: i < 10 true -> 185
- 185 -> EnterScope: j -> 186
- 186 -> initialize variable: j -> 187
- 187 -> Assign: j = 0 -> 188
- 188 -> enter_loop -> 189
- 189 -> join -> 190
- 190 -> Loop(16) 149 {[ 149 -> Assume: j < 10 true -> 150
- 150 -> EnterScope: tmp_0 -> 152
- 152 -> EnterScope: \result<my_switch> -> 154
- 154 -> CallDeclared:
+ my_switch(tmp) -> 154
+ 154 -> Assign: tmp_0 = \result<my_switch> -> 156
+ 156 -> LeaveScope: \result<my_switch> -> 157
+ 157 -> Assign: tmp = tmp_0 + tmp -> 159
+ 159 -> LeaveScope: tmp_0 -> 160
+ 160 -> Assign: j = j + 1 -> 162 ]} -> 177;
+ join -> 187
+ 177 -> Assume: j < 10 false -> 178
+ 178 -> leave_loop -> 179
+ 179 -> LeaveScope: j -> 180
+ 180 -> Assign: i = i + 1 -> 181
+ 181 -> Assume: i < 10 true -> 182
+ 182 -> EnterScope: j -> 183
+ 183 -> initialize variable: j -> 184
+ 184 -> Assign: j = 0 -> 185
+ 185 -> enter_loop -> 186
+ 186 -> join -> 187
+ 187 -> Loop(16) 148 {[ 148 -> Assume: j < 10 true -> 149
+ 149 -> EnterScope: tmp_0 -> 151
+ 151 -> EnterScope: \result<my_switch> -> 153
+ 153 -> CallDeclared:
\result<my_switch> =
- 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 ]} -> 192;
- join -> 203
- 192 -> Assume: j < 10 false -> 193
- 193 -> leave_loop -> 194
- 194 -> LeaveScope: j -> 195
- 195 -> LeaveScope: j -> 196
- 196 -> Assign: i = i + 1 -> 197
- 197 -> Assume: i < 10 true -> 198
- 198 -> EnterScope: j -> 199
- 199 -> initialize variable: j -> 200
- 200 -> Assign: j = 0 -> 201
- 201 -> enter_loop -> 202
- 202 -> join -> 203
- 203 -> Loop(16) 149 {[ 149 -> Assume: j < 10 true -> 150
- 150 -> EnterScope: tmp_0 -> 152
- 152 -> EnterScope: \result<my_switch> -> 154
- 154 -> CallDeclared:
+ my_switch(tmp) -> 154
+ 154 -> Assign: tmp_0 = \result<my_switch> -> 156
+ 156 -> LeaveScope: \result<my_switch> -> 157
+ 157 -> Assign: tmp = tmp_0 + tmp -> 159
+ 159 -> LeaveScope: tmp_0 -> 160
+ 160 -> Assign: j = j + 1 -> 162 ]} -> 189;
+ join -> 199
+ 189 -> Assume: j < 10 false -> 190
+ 190 -> leave_loop -> 191
+ 191 -> LeaveScope: j -> 192
+ 192 -> Assign: i = i + 1 -> 193
+ 193 -> Assume: i < 10 true -> 194
+ 194 -> EnterScope: j -> 195
+ 195 -> initialize variable: j -> 196
+ 196 -> Assign: j = 0 -> 197
+ 197 -> enter_loop -> 198
+ 198 -> join -> 199
+ 199 -> Loop(16) 148 {[ 148 -> Assume: j < 10 true -> 149
+ 149 -> EnterScope: tmp_0 -> 151
+ 151 -> EnterScope: \result<my_switch> -> 153
+ 153 -> CallDeclared:
\result<my_switch> =
- 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 ]} -> 205;
- join -> 216
- 205 -> Assume: j < 10 false -> 206
- 206 -> leave_loop -> 207
- 207 -> LeaveScope: j -> 208
- 208 -> LeaveScope: j -> 209
- 209 -> Assign: i = i + 1 -> 210
- 210 -> Assume: i < 10 true -> 211
- 211 -> EnterScope: j -> 212
- 212 -> initialize variable: j -> 213
- 213 -> Assign: j = 0 -> 214
- 214 -> enter_loop -> 215
- 215 -> join -> 216
- 216 -> Loop(16) 149 {[ 149 -> Assume: j < 10 true -> 150
- 150 -> EnterScope: tmp_0 -> 152
- 152 -> EnterScope: \result<my_switch> -> 154
- 154 -> CallDeclared:
+ my_switch(tmp) -> 154
+ 154 -> Assign: tmp_0 = \result<my_switch> -> 156
+ 156 -> LeaveScope: \result<my_switch> -> 157
+ 157 -> Assign: tmp = tmp_0 + tmp -> 159
+ 159 -> LeaveScope: tmp_0 -> 160
+ 160 -> Assign: j = j + 1 -> 162 ]} -> 201;
+ join -> 211
+ 201 -> Assume: j < 10 false -> 202
+ 202 -> leave_loop -> 203
+ 203 -> LeaveScope: j -> 204
+ 204 -> Assign: i = i + 1 -> 205
+ 205 -> Assume: i < 10 true -> 206
+ 206 -> EnterScope: j -> 207
+ 207 -> initialize variable: j -> 208
+ 208 -> Assign: j = 0 -> 209
+ 209 -> enter_loop -> 210
+ 210 -> join -> 211
+ 211 -> Loop(16) 148 {[ 148 -> Assume: j < 10 true -> 149
+ 149 -> EnterScope: tmp_0 -> 151
+ 151 -> EnterScope: \result<my_switch> -> 153
+ 153 -> CallDeclared:
\result<my_switch> =
- 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 ]} -> 218;
- join -> 229
- 218 -> Assume: j < 10 false -> 219
- 219 -> leave_loop -> 220
- 220 -> LeaveScope: j -> 221
- 221 -> LeaveScope: j -> 222
- 222 -> Assign: i = i + 1 -> 223
- 223 -> Assume: i < 10 true -> 224
- 224 -> EnterScope: j -> 225
- 225 -> initialize variable: j -> 226
- 226 -> Assign: j = 0 -> 227
- 227 -> enter_loop -> 228
- 228 -> join -> 229
- 229 -> Loop(16) 149 {[ 149 -> Assume: j < 10 true -> 150
- 150 -> EnterScope: tmp_0 -> 152
- 152 -> EnterScope: \result<my_switch> -> 154
- 154 -> CallDeclared:
+ my_switch(tmp) -> 154
+ 154 -> Assign: tmp_0 = \result<my_switch> -> 156
+ 156 -> LeaveScope: \result<my_switch> -> 157
+ 157 -> Assign: tmp = tmp_0 + tmp -> 159
+ 159 -> LeaveScope: tmp_0 -> 160
+ 160 -> Assign: j = j + 1 -> 162 ]} -> 213;
+ join -> 223
+ 213 -> Assume: j < 10 false -> 214
+ 214 -> leave_loop -> 215
+ 215 -> LeaveScope: j -> 216
+ 216 -> Assign: i = i + 1 -> 217
+ 217 -> Assume: i < 10 true -> 218
+ 218 -> EnterScope: j -> 219
+ 219 -> initialize variable: j -> 220
+ 220 -> Assign: j = 0 -> 221
+ 221 -> enter_loop -> 222
+ 222 -> join -> 223
+ 223 -> Loop(16) 148 {[ 148 -> Assume: j < 10 true -> 149
+ 149 -> EnterScope: tmp_0 -> 151
+ 151 -> EnterScope: \result<my_switch> -> 153
+ 153 -> CallDeclared:
\result<my_switch> =
- 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 ]} -> 231;
- join -> 242
- 231 -> Assume: j < 10 false -> 232
- 232 -> leave_loop -> 233
- 233 -> LeaveScope: j -> 234
- 234 -> LeaveScope: j -> 235
- 235 -> Assign: i = i + 1 -> 236
- 236 -> Assume: i < 10 true -> 237
- 237 -> EnterScope: j -> 238
- 238 -> initialize variable: j -> 239
- 239 -> Assign: j = 0 -> 240
- 240 -> enter_loop -> 241
- 241 -> join -> 242
- 242 -> Loop(16) 149 {[ 149 -> Assume: j < 10 true -> 150
- 150 -> EnterScope: tmp_0 -> 152
- 152 -> EnterScope: \result<my_switch> -> 154
- 154 -> CallDeclared:
+ my_switch(tmp) -> 154
+ 154 -> Assign: tmp_0 = \result<my_switch> -> 156
+ 156 -> LeaveScope: \result<my_switch> -> 157
+ 157 -> Assign: tmp = tmp_0 + tmp -> 159
+ 159 -> LeaveScope: tmp_0 -> 160
+ 160 -> Assign: j = j + 1 -> 162 ]} -> 225;
+ join -> 235
+ 225 -> Assume: j < 10 false -> 226
+ 226 -> leave_loop -> 227
+ 227 -> LeaveScope: j -> 228
+ 228 -> Assign: i = i + 1 -> 229
+ 229 -> Assume: i < 10 true -> 230
+ 230 -> EnterScope: j -> 231
+ 231 -> initialize variable: j -> 232
+ 232 -> Assign: j = 0 -> 233
+ 233 -> enter_loop -> 234
+ 234 -> join -> 235
+ 235 -> Loop(16) 148 {[ 148 -> Assume: j < 10 true -> 149
+ 149 -> EnterScope: tmp_0 -> 151
+ 151 -> EnterScope: \result<my_switch> -> 153
+ 153 -> CallDeclared:
\result<my_switch> =
- 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 ]} -> 244;
- join -> 255
- 244 -> Assume: j < 10 false -> 245
- 245 -> leave_loop -> 246
- 246 -> LeaveScope: j -> 247
- 247 -> LeaveScope: j -> 248
- 248 -> Assign: i = i + 1 -> 249
- 249 -> Assume: i < 10 true -> 250
- 250 -> EnterScope: j -> 251
- 251 -> initialize variable: j -> 252
- 252 -> Assign: j = 0 -> 253
- 253 -> enter_loop -> 254
- 254 -> join -> 255
- 255 -> Loop(16) 149 {[ 149 -> Assume: j < 10 true -> 150
- 150 -> EnterScope: tmp_0 -> 152
- 152 -> EnterScope: \result<my_switch> -> 154
- 154 -> CallDeclared:
+ my_switch(tmp) -> 154
+ 154 -> Assign: tmp_0 = \result<my_switch> -> 156
+ 156 -> LeaveScope: \result<my_switch> -> 157
+ 157 -> Assign: tmp = tmp_0 + tmp -> 159
+ 159 -> LeaveScope: tmp_0 -> 160
+ 160 -> Assign: j = j + 1 -> 162 ]} -> 237;
+ join -> 247
+ 237 -> Assume: j < 10 false -> 238
+ 238 -> leave_loop -> 239
+ 239 -> LeaveScope: j -> 240
+ 240 -> Assign: i = i + 1 -> 241
+ 241 -> Assume: i < 10 true -> 242
+ 242 -> EnterScope: j -> 243
+ 243 -> initialize variable: j -> 244
+ 244 -> Assign: j = 0 -> 245
+ 245 -> enter_loop -> 246
+ 246 -> join -> 247
+ 247 -> Loop(16) 148 {[ 148 -> Assume: j < 10 true -> 149
+ 149 -> EnterScope: tmp_0 -> 151
+ 151 -> EnterScope: \result<my_switch> -> 153
+ 153 -> CallDeclared:
\result<my_switch> =
- 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 ]} -> 257;
- join -> 268
- 257 -> Assume: j < 10 false -> 258
- 258 -> leave_loop -> 259
- 259 -> LeaveScope: j -> 260
- 260 -> LeaveScope: j -> 261
- 261 -> Assign: i = i + 1 -> 262
- 262 -> Assume: i < 10 true -> 263
- 263 -> EnterScope: j -> 264
- 264 -> initialize variable: j -> 265
- 265 -> Assign: j = 0 -> 266
- 266 -> enter_loop -> 267
- 267 -> join -> 268
- 268 -> Loop(16) 149 {[ 149 -> Assume: j < 10 true -> 150
- 150 -> EnterScope: tmp_0 -> 152
- 152 -> EnterScope: \result<my_switch> -> 154
- 154 -> CallDeclared:
+ my_switch(tmp) -> 154
+ 154 -> Assign: tmp_0 = \result<my_switch> -> 156
+ 156 -> LeaveScope: \result<my_switch> -> 157
+ 157 -> Assign: tmp = tmp_0 + tmp -> 159
+ 159 -> LeaveScope: tmp_0 -> 160
+ 160 -> Assign: j = j + 1 -> 162 ]} -> 249;
+ join -> 259
+ 249 -> Assume: j < 10 false -> 250
+ 250 -> leave_loop -> 251
+ 251 -> LeaveScope: j -> 252
+ 252 -> Assign: i = i + 1 -> 253
+ 253 -> Assume: i < 10 true -> 254
+ 254 -> EnterScope: j -> 255
+ 255 -> initialize variable: j -> 256
+ 256 -> Assign: j = 0 -> 257
+ 257 -> enter_loop -> 258
+ 258 -> join -> 259
+ 259 -> Loop(16) 148 {[ 148 -> Assume: j < 10 true -> 149
+ 149 -> EnterScope: tmp_0 -> 151
+ 151 -> EnterScope: \result<my_switch> -> 153
+ 153 -> CallDeclared:
\result<my_switch> =
- 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 ]} -> 270;
- join -> 281
- 270 -> Assume: j < 10 false -> 271
- 271 -> leave_loop -> 272
- 272 -> LeaveScope: j -> 273
- 273 -> LeaveScope: j -> 274
- 274 -> Assign: i = i + 1 -> 275
- 275 -> Assume: i < 10 true -> 276; join -> 289
- 276 -> EnterScope: j -> 277; join -> 291
- 277 -> initialize variable: j -> 278
- 278 -> Assign: j = 0 -> 279
- 279 -> enter_loop -> 280
- 280 -> join -> 281
- 281 -> Loop(16) 149 {[ 149 -> Assume: j < 10 true -> 150
- 150 -> EnterScope: tmp_0 -> 152
- 152 -> EnterScope: \result<my_switch> -> 154
- 154 -> CallDeclared:
+ my_switch(tmp) -> 154
+ 154 -> Assign: tmp_0 = \result<my_switch> -> 156
+ 156 -> LeaveScope: \result<my_switch> -> 157
+ 157 -> Assign: tmp = tmp_0 + tmp -> 159
+ 159 -> LeaveScope: tmp_0 -> 160
+ 160 -> Assign: j = j + 1 -> 162 ]} -> 261;
+ join -> 271
+ 261 -> Assume: j < 10 false -> 262
+ 262 -> leave_loop -> 263
+ 263 -> LeaveScope: j -> 264
+ 264 -> Assign: i = i + 1 -> 265
+ 265 -> Assume: i < 10 true -> 266; join -> 278
+ 266 -> EnterScope: j -> 267; join -> 280
+ 267 -> initialize variable: j -> 268
+ 268 -> Assign: j = 0 -> 269
+ 269 -> enter_loop -> 270
+ 270 -> join -> 271
+ 271 -> Loop(16) 148 {[ 148 -> Assume: j < 10 true -> 149
+ 149 -> EnterScope: tmp_0 -> 151
+ 151 -> EnterScope: \result<my_switch> -> 153
+ 153 -> CallDeclared:
\result<my_switch> =
- 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 ]} -> 283;
- join -> 296
- 283 -> Assume: j < 10 false -> 284
- 284 -> leave_loop -> 285
- 285 -> LeaveScope: j -> 286; join -> 301
- 286 -> LeaveScope: j -> 287
- 287 -> Assign: i = i + 1 -> 288; join -> 304
- 288 -> join -> 289
- 289 -> Assume: i < 10 true -> 290; join -> 306
- 290 -> join -> 291
- 291 -> EnterScope: j -> 292; join -> 308
- 292 -> initialize variable: j -> 293
- 293 -> Assign: j = 0 -> 294
- 294 -> enter_loop -> 295
- 295 -> join -> 296
- 296 -> Loop(16) 149 {[ 149 -> Assume: j < 10 true -> 150
- 150 -> EnterScope: tmp_0 -> 152
- 152 -> EnterScope: \result<my_switch> -> 154
- 154 -> CallDeclared:
+ my_switch(tmp) -> 154
+ 154 -> Assign: tmp_0 = \result<my_switch> -> 156
+ 156 -> LeaveScope: \result<my_switch> -> 157
+ 157 -> Assign: tmp = tmp_0 + tmp -> 159
+ 159 -> LeaveScope: tmp_0 -> 160
+ 160 -> Assign: j = j + 1 -> 162 ]} -> 273;
+ join -> 285
+ 273 -> Assume: j < 10 false -> 274
+ 274 -> leave_loop -> 275
+ 275 -> LeaveScope: j -> 276; join -> 290
+ 276 -> Assign: i = i + 1 -> 277; join -> 292
+ 277 -> join -> 278
+ 278 -> Assume: i < 10 true -> 279; join -> 294
+ 279 -> join -> 280
+ 280 -> EnterScope: j -> 281; join -> 296
+ 281 -> initialize variable: j -> 282
+ 282 -> Assign: j = 0 -> 283
+ 283 -> enter_loop -> 284
+ 284 -> join -> 285
+ 285 -> Loop(16) 148 {[ 148 -> Assume: j < 10 true -> 149
+ 149 -> EnterScope: tmp_0 -> 151
+ 151 -> EnterScope: \result<my_switch> -> 153
+ 153 -> CallDeclared:
\result<my_switch> =
- 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 ]} -> 298;
- join -> 313
- 298 -> Assume: j < 10 false -> 299
- 299 -> leave_loop -> 300
+ my_switch(tmp) -> 154
+ 154 -> Assign: tmp_0 = \result<my_switch> -> 156
+ 156 -> LeaveScope: \result<my_switch> -> 157
+ 157 -> Assign: tmp = tmp_0 + tmp -> 159
+ 159 -> LeaveScope: tmp_0 -> 160
+ 160 -> Assign: j = j + 1 -> 162 ]} -> 287;
+ join -> 301
+ 287 -> Assume: j < 10 false -> 288
+ 288 -> leave_loop -> 289
+ 289 -> join -> 290
+ 290 -> LeaveScope: j -> 291; join -> 306
+ 291 -> join -> 292
+ 292 -> Assign: i = i + 1 -> 293; join -> 308
+ 293 -> join -> 294
+ 294 -> Assume: i < 10 true -> 295; join -> 310
+ 295 -> join -> 296
+ 296 -> EnterScope: j -> 297; join -> 313
+ 297 -> initialize variable: j -> 298
+ 298 -> Assign: j = 0 -> 299
+ 299 -> enter_loop -> 300
300 -> join -> 301
- 301 -> LeaveScope: j -> 302; join -> 318
- 302 -> LeaveScope: j -> 303
- 303 -> join -> 304
- 304 -> Assign: i = i + 1 -> 305; join -> 321
+ 301 -> Loop(16) 148 {[ 148 -> Assume: j < 10 true -> 149
+ 149 -> EnterScope: tmp_0 -> 151
+ 151 -> EnterScope: \result<my_switch> -> 153
+ 153 -> CallDeclared:
+ \result<my_switch> =
+ my_switch(tmp) -> 154
+ 154 -> Assign: tmp_0 = \result<my_switch> -> 156
+ 156 -> LeaveScope: \result<my_switch> -> 157
+ 157 -> Assign: tmp = tmp_0 + tmp -> 159
+ 159 -> LeaveScope: tmp_0 -> 160
+ 160 -> Assign: j = j + 1 -> 162 ]} -> 303;
+ join -> 318
+ 303 -> Assume: j < 10 false -> 304
+ 304 -> leave_loop -> 305
305 -> join -> 306
- 306 -> Assume: i < 10 true -> 307; join -> 323
+ 306 -> LeaveScope: j -> 307; join -> 323
307 -> join -> 308
- 308 -> EnterScope: j -> 309; join -> 326
- 309 -> initialize variable: j -> 310
- 310 -> Assign: j = 0 -> 311
- 311 -> enter_loop -> 312
- 312 -> join -> 313
- 313 -> 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) -> 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 ]} -> 315;
- join -> 331
- 315 -> Assume: j < 10 false -> 316
- 316 -> leave_loop -> 317
- 317 -> join -> 318
- 318 -> LeaveScope: j -> 319; join -> 336
- 319 -> LeaveScope: j -> 320
- 320 -> join -> 321
- 321 -> Assign: i = i + 1 -> 322; join -> 339
- 322 -> join -> 323
- 323 -> join -> 326
- 326 -> join -> 331
- 331 -> join -> 336
- 336 -> join -> 339
- 339 -> Loop(10) 324 {[ 324 -> Assume: i < 10 true -> 325
- 325 -> EnterScope: j -> 327
- 327 -> initialize variable: j -> 328
- 328 -> Assign: j = 0 -> 329
- 329 -> enter_loop -> 330
- 330 -> Loop(16) 149 {[ 149 -> Assume:
+ 308 -> Assign: i = i + 1 -> 309; join -> 325
+ 309 -> join -> 310
+ 310 -> join -> 313
+ 313 -> join -> 318
+ 318 -> join -> 323
+ 323 -> join -> 325
+ 325 -> Loop(10) 311 {[ 311 -> Assume: i < 10 true -> 312
+ 312 -> EnterScope: j -> 314
+ 314 -> initialize variable: j -> 315
+ 315 -> Assign: j = 0 -> 316
+ 316 -> enter_loop -> 317
+ 317 -> Loop(16) 148 {[ 148 -> Assume:
j < 10 true
- -> 150
- 150 -> EnterScope:
- tmp_0 -> 152
- 152 -> EnterScope:
+ -> 149
+ 149 -> EnterScope:
+ tmp_0 -> 151
+ 151 -> EnterScope:
\result<my_switch>
- -> 154
- 154 -> CallDeclared:
+ -> 153
+ 153 -> CallDeclared:
\result<my_switch> =
my_switch(
- tmp) -> 155
- 155 -> Assign:
+ tmp) -> 154
+ 154 -> Assign:
tmp_0 = \result<my_switch>
- -> 157
- 157 -> LeaveScope:
+ -> 156
+ 156 -> LeaveScope:
\result<my_switch>
- -> 158
- 158 -> Assign:
+ -> 157
+ 157 -> Assign:
tmp = tmp_0 + tmp
- -> 160
- 160 -> LeaveScope:
- tmp_0 -> 161
- 161 -> Assign:
+ -> 159
+ 159 -> LeaveScope:
+ tmp_0 -> 160
+ 160 -> Assign:
j = j + 1
- -> 163 ]}
- -> 333
- 333 -> Assume: j < 10 false -> 334
- 334 -> leave_loop -> 335
- 335 -> LeaveScope: j -> 337
- 337 -> LeaveScope: j -> 338
- 338 -> Assign: i = i + 1 -> 340 ]} -> 343
- 343 -> Assume: i < 10 false -> 344
- 344 -> leave_loop -> 345
- 345 -> LeaveScope: i -> 346
- 346 -> LeaveScope: i -> 347
- 347 -> EnterScope: \result<main> -> 348
- 348 -> Assign: \result<main> = tmp -> 349 ]} at 349
+ -> 162 ]}
+ -> 320
+ 320 -> Assume: j < 10 false -> 321
+ 321 -> leave_loop -> 322
+ 322 -> LeaveScope: j -> 324
+ 324 -> Assign: i = i + 1 -> 326 ]} -> 329
+ 329 -> Assume: i < 10 false -> 330
+ 330 -> leave_loop -> 331
+ 331 -> LeaveScope: i -> 332
+ 332 -> EnterScope: \result<main> -> 333
+ 333 -> Assign: \result<main> = tmp -> 334 ]} at 334
[from] Computing for function main
[from] Computing for function my_switch <-main
[from] Done for function my_switch
--
GitLab