1 Warning (during instrumentation):
2 Clight instrumentation is not implemented yet.
3 Checking execution traces...OK.
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.
14 Regular(assign t1,seq)
18 Regular(assign t2,seq)
22 Regular(assign t3,seq)
26 Regular(ifthenelse,seq)
29 Regular(assign t4,seq)
33 Regular(assign t5,seq)
48 Regular(ifthenelse,seq)
70 Regular(ifthenelse,seq)
72 Regular(ifthenelse,seq)
74 Regular(assign result,seq)
86 Regular(ifthenelse,seq)
88 Regular(ifthenelse,seq)
90 Regular(assign result,seq)
102 Regular(ifthenelse,seq)
104 Regular(assign min,seq)
116 Regular(assign a,seq)
120 Regular(ifthenelse,seq)
122 Regular(assign b,seq)
134 Regular(assign c,seq)
138 Regular(ifthenelse,seq)
140 Regular(assign c,seq)
152 Regular(assign c,seq)
156 Regular(assign d,seq)
160 Regular(assign v,seq)
164 Regular(assign w,seq)
168 Regular(assign z,seq)
172 Regular(ifthenelse,seq)
174 Regular(assign c,seq)
178 Regular(ifthenelse,seq)
181 Regular(assign z,seq)
184 Regular(assign w,seq)
188 Regular(assign d,seq)
192 Regular(assign v,seq)
204 Regular(ifthenelse,seq)
206 Regular(ifthenelse,seq)
208 Regular(assign result,seq)
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 }