tests/clight/ifthenelse.log.expected

   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