[ 0:01] compiling /home/xrockai/src/divine/nightly/test/svcomp/systemc/toy2_false.cil.c [ 0:01] compiling /dios/lib/config/seqklee.bc [ 0:01] setting up pass: functionmeta, options = [ 0:02] setting up pass: fuse-ctors, options = [ 0:02] KLEE: output directory is "/var/obj/divine-nightly/semidbg/test/__test_work_dir.0/_klee_out" [ 0:04] KLEE: Using Z3 solver backend [ 0:04] WARNING: this target does not support the llvm.stacksave intrinsic. [ 0:04] warning: Linking two modules of different target triples: klee_div_zero_check.bc' is 'x86_64-unknown-linux-gnu' whereas 'klee.bc' is 'x86_64-unknown-none-elf' [ 0:04] [ 0:04] KLEE: WARNING: undefined reference to function: __dios_tainted_init [ 0:07] KLEE: WARNING: undefined reference to function: klee_free [ 0:07] KLEE: WARNING: undefined reference to function: klee_malloc [ 0:07] i:1 [ 0:07] KLEE: WARNING ONCE: Alignment of memory from call "klee_malloc" is not modelled. Using alignment of 8. [ 0:07] about to __boot:0 [ 0:07] about to run the scheduler:0 [ 0:07] KLEE: WARNING ONCE: calling external: __dios_tainted_init() at /dios/libc/sys/start.cpp:49 5 [ 0:07] KLEE: ERROR: /dios/libc/sys/start.cpp:87: failed external call: __dios_tainted_init [ 0:07] KLEE: NOTE: now ignoring this error at this location [ 0:07] KLEE: ERROR: EXITING ON ERROR: [ 0:07] Error: failed external call: __dios_tainted_init [ 0:07] File: /dios/libc/sys/start.cpp [ 0:07] Line: 87 [ 0:07] assembly.ll line: 35429 [ 0:07] Stack: [ 0:07] #000035429 in __dios_start (l=0, argc=1, argv=94715319243272, envp=94715319304200) at /dios/libc/sys/start.cpp:87 [ 0:07] #100011448 in _ZN6__dios10sched_nullINS_5ClockINS_10NondetKleeINS_4BaseEEEEEE13run_schedulerINS_7ContextEEEvv () at /dios/sys/sched_null.hpp:163 [ 0:07] #200043779 in klee_boot (argc=2, argv=94715293702144) at /dios/arch/klee/boot.c:41 [ 0:07] [ 0:07] [ 0:07] 1 /* TAGS: error c sym */ [ 0:07] 2 /* VERIFY_OPTS: --symbolic --sequential -o nofail:malloc */ [ 0:07] 3 extern void __VERIFIER_error() __attribute__ ((__noreturn__)); [ 0:07] 4 [ 0:07] 5 extern int __VERIFIER_nondet_int(); [ 0:07] 6 /* Generated by CIL v. 1.3.6 */ [ 0:07] 7 /* print_CIL_Input is true */ [ 0:07] 8 [ 0:07] 9 [ 0:07] 10 [ 0:07] 11 void error(void) [ 0:07] 12 { [ 0:07] 13 [ 0:07] 14 { [ 0:07] 15 ERROR: __VERIFIER_error(); /* ERROR */ [ 0:07] 16 return; [ 0:07] 17 } [ 0:07] 18 } [ 0:07] 19 [ 0:07] 20 int c ; [ 0:07] 21 int c_t ; [ 0:07] 22 int c_req_up ; [ 0:07] 23 int p_in ; [ 0:07] 24 int p_out ; [ 0:07] 25 int wl_st ; [ 0:07] 26 int c1_st ; [ 0:07] 27 int c2_st ; [ 0:07] 28 int wb_st ; [ 0:07] 29 int r_st ; [ 0:07] 30 int wl_i ; [ 0:07] 31 int c1_i ; [ 0:07] 32 int c2_i ; [ 0:07] 33 int wb_i ; [ 0:07] 34 int r_i ; [ 0:07] 35 int wl_pc ; [ 0:07] 36 int c1_pc ; [ 0:07] 37 int c2_pc ; [ 0:07] 38 int wb_pc ; [ 0:07] 39 int e_e ; [ 0:07] 40 int e_f ; [ 0:07] 41 int e_g ; [ 0:07] 42 int e_c ; [ 0:07] 43 int e_p_in ; [ 0:07] 44 int e_wl ; [ 0:07] 45 void write_loop(void) ; [ 0:07] 46 void compute1(void) ; [ 0:07] 47 void compute2(void) ; [ 0:07] 48 void write_back(void) ; [ 0:07] 49 void read(void) ; [ 0:07] 50 int d ; [ 0:07] 51 int data ; [ 0:07] 52 int processed ; [ 0:07] 53 static int t_b ; [ 0:07] 54 void write_loop(void) [ 0:07] 55 { int t ; [ 0:07] 56 [ 0:07] 57 { [ 0:07] 58 if ((int )wl_pc == 0) { [ 0:07] 59 goto WL_ENTRY_LOC; [ 0:07] 60 } else { [ 0:07] 61 if ((int )wl_pc == 2) { [ 0:07] 62 goto WL_WAIT_2_LOC; [ 0:07] 63 } else { [ 0:07] 64 if ((int )wl_pc == 1) { [ 0:07] 65 goto WL_WAIT_1_LOC; [ 0:07] 66 } else { [ 0:07] 67 [ 0:07] 68 } [ 0:07] 69 } [ 0:07] 70 } [ 0:07] 71 WL_ENTRY_LOC: [ 0:07] 72 wl_st = 2; [ 0:07] 73 wl_pc = 1; [ 0:07] 74 e_wl = 0; [ 0:07] 75 [ 0:07] 76 goto return_label; [ 0:07] 77 WL_WAIT_1_LOC: [ 0:07] 78 { [ 0:07] 79 while (1) { [ 0:07] 80 while_0_continue: /* CIL Label */ ; [ 0:07] 81 t = d; [ 0:07] 82 data = d; [ 0:07] 83 processed = 0; [ 0:07] 84 e_f = 1; [ 0:07] 85 if ((int )c1_pc == 1) { [ 0:07] 86 if ((int )e_f == 1) { [ 0:07] 87 c1_st = 0; [ 0:07] 88 } else { [ 0:07] 89 [ 0:07] 90 } [ 0:07] 91 } else { [ 0:07] 92 [ 0:07] 93 } [ 0:07] 94 if ((int )c2_pc == 1) { [ 0:07] 95 if ((int )e_f == 1) { [ 0:07] 96 c2_st = 0; [ 0:07] 97 } else { [ 0:07] 98 [ 0:07] 99 } [ 0:07] 100 } else { [ 0:07] 101 [ 0:07] 102 } [ 0:07] 103 e_f = 2; [ 0:07] 104 wl_st = 2; [ 0:07] 105 wl_pc = 2; [ 0:07] 106 t_b = t; [ 0:07] 107 [ 0:07] 108 goto return_label; [ 0:07] 109 WL_WAIT_2_LOC: [ 0:07] 110 t = t_b; [ 0:07] 111 if (d == t + 1) { [ 0:07] 112 [ 0:07] 113 } else { [ 0:07] 114 { [ 0:07] 115 error(); [ 0:07] 116 } [ 0:07] 117 } [ 0:07] 118 } [ 0:07] 119 while_0_break: /* CIL Label */ ; [ 0:07] 120 } [ 0:07] 121 return_label: /* CIL Label */ [ 0:07] 122 return; [ 0:07] 123 } [ 0:07] 124 } [ 0:07] 125 void compute1(void) [ 0:07] 126 { [ 0:07] 127 [ 0:07] 128 { [ 0:07] 129 if ((int )c1_pc == 0) { [ 0:07] 130 goto C1_ENTRY_LOC; [ 0:07] 131 } else { [ 0:07] 132 if ((int )c1_pc == 1) { [ 0:07] 133 goto C1_WAIT_LOC; [ 0:07] 134 } else { [ 0:07] 135 [ 0:07] 136 } [ 0:07] 137 } [ 0:07] 138 C1_ENTRY_LOC: [ 0:07] 139 { [ 0:07] 140 while (1) { [ 0:07] 141 while_1_continue: /* CIL Label */ ; [ 0:07] 142 c1_st = 2; [ 0:07] 143 c1_pc = 1; [ 0:07] 144 [ 0:07] 145 goto return_label; [ 0:07] 146 C1_WAIT_LOC: [ 0:07] 147 if (! processed) { [ 0:07] 148 data += 1; [ 0:07] 149 e_g = 1; [ 0:07] 150 if ((int )wb_pc == 1) { [ 0:07] 151 if ((int )e_g == 1) { [ 0:07] 152 wb_st = 0; [ 0:07] 153 } else { [ 0:07] 154 [ 0:07] 155 } [ 0:07] 156 } else { [ 0:07] 157 [ 0:07] 158 } [ 0:07] 159 e_g = 2; [ 0:07] 160 } else { [ 0:07] 161 [ 0:07] 162 } [ 0:07] 163 } [ 0:07] 164 while_1_break: /* CIL Label */ ; [ 0:07] 165 } [ 0:07] 166 return_label: /* CIL Label */ [ 0:07] 167 return; [ 0:07] 168 } [ 0:07] 169 } [ 0:07] 170 void compute2(void) [ 0:07] 171 { [ 0:07] 172 [ 0:07] 173 { [ 0:07] 174 if ((int )c2_pc == 0) { [ 0:07] 175 goto C2_ENTRY_LOC; [ 0:07] 176 } else { [ 0:07] 177 if ((int )c2_pc == 1) { [ 0:07] 178 goto C2_WAIT_LOC; [ 0:07] 179 } else { [ 0:07] 180 [ 0:07] 181 } [ 0:07] 182 } [ 0:07] 183 C2_ENTRY_LOC: [ 0:07] 184 { [ 0:07] 185 while (1) { [ 0:07] 186 while_2_continue: /* CIL Label */ ; [ 0:07] 187 c2_st = 2; [ 0:07] 188 c2_pc = 1; [ 0:07] 189 [ 0:07] 190 goto return_label; [ 0:07] 191 C2_WAIT_LOC: [ 0:07] 192 if (! processed) { [ 0:07] 193 data += 1; [ 0:07] 194 e_g = 1; [ 0:07] 195 if ((int )wb_pc == 1) { [ 0:07] 196 if ((int )e_g == 1) { [ 0:07] 197 wb_st = 0; [ 0:07] 198 } else { [ 0:07] 199 [ 0:07] 200 } [ 0:07] 201 } else { [ 0:07] 202 [ 0:07] 203 } [ 0:07] 204 e_g = 2; [ 0:07] 205 } else { [ 0:07] 206 [ 0:07] 207 } [ 0:07] 208 } [ 0:07] 209 while_2_break: /* CIL Label */ ; [ 0:07] 210 } [ 0:07] 211 return_label: /* CIL Label */ [ 0:07] 212 return; [ 0:07] 213 } [ 0:07] 214 } [ 0:07] 215 void write_back(void) [ 0:07] 216 { [ 0:07] 217 [ 0:07] 218 { [ 0:07] 219 if ((int )wb_pc == 0) { [ 0:07] 220 goto WB_ENTRY_LOC; [ 0:07] 221 } else { [ 0:07] 222 if ((int )wb_pc == 1) { [ 0:07] 223 goto WB_WAIT_LOC; [ 0:07] 224 } else { [ 0:07] 225 [ 0:07] 226 } [ 0:07] 227 } [ 0:07] 228 WB_ENTRY_LOC: [ 0:07] 229 { [ 0:07] 230 while (1) { [ 0:07] 231 while_3_continue: /* CIL Label */ ; [ 0:07] 232 wb_st = 2; [ 0:07] 233 wb_pc = 1; [ 0:07] 234 [ 0:07] 235 goto return_label; [ 0:07] 236 WB_WAIT_LOC: [ 0:07] 237 c_t = data; [ 0:07] 238 c_req_up = 1; [ 0:07] 239 processed = 1; [ 0:07] 240 } [ 0:07] 241 while_3_break: /* CIL Label */ ; [ 0:07] 242 } [ 0:07] 243 return_label: /* CIL Label */ [ 0:07] 244 return; [ 0:07] 245 } [ 0:07] 246 } [ 0:07] 247 void read(void) [ 0:07] 248 { [ 0:07] 249 [ 0:07] 250 { [ 0:07] 251 d = c; [ 0:07] 252 e_e = 1; [ 0:07] 253 if ((int )wl_pc == 1) { [ 0:07] 254 if ((int )e_wl == 1) { [ 0:07] 255 wl_st = 0; [ 0:07] 256 } else { [ 0:07] 257 goto _L; [ 0:07] 258 } [ 0:07] 259 } else { [ 0:07] 260 _L: /* CIL Label */ [ 0:07] 261 if ((int )wl_pc == 2) { [ 0:07] 262 if ((int )e_e == 1) { [ 0:07] 263 wl_st = 0; [ 0:07] 264 } else { [ 0:07] 265 [ 0:07] 266 } [ 0:07] 267 } else { [ 0:07] 268 [ 0:07] 269 } [ 0:07] 270 } [ 0:07] 271 e_e = 2; [ 0:07] 272 r_st = 2; [ 0:07] 273 [ 0:07] 274 return; [ 0:07] 275 } [ 0:07] 276 } [ 0:07] 277 void eval(void) [ 0:07] 278 { int tmp ; [ 0:07] 279 int tmp___0 ; [ 0:07] 280 int tmp___1 ; [ 0:07] 281 int tmp___2 ; [ 0:07] 282 int tmp___3 ; [ 0:07] 283 [ 0:07] 284 { [ 0:07] 285 { [ 0:07] 286 while (1) { [ 0:07] 287 while_4_continue: /* CIL Label */ ; [ 0:07] 288 if ((int )wl_st == 0) { [ 0:07] 289 [ 0:07] 290 } else { [ 0:07] 291 if ((int )c1_st == 0) { [ 0:07] 292 [ 0:07] 293 } else { [ 0:07] 294 if ((int )c2_st == 0) { [ 0:07] 295 [ 0:07] 296 } else { [ 0:07] 297 if ((int )wb_st == 0) { [ 0:07] 298 [ 0:07] 299 } else { [ 0:07] 300 if ((int )r_st == 0) { [ 0:07] 301 [ 0:07] 302 } else { [ 0:07] 303 goto while_4_break; [ 0:07] 304 } [ 0:07] 305 } [ 0:07] 306 } [ 0:07] 307 } [ 0:07] 308 } [ 0:07] 309 if ((int )wl_st == 0) { [ 0:07] 310 { [ 0:07] 311 tmp = __VERIFIER_nondet_int(); [ 0:07] 312 } [ 0:07] 313 if (tmp) { [ 0:07] 314 { [ 0:07] 315 wl_st = 1; [ 0:07] 316 write_loop(); [ 0:07] 317 } [ 0:07] 318 } else { [ 0:07] 319 [ 0:07] 320 } [ 0:07] 321 } else { [ 0:07] 322 [ 0:07] 323 } [ 0:07] 324 if ((int )c1_st == 0) { [ 0:07] 325 { [ 0:07] 326 tmp___0 = __VERIFIER_nondet_int(); [ 0:07] 327 } [ 0:07] 328 if (tmp___0) { [ 0:07] 329 { [ 0:07] 330 c1_st = 1; [ 0:07] 331 compute1(); [ 0:07] 332 } [ 0:07] 333 } else { [ 0:07] 334 [ 0:07] 335 } [ 0:07] 336 } else { [ 0:07] 337 [ 0:07] 338 } [ 0:07] 339 if ((int )c2_st == 0) { [ 0:07] 340 { [ 0:07] 341 tmp___1 = __VERIFIER_nondet_int(); [ 0:07] 342 } [ 0:07] 343 if (tmp___1) { [ 0:07] 344 { [ 0:07] 345 c2_st = 1; [ 0:07] 346 compute2(); [ 0:07] 347 } [ 0:07] 348 } else { [ 0:07] 349 [ 0:07] 350 } [ 0:07] 351 } else { [ 0:07] 352 [ 0:07] 353 } [ 0:07] 354 if ((int )wb_st == 0) { [ 0:07] 355 { [ 0:07] 356 tmp___2 = __VERIFIER_nondet_int(); [ 0:07] 357 } [ 0:07] 358 if (tmp___2) { [ 0:07] 359 { [ 0:07] 360 wb_st = 1; [ 0:07] 361 write_back(); [ 0:07] 362 } [ 0:07] 363 } else { [ 0:07] 364 [ 0:07] 365 } [ 0:07] 366 } else { [ 0:07] 367 [ 0:07] 368 } [ 0:07] 369 if ((int )r_st == 0) { [ 0:07] 370 { [ 0:07] 371 tmp___3 = __VERIFIER_nondet_int(); [ 0:07] 372 } [ 0:07] 373 if (tmp___3) { [ 0:07] 374 { [ 0:07] 375 r_st = 1; [ 0:07] 376 read(); [ 0:07] 377 } [ 0:07] 378 } else { [ 0:07] 379 [ 0:07] 380 } [ 0:07] 381 } else { [ 0:07] 382 [ 0:07] 383 } [ 0:07] 384 } [ 0:07] 385 while_4_break: /* CIL Label */ ; [ 0:07] 386 } [ 0:07] 387 [ 0:07] 388 return; [ 0:07] 389 } [ 0:07] 390 } [ 0:07] 391 void start_simulation(void) [ 0:07] 392 { int kernel_st ; [ 0:07] 393 [ 0:07] 394 { [ 0:07] 395 kernel_st = 0; [ 0:07] 396 if ((int )c_req_up == 1) { [ 0:07] 397 if (c != c_t) { [ 0:07] 398 c = c_t; [ 0:07] 399 e_c = 0; [ 0:07] 400 } else { [ 0:07] 401 [ 0:07] 402 } [ 0:07] 403 c_req_up = 0; [ 0:07] 404 } else { [ 0:07] 405 [ 0:07] 406 } [ 0:07] 407 if ((int )wl_i == 1) { [ 0:07] 408 wl_st = 0; [ 0:07] 409 } else { [ 0:07] 410 wl_st = 2; [ 0:07] 411 } [ 0:07] 412 if ((int )c1_i == 1) { [ 0:07] 413 c1_st = 0; [ 0:07] 414 } else { [ 0:07] 415 c1_st = 2; [ 0:07] 416 } [ 0:07] 417 if ((int )c2_i == 1) { [ 0:07] 418 c2_st = 0; [ 0:07] 419 } else { [ 0:07] 420 c2_st = 2; [ 0:07] 421 } [ 0:07] 422 if ((int )wb_i == 1) { [ 0:07] 423 wb_st = 0; [ 0:07] 424 } else { [ 0:07] 425 wb_st = 2; [ 0:07] 426 } [ 0:07] 427 if ((int )r_i == 1) { [ 0:07] 428 r_st = 0; [ 0:07] 429 } else { [ 0:07] 430 r_st = 2; [ 0:07] 431 } [ 0:07] 432 if ((int )e_f == 0) { [ 0:07] 433 e_f = 1; [ 0:07] 434 } else { [ 0:07] 435 [ 0:07] 436 } [ 0:07] 437 if ((int )e_g == 0) { [ 0:07] 438 e_g = 1; [ 0:07] 439 } else { [ 0:07] 440 [ 0:07] 441 } [ 0:07] 442 if ((int )e_e == 0) { [ 0:07] 443 e_e = 1; [ 0:07] 444 } else { [ 0:07] 445 [ 0:07] 446 } [ 0:07] 447 if ((int )e_c == 0) { [ 0:07] 448 e_c = 1; [ 0:07] 449 } else { [ 0:07] 450 [ 0:07] 451 } [ 0:07] 452 if ((int )e_wl == 0) { [ 0:07] 453 e_wl = 1; [ 0:07] 454 } else { [ 0:07] 455 [ 0:07] 456 } [ 0:07] 457 if ((int )wl_pc == 1) { [ 0:07] 458 if ((int )e_wl == 1) { [ 0:07] 459 wl_st = 0; [ 0:07] 460 } else { [ 0:07] 461 goto _L; [ 0:07] 462 } [ 0:07] 463 } else { [ 0:07] 464 _L: /* CIL Label */ [ 0:07] 465 if ((int )wl_pc == 2) { [ 0:07] 466 if ((int )e_e == 1) { [ 0:07] 467 wl_st = 0; [ 0:07] 468 } else { [ 0:07] 469 [ 0:07] 470 } [ 0:07] 471 } else { [ 0:07] 472 [ 0:07] 473 } [ 0:07] 474 } [ 0:07] 475 if ((int )c1_pc == 1) { [ 0:07] 476 if ((int )e_f == 1) { [ 0:07] 477 c1_st = 0; [ 0:07] 478 } else { [ 0:07] 479 [ 0:07] 480 } [ 0:07] 481 } else { [ 0:07] 482 [ 0:07] 483 } [ 0:07] 484 if ((int )c2_pc == 1) { [ 0:07] 485 if ((int )e_f == 1) { [ 0:07] 486 c2_st = 0; [ 0:07] 487 } else { [ 0:07] 488 [ 0:07] 489 } [ 0:07] 490 } else { [ 0:07] 491 [ 0:07] 492 } [ 0:07] 493 if ((int )wb_pc == 1) { [ 0:07] 494 if ((int )e_g == 1) { [ 0:07] 495 wb_st = 0; [ 0:07] 496 } else { [ 0:07] 497 [ 0:07] 498 } [ 0:07] 499 } else { [ 0:07] 500 [ 0:07] 501 } [ 0:07] 502 if ((int )e_c == 1) { [ 0:07] 503 r_st = 0; [ 0:07] 504 } else { [ 0:07] 505 [ 0:07] 506 } [ 0:07] 507 if ((int )e_e == 1) { [ 0:07] 508 e_e = 2; [ 0:07] 509 } else { [ 0:07] 510 [ 0:07] 511 } [ 0:07] 512 if ((int )e_f == 1) { [ 0:07] 513 e_f = 2; [ 0:07] 514 } else { [ 0:07] 515 [ 0:07] 516 } [ 0:07] 517 if ((int )e_g == 1) { [ 0:07] 518 e_g = 2; [ 0:07] 519 } else { [ 0:07] 520 [ 0:07] 521 } [ 0:07] 522 if ((int )e_c == 1) { [ 0:07] 523 e_c = 2; [ 0:07] 524 } else { [ 0:07] 525 [ 0:07] 526 } [ 0:07] 527 if ((int )e_wl == 1) { [ 0:07] 528 e_wl = 2; [ 0:07] 529 } else { [ 0:07] 530 [ 0:07] 531 } [ 0:07] 532 { [ 0:07] 533 while (1) { [ 0:07] 534 while_5_continue: /* CIL Label */ ; [ 0:07] 535 { [ 0:07] 536 kernel_st = 1; [ 0:07] 537 eval(); [ 0:07] 538 } [ 0:07] 539 kernel_st = 2; [ 0:07] 540 if ((int )c_req_up == 1) { [ 0:07] 541 if (c != c_t) { [ 0:07] 542 c = c_t; [ 0:07] 543 e_c = 0; [ 0:07] 544 } else { [ 0:07] 545 [ 0:07] 546 } [ 0:07] 547 c_req_up = 0; [ 0:07] 548 } else { [ 0:07] 549 [ 0:07] 550 } [ 0:07] 551 kernel_st = 3; [ 0:07] 552 if ((int )e_f == 0) { [ 0:07] 553 e_f = 1; [ 0:07] 554 } else { [ 0:07] 555 [ 0:07] 556 } [ 0:07] 557 if ((int )e_g == 0) { [ 0:07] 558 e_g = 1; [ 0:07] 559 } else { [ 0:07] 560 [ 0:07] 561 } [ 0:07] 562 if ((int )e_e == 0) { [ 0:07] 563 e_e = 1; [ 0:07] 564 } else { [ 0:07] 565 [ 0:07] 566 } [ 0:07] 567 if ((int )e_c == 0) { [ 0:07] 568 e_c = 1; [ 0:07] 569 } else { [ 0:07] 570 [ 0:07] 571 } [ 0:07] 572 if ((int )e_wl == 0) { [ 0:07] 573 e_wl = 1; [ 0:07] 574 } else { [ 0:07] 575 [ 0:07] 576 } [ 0:07] 577 if ((int )wl_pc == 1) { [ 0:07] 578 if ((int )e_wl == 1) { [ 0:07] 579 wl_st = 0; [ 0:07] 580 } else { [ 0:07] 581 goto _L___0; [ 0:07] 582 } [ 0:07] 583 } else { [ 0:07] 584 _L___0: /* CIL Label */ [ 0:07] 585 if ((int )wl_pc == 2) { [ 0:07] 586 if ((int )e_e == 1) { [ 0:07] 587 wl_st = 0; [ 0:07] 588 } else { [ 0:07] 589 [ 0:07] 590 } [ 0:07] 591 } else { [ 0:07] 592 [ 0:07] 593 } [ 0:07] 594 } [ 0:07] 595 if ((int )c1_pc == 1) { [ 0:07] 596 if ((int )e_f == 1) { [ 0:07] 597 c1_st = 0; [ 0:07] 598 } else { [ 0:07] 599 [ 0:07] 600 } [ 0:07] 601 } else { [ 0:07] 602 [ 0:07] 603 } [ 0:07] 604 if ((int )c2_pc == 1) { [ 0:07] 605 if ((int )e_f == 1) { [ 0:07] 606 c2_st = 0; [ 0:07] 607 } else { [ 0:07] 608 [ 0:07] 609 } [ 0:07] 610 } else { [ 0:07] 611 [ 0:07] 612 } [ 0:07] 613 if ((int )wb_pc == 1) { [ 0:07] 614 if ((int )e_g == 1) { [ 0:07] 615 wb_st = 0; [ 0:07] 616 } else { [ 0:07] 617 [ 0:07] 618 } [ 0:07] 619 } else { [ 0:07] 620 [ 0:07] 621 } [ 0:07] 622 if ((int )e_c == 1) { [ 0:07] 623 r_st = 0; [ 0:07] 624 } else { [ 0:07] 625 [ 0:07] 626 } [ 0:07] 627 if ((int )e_e == 1) { [ 0:07] 628 e_e = 2; [ 0:07] 629 } else { [ 0:07] 630 [ 0:07] 631 } [ 0:07] 632 if ((int )e_f == 1) { [ 0:07] 633 e_f = 2; [ 0:07] 634 } else { [ 0:07] 635 [ 0:07] 636 } [ 0:07] 637 if ((int )e_g == 1) { [ 0:07] 638 e_g = 2; [ 0:07] 639 } else { [ 0:07] 640 [ 0:07] 641 } [ 0:07] 642 if ((int )e_c == 1) { [ 0:07] 643 e_c = 2; [ 0:07] 644 } else { [ 0:07] 645 [ 0:07] 646 } [ 0:07] 647 if ((int )e_wl == 1) { [ 0:07] 648 e_wl = 2; [ 0:07] 649 } else { [ 0:07] 650 [ 0:07] 651 } [ 0:07] 652 if ((int )wl_st == 0) { [ 0:07] 653 [ 0:07] 654 } else { [ 0:07] 655 if ((int )c1_st == 0) { [ 0:07] 656 [ 0:07] 657 } else { [ 0:07] 658 if ((int )c2_st == 0) { [ 0:07] 659 [ 0:07] 660 } else { [ 0:07] 661 if ((int )wb_st == 0) { [ 0:07] 662 [ 0:07] 663 } else { [ 0:07] 664 if ((int )r_st == 0) { [ 0:07] 665 [ 0:07] 666 } else { [ 0:07] 667 goto while_5_break; [ 0:07] 668 } [ 0:07] 669 } [ 0:07] 670 } [ 0:07] 671 } [ 0:07] 672 } [ 0:07] 673 } [ 0:07] 674 while_5_break: /* CIL Label */ ; [ 0:07] 675 } [ 0:07] 676 [ 0:07] 677 return; [ 0:07] 678 } [ 0:07] 679 } [ 0:07] 680 int main(void) [ 0:07] 681 { int __retres1 ; [ 0:07] 682 [ 0:07] 683 { [ 0:07] 684 { [ 0:07] 685 e_wl = 2; [ 0:07] 686 e_c = e_wl; [ 0:07] 687 e_g = e_c; [ 0:07] 688 e_f = e_g; [ 0:07] 689 e_e = e_f; [ 0:07] 690 wl_pc = 0; [ 0:07] 691 c1_pc = 0; [ 0:07] 692 c2_pc = 0; [ 0:07] 693 wb_pc = 0; [ 0:07] 694 wb_i = 1; [ 0:07] 695 c2_i = wb_i; [ 0:07] 696 c1_i = c2_i; [ 0:07] 697 wl_i = c1_i; [ 0:07] 698 r_i = 0; [ 0:07] 699 c_req_up = 0; [ 0:07] 700 d = 0; [ 0:07] 701 c = 0; [ 0:07] 702 start_simulation(); [ 0:07] 703 } [ 0:07] 704 __retres1 = 0; [ 0:07] 705 return (__retres1); [ 0:07] 706 } [ 0:07] 707 } [ 0:07] # expected error to be found at /home/xrockai/src/divine/nightly/test/svcomp/systemc/toy2_false.cil.c:15, but it was not