1 | Warning (during instrumentation): |
---|
2 | Clight instrumentation is not implemented yet. |
---|
3 | Checking execution traces...OK. |
---|
4 | ing has cost 0. |
---|
5 | Warning: branching to if_jian12 has cost 1; continuing has cost 3. |
---|
6 | Warning: branching to if_jian13 has cost 2; continuing has cost 3. |
---|
7 | Call(func,stop) |
---|
8 | Regular(seq,stop) |
---|
9 | Regular(cost,seq) |
---|
10 | Regular(call,seq) |
---|
11 | Call(func,call) |
---|
12 | Regular(seq,call) |
---|
13 | Regular(cost,seq) |
---|
14 | Regular(assign t1,seq) |
---|
15 | Regular(skip,seq) |
---|
16 | Regular(seq,call) |
---|
17 | Regular(cost,seq) |
---|
18 | Regular(assign t2,seq) |
---|
19 | Regular(skip,seq) |
---|
20 | Regular(seq,call) |
---|
21 | Regular(cost,seq) |
---|
22 | Regular(assign t3,seq) |
---|
23 | Regular(skip,seq) |
---|
24 | Regular(seq,call) |
---|
25 | Regular(cost,seq) |
---|
26 | Regular(ifthenelse,seq) |
---|
27 | Regular(seq,seq) |
---|
28 | Regular(cost,seq) |
---|
29 | Regular(assign t4,seq) |
---|
30 | Regular(skip,seq) |
---|
31 | Regular(seq,seq) |
---|
32 | Regular(cost,seq) |
---|
33 | Regular(assign t5,seq) |
---|
34 | Regular(skip,seq) |
---|
35 | Regular(cost,seq) |
---|
36 | Regular(assign u,seq) |
---|
37 | Regular(skip,seq) |
---|
38 | Regular(cost,call) |
---|
39 | Regular(return,call) |
---|
40 | Return(Int(22),call) |
---|
41 | Regular(skip,seq) |
---|
42 | Regular(seq,stop) |
---|
43 | Regular(cost,seq) |
---|
44 | Regular(call,seq) |
---|
45 | Call(func,call) |
---|
46 | Regular(seq,call) |
---|
47 | Regular(cost,seq) |
---|
48 | Regular(ifthenelse,seq) |
---|
49 | Regular(seq,seq) |
---|
50 | Regular(cost,seq) |
---|
51 | Regular(assign e,seq) |
---|
52 | Regular(skip,seq) |
---|
53 | Regular(seq,seq) |
---|
54 | Regular(cost,seq) |
---|
55 | Regular(assign e,seq) |
---|
56 | Regular(skip,seq) |
---|
57 | Regular(cost,seq) |
---|
58 | Regular(assign g,seq) |
---|
59 | Regular(skip,seq) |
---|
60 | Regular(cost,call) |
---|
61 | Regular(return,call) |
---|
62 | Return(Int(6),call) |
---|
63 | Regular(skip,seq) |
---|
64 | Regular(seq,stop) |
---|
65 | Regular(cost,seq) |
---|
66 | Regular(call,seq) |
---|
67 | Call(func,call) |
---|
68 | Regular(seq,call) |
---|
69 | Regular(cost,seq) |
---|
70 | Regular(ifthenelse,seq) |
---|
71 | Regular(cost,seq) |
---|
72 | Regular(ifthenelse,seq) |
---|
73 | Regular(cost,seq) |
---|
74 | Regular(assign result,seq) |
---|
75 | Regular(skip,seq) |
---|
76 | Regular(cost,call) |
---|
77 | Regular(return,call) |
---|
78 | Return(Int(2),call) |
---|
79 | Regular(skip,seq) |
---|
80 | Regular(seq,stop) |
---|
81 | Regular(cost,seq) |
---|
82 | Regular(call,seq) |
---|
83 | Call(func,call) |
---|
84 | Regular(seq,call) |
---|
85 | Regular(cost,seq) |
---|
86 | Regular(ifthenelse,seq) |
---|
87 | Regular(cost,seq) |
---|
88 | Regular(ifthenelse,seq) |
---|
89 | Regular(cost,seq) |
---|
90 | Regular(assign result,seq) |
---|
91 | Regular(skip,seq) |
---|
92 | Regular(cost,call) |
---|
93 | Regular(return,call) |
---|
94 | Return(Int(2),call) |
---|
95 | Regular(skip,seq) |
---|
96 | Regular(seq,stop) |
---|
97 | Regular(cost,seq) |
---|
98 | Regular(call,seq) |
---|
99 | Call(func,call) |
---|
100 | Regular(seq,call) |
---|
101 | Regular(cost,seq) |
---|
102 | Regular(ifthenelse,seq) |
---|
103 | Regular(cost,seq) |
---|
104 | Regular(assign min,seq) |
---|
105 | Regular(skip,seq) |
---|
106 | Regular(cost,call) |
---|
107 | Regular(return,call) |
---|
108 | Return(Int(1),call) |
---|
109 | Regular(skip,seq) |
---|
110 | Regular(seq,stop) |
---|
111 | Regular(cost,seq) |
---|
112 | Regular(call,seq) |
---|
113 | Call(func,call) |
---|
114 | Regular(seq,call) |
---|
115 | Regular(cost,seq) |
---|
116 | Regular(assign a,seq) |
---|
117 | Regular(skip,seq) |
---|
118 | Regular(seq,call) |
---|
119 | Regular(cost,seq) |
---|
120 | Regular(ifthenelse,seq) |
---|
121 | Regular(cost,seq) |
---|
122 | Regular(assign b,seq) |
---|
123 | Regular(skip,seq) |
---|
124 | Regular(cost,call) |
---|
125 | Regular(return,call) |
---|
126 | Return(Int(3),call) |
---|
127 | Regular(skip,seq) |
---|
128 | Regular(seq,stop) |
---|
129 | Regular(cost,seq) |
---|
130 | Regular(call,seq) |
---|
131 | Call(func,call) |
---|
132 | Regular(seq,call) |
---|
133 | Regular(cost,seq) |
---|
134 | Regular(assign c,seq) |
---|
135 | Regular(skip,seq) |
---|
136 | Regular(seq,call) |
---|
137 | Regular(cost,seq) |
---|
138 | Regular(ifthenelse,seq) |
---|
139 | Regular(cost,seq) |
---|
140 | Regular(assign c,seq) |
---|
141 | Regular(skip,seq) |
---|
142 | Regular(cost,call) |
---|
143 | Regular(return,call) |
---|
144 | Return(Int(1),call) |
---|
145 | Regular(skip,seq) |
---|
146 | Regular(seq,stop) |
---|
147 | Regular(cost,seq) |
---|
148 | Regular(call,seq) |
---|
149 | Call(func,call) |
---|
150 | Regular(seq,call) |
---|
151 | Regular(cost,seq) |
---|
152 | Regular(assign c,seq) |
---|
153 | Regular(skip,seq) |
---|
154 | Regular(seq,call) |
---|
155 | Regular(cost,seq) |
---|
156 | Regular(assign d,seq) |
---|
157 | Regular(skip,seq) |
---|
158 | Regular(seq,call) |
---|
159 | Regular(cost,seq) |
---|
160 | Regular(assign v,seq) |
---|
161 | Regular(skip,seq) |
---|
162 | Regular(seq,call) |
---|
163 | Regular(cost,seq) |
---|
164 | Regular(assign w,seq) |
---|
165 | Regular(skip,seq) |
---|
166 | Regular(seq,call) |
---|
167 | Regular(cost,seq) |
---|
168 | Regular(assign z,seq) |
---|
169 | Regular(skip,seq) |
---|
170 | Regular(seq,call) |
---|
171 | Regular(cost,seq) |
---|
172 | Regular(ifthenelse,seq) |
---|
173 | Regular(cost,seq) |
---|
174 | Regular(assign c,seq) |
---|
175 | Regular(skip,seq) |
---|
176 | Regular(seq,call) |
---|
177 | Regular(cost,seq) |
---|
178 | Regular(ifthenelse,seq) |
---|
179 | Regular(seq,seq) |
---|
180 | Regular(cost,seq) |
---|
181 | Regular(assign z,seq) |
---|
182 | Regular(skip,seq) |
---|
183 | Regular(cost,seq) |
---|
184 | Regular(assign w,seq) |
---|
185 | Regular(skip,seq) |
---|
186 | Regular(seq,call) |
---|
187 | Regular(cost,seq) |
---|
188 | Regular(assign d,seq) |
---|
189 | Regular(skip,seq) |
---|
190 | Regular(seq,call) |
---|
191 | Regular(cost,seq) |
---|
192 | Regular(assign v,seq) |
---|
193 | Regular(skip,seq) |
---|
194 | Regular(cost,call) |
---|
195 | Regular(return,call) |
---|
196 | Return(Int(3),call) |
---|
197 | Regular(skip,seq) |
---|
198 | Regular(seq,stop) |
---|
199 | Regular(cost,seq) |
---|
200 | Regular(call,seq) |
---|
201 | Call(func,call) |
---|
202 | Regular(seq,call) |
---|
203 | Regular(cost,seq) |
---|
204 | Regular(ifthenelse,seq) |
---|
205 | Regular(cost,seq) |
---|
206 | Regular(ifthenelse,seq) |
---|
207 | Regular(cost,seq) |
---|
208 | Regular(assign result,seq) |
---|
209 | Regular(skip,seq) |
---|
210 | Regular(cost,call) |
---|
211 | Regular(return,call) |
---|
212 | Return(Int(-1),call) |
---|
213 | Regular(skip,seq) |
---|
214 | Regular(cost,stop) |
---|
215 | Regular(return,stop) |
---|
216 | Result: Int(-1) |
---|
217 | Memory dump: |
---|
218 | n = 54 |
---|
219 | block 1 : Free. |
---|
220 | |
---|
221 | block 2 : Free. |
---|
222 | |
---|
223 | block 3 : Free. |
---|
224 | |
---|
225 | block 4 : Free. |
---|
226 | |
---|
227 | block 5 : Free. |
---|
228 | |
---|
229 | block 6 : Free. |
---|
230 | |
---|
231 | block 7 : Free. |
---|
232 | |
---|
233 | block 8 : Free. |
---|
234 | |
---|
235 | block 9 : Free. |
---|
236 | |
---|
237 | block 10 : Free. |
---|
238 | |
---|
239 | block 11 : Free. |
---|
240 | |
---|
241 | block 12 : Free. |
---|
242 | |
---|
243 | block 13 : Free. |
---|
244 | |
---|
245 | block 14 : Free. |
---|
246 | |
---|
247 | block 15 : Free. |
---|
248 | |
---|
249 | block 16 : Free. |
---|
250 | |
---|
251 | block 17 : Free. |
---|
252 | |
---|
253 | block 18 : Free. |
---|
254 | |
---|
255 | block 19 : Free. |
---|
256 | |
---|
257 | block 20 : Free. |
---|
258 | |
---|
259 | block 21 : Free. |
---|
260 | |
---|
261 | block 22 : Free. |
---|
262 | |
---|
263 | block 23 : Free. |
---|
264 | |
---|
265 | block 24 : Free. |
---|
266 | |
---|
267 | block 25 : Free. |
---|
268 | |
---|
269 | block 26 : Free. |
---|
270 | |
---|
271 | block 27 : Free. |
---|
272 | |
---|
273 | block 28 : Free. |
---|
274 | |
---|
275 | block 29 : Free. |
---|
276 | |
---|
277 | block 30 : Free. |
---|
278 | |
---|
279 | block 31 : Free. |
---|
280 | |
---|
281 | block 32 : Free. |
---|
282 | |
---|
283 | block 33 : Free. |
---|
284 | |
---|
285 | block 34 : Free. |
---|
286 | |
---|
287 | block 35 : Free. |
---|
288 | |
---|
289 | block 36 : Free. |
---|
290 | |
---|
291 | block 37 : Free. |
---|
292 | |
---|
293 | block 38 : Free. |
---|
294 | |
---|
295 | block 39 : Free. |
---|
296 | |
---|
297 | block 40 : Free. |
---|
298 | |
---|
299 | block 41 : Free. |
---|
300 | |
---|
301 | block 42 : Free. |
---|
302 | |
---|
303 | block 43 : Free. |
---|
304 | |
---|
305 | block 44 : Free. |
---|
306 | |
---|
307 | block 45 : Free. |
---|
308 | |
---|
309 | block 46 : Free. |
---|
310 | |
---|
311 | block 47 : Free. |
---|
312 | |
---|
313 | block 48 : Free. |
---|
314 | |
---|
315 | block 49 : Free. |
---|
316 | |
---|
317 | block 50 : Free. |
---|
318 | |
---|
319 | block 51 : Free. |
---|
320 | |
---|
321 | block 52 : Free. |
---|
322 | |
---|
323 | block 53 : Free. |
---|
324 | |
---|
325 | State_call { function() - stop } |
---|
326 | State_regular { seq - stop } |
---|
327 | State_regular { cost - seq::cont } |
---|
328 | State_regular { call - seq::cont } |
---|
329 | State_call { function(Int(1),Int(2),Int(3),Int(4),Int(5),Int(6),Int(7),Int(8),Int(9)) - returnto } |
---|
330 | State_regular { seq - returnto } |
---|
331 | State_regular { cost - seq::cont } |
---|
332 | State_regular { assign - seq::cont } |
---|
333 | State_regular { skip - seq::cont } |
---|
334 | State_regular { seq - returnto } |
---|
335 | State_regular { cost - seq::cont } |
---|
336 | State_regular { assign - seq::cont } |
---|
337 | State_regular { skip - seq::cont } |
---|
338 | State_regular { seq - returnto } |
---|
339 | State_regular { cost - seq::cont } |
---|
340 | State_regular { assign - seq::cont } |
---|
341 | State_regular { skip - seq::cont } |
---|
342 | State_regular { seq - returnto } |
---|
343 | State_regular { cost - cost::cont } |
---|
344 | State_regular { ifthenelse - cost::cont } |
---|
345 | State_regular { seq - cost::cont } |
---|
346 | State_regular { cost - seq::cont } |
---|
347 | State_regular { assign - seq::cont } |
---|
348 | State_regular { skip - seq::cont } |
---|
349 | State_regular { seq - cost::cont } |
---|
350 | State_regular { cost - cost::cont } |
---|
351 | State_regular { assign - cost::cont } |
---|
352 | State_regular { skip - cost::cont } |
---|
353 | State_regular { cost - cost::cont } |
---|
354 | State_regular { assign - cost::cont } |
---|
355 | State_regular { skip - cost::cont } |
---|
356 | State_regular { cost - returnto } |
---|
357 | State_regular { return - returnto } |
---|
358 | State_return { Int(22) - returnto } |
---|
359 | State_regular { skip - seq::cont } |
---|
360 | State_regular { seq - stop } |
---|
361 | State_regular { cost - seq::cont } |
---|
362 | State_regular { call - seq::cont } |
---|
363 | State_call { function(Int(1),Int(2)) - returnto } |
---|
364 | State_regular { seq - returnto } |
---|
365 | State_regular { cost - cost::cont } |
---|
366 | State_regular { ifthenelse - cost::cont } |
---|
367 | State_regular { seq - cost::cont } |
---|
368 | State_regular { cost - seq::cont } |
---|
369 | State_regular { assign - seq::cont } |
---|
370 | State_regular { skip - seq::cont } |
---|
371 | State_regular { seq - cost::cont } |
---|
372 | State_regular { cost - cost::cont } |
---|
373 | State_regular { assign - cost::cont } |
---|
374 | State_regular { skip - cost::cont } |
---|
375 | State_regular { cost - cost::cont } |
---|
376 | State_regular { assign - cost::cont } |
---|
377 | State_regular { skip - cost::cont } |
---|
378 | State_regular { cost - returnto } |
---|
379 | State_regular { return - returnto } |
---|
380 | State_return { Int(6) - returnto } |
---|
381 | State_regular { skip - seq::cont } |
---|
382 | State_regular { seq - stop } |
---|
383 | State_regular { cost - seq::cont } |
---|
384 | State_regular { call - seq::cont } |
---|
385 | State_call { function(Int(1),Int(2),Int(3)) - returnto } |
---|
386 | State_regular { seq - returnto } |
---|
387 | State_regular { cost - cost::cont } |
---|
388 | State_regular { ifthenelse - cost::cont } |
---|
389 | State_regular { cost - cost::cont } |
---|
390 | State_regular { ifthenelse - cost::cont } |
---|
391 | State_regular { cost - cost::cont } |
---|
392 | State_regular { assign - cost::cont } |
---|
393 | State_regular { skip - cost::cont } |
---|
394 | State_regular { cost - returnto } |
---|
395 | State_regular { return - returnto } |
---|
396 | State_return { Int(2) - returnto } |
---|
397 | State_regular { skip - seq::cont } |
---|
398 | State_regular { seq - stop } |
---|
399 | State_regular { cost - seq::cont } |
---|
400 | State_regular { call - seq::cont } |
---|
401 | State_call { function(Int(1),Int(2),Int(3)) - returnto } |
---|
402 | State_regular { seq - returnto } |
---|
403 | State_regular { cost - cost::cont } |
---|
404 | State_regular { ifthenelse - cost::cont } |
---|
405 | State_regular { cost - cost::cont } |
---|
406 | State_regular { ifthenelse - cost::cont } |
---|
407 | State_regular { cost - cost::cont } |
---|
408 | State_regular { assign - cost::cont } |
---|
409 | State_regular { skip - cost::cont } |
---|
410 | State_regular { cost - returnto } |
---|
411 | State_regular { return - returnto } |
---|
412 | State_return { Int(2) - returnto } |
---|
413 | State_regular { skip - seq::cont } |
---|
414 | State_regular { seq - stop } |
---|
415 | State_regular { cost - seq::cont } |
---|
416 | State_regular { call - seq::cont } |
---|
417 | State_call { function(Int(1),Int(2)) - returnto } |
---|
418 | State_regular { seq - returnto } |
---|
419 | State_regular { cost - cost::cont } |
---|
420 | State_regular { ifthenelse - cost::cont } |
---|
421 | State_regular { cost - cost::cont } |
---|
422 | State_regular { assign - cost::cont } |
---|
423 | State_regular { skip - cost::cont } |
---|
424 | State_regular { cost - returnto } |
---|
425 | State_regular { return - returnto } |
---|
426 | State_return { Int(1) - returnto } |
---|
427 | State_regular { skip - seq::cont } |
---|
428 | State_regular { seq - stop } |
---|
429 | State_regular { cost - seq::cont } |
---|
430 | State_regular { call - seq::cont } |
---|
431 | State_call { function(Int(1),Int(2)) - returnto } |
---|
432 | State_regular { seq - returnto } |
---|
433 | State_regular { cost - seq::cont } |
---|
434 | State_regular { assign - seq::cont } |
---|
435 | State_regular { skip - seq::cont } |
---|
436 | State_regular { seq - returnto } |
---|
437 | State_regular { cost - cost::cont } |
---|
438 | State_regular { ifthenelse - cost::cont } |
---|
439 | State_regular { cost - cost::cont } |
---|
440 | State_regular { assign - cost::cont } |
---|
441 | State_regular { skip - cost::cont } |
---|
442 | State_regular { cost - returnto } |
---|
443 | State_regular { return - returnto } |
---|
444 | State_return { Int(3) - returnto } |
---|
445 | State_regular { skip - seq::cont } |
---|
446 | State_regular { seq - stop } |
---|
447 | State_regular { cost - seq::cont } |
---|
448 | State_regular { call - seq::cont } |
---|
449 | State_call { function(Int(1),Int(2)) - returnto } |
---|
450 | State_regular { seq - returnto } |
---|
451 | State_regular { cost - seq::cont } |
---|
452 | State_regular { assign - seq::cont } |
---|
453 | State_regular { skip - seq::cont } |
---|
454 | State_regular { seq - returnto } |
---|
455 | State_regular { cost - cost::cont } |
---|
456 | State_regular { ifthenelse - cost::cont } |
---|
457 | State_regular { cost - cost::cont } |
---|
458 | State_regular { assign - cost::cont } |
---|
459 | State_regular { skip - cost::cont } |
---|
460 | State_regular { cost - returnto } |
---|
461 | State_regular { return - returnto } |
---|
462 | State_return { Int(1) - returnto } |
---|
463 | State_regular { skip - seq::cont } |
---|
464 | State_regular { seq - stop } |
---|
465 | State_regular { cost - seq::cont } |
---|
466 | State_regular { call - seq::cont } |
---|
467 | State_call { function(Int(1),Int(2),Int(3),Int(4)) - returnto } |
---|
468 | State_regular { seq - returnto } |
---|
469 | State_regular { cost - seq::cont } |
---|
470 | State_regular { assign - seq::cont } |
---|
471 | State_regular { skip - seq::cont } |
---|
472 | State_regular { seq - returnto } |
---|
473 | State_regular { cost - seq::cont } |
---|
474 | State_regular { assign - seq::cont } |
---|
475 | State_regular { skip - seq::cont } |
---|
476 | State_regular { seq - returnto } |
---|
477 | State_regular { cost - seq::cont } |
---|
478 | State_regular { assign - seq::cont } |
---|
479 | State_regular { skip - seq::cont } |
---|
480 | State_regular { seq - returnto } |
---|
481 | State_regular { cost - seq::cont } |
---|
482 | State_regular { assign - seq::cont } |
---|
483 | State_regular { skip - seq::cont } |
---|
484 | State_regular { seq - returnto } |
---|
485 | State_regular { cost - seq::cont } |
---|
486 | State_regular { assign - seq::cont } |
---|
487 | State_regular { skip - seq::cont } |
---|
488 | State_regular { seq - returnto } |
---|
489 | State_regular { cost - seq::cont } |
---|
490 | State_regular { ifthenelse - seq::cont } |
---|
491 | State_regular { cost - seq::cont } |
---|
492 | State_regular { assign - seq::cont } |
---|
493 | State_regular { skip - seq::cont } |
---|
494 | State_regular { seq - returnto } |
---|
495 | State_regular { cost - seq::cont } |
---|
496 | State_regular { ifthenelse - seq::cont } |
---|
497 | State_regular { seq - seq::cont } |
---|
498 | State_regular { cost - cost::cont } |
---|
499 | State_regular { assign - cost::cont } |
---|
500 | State_regular { skip - cost::cont } |
---|
501 | State_regular { cost - seq::cont } |
---|
502 | State_regular { assign - seq::cont } |
---|
503 | State_regular { skip - seq::cont } |
---|
504 | State_regular { seq - returnto } |
---|
505 | State_regular { cost - seq::cont } |
---|
506 | State_regular { assign - seq::cont } |
---|
507 | State_regular { skip - seq::cont } |
---|
508 | State_regular { seq - returnto } |
---|
509 | State_regular { cost - cost::cont } |
---|
510 | State_regular { assign - cost::cont } |
---|
511 | State_regular { skip - cost::cont } |
---|
512 | State_regular { cost - returnto } |
---|
513 | State_regular { return - returnto } |
---|
514 | State_return { Int(3) - returnto } |
---|
515 | State_regular { skip - seq::cont } |
---|
516 | State_regular { seq - stop } |
---|
517 | State_regular { cost - cost::cont } |
---|
518 | State_regular { call - cost::cont } |
---|
519 | State_call { function(Int(1),Int(2),Int(3)) - returnto } |
---|
520 | State_regular { seq - returnto } |
---|
521 | State_regular { cost - cost::cont } |
---|
522 | State_regular { ifthenelse - cost::cont } |
---|
523 | State_regular { cost - cost::cont } |
---|
524 | State_regular { ifthenelse - cost::cont } |
---|
525 | State_regular { cost - cost::cont } |
---|
526 | State_regular { assign - cost::cont } |
---|
527 | State_regular { skip - cost::cont } |
---|
528 | State_regular { cost - returnto } |
---|
529 | State_regular { return - returnto } |
---|
530 | State_return { Int(-1) - returnto } |
---|
531 | State_regular { skip - cost::cont } |
---|
532 | State_regular { cost - stop } |
---|
533 | State_regular { return - stop } |
---|
534 | Result: Int(-1) |
---|
535 | Memory dump: |
---|
536 | n = 11 |
---|
537 | block 1 : Free. |
---|
538 | |
---|
539 | block 2 : Free. |
---|
540 | |
---|
541 | block 3 : Free. |
---|
542 | |
---|
543 | block 4 : Free. |
---|
544 | |
---|
545 | block 5 : Free. |
---|
546 | |
---|
547 | block 6 : Free. |
---|
548 | |
---|
549 | block 7 : Free. |
---|
550 | |
---|
551 | block 8 : Free. |
---|
552 | |
---|
553 | block 9 : Free. |
---|
554 | |
---|
555 | block 10 : Free. |
---|
556 | |
---|