[ 0:01] compiling /home/xrockai/src/divine/nightly/test/svcomp/systemc/transmitter.01_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.20/_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: 34708 [ 0:07] Stack: [ 0:07] #000034708 in __dios_start (l=0, argc=1, argv=94087876465160, envp=94087876550664) at /dios/libc/sys/start.cpp:87 [ 0:07] #100010727 in _ZN6__dios10sched_nullINS_5ClockINS_10NondetKleeINS_4BaseEEEEEE13run_schedulerINS_7ContextEEEvv () at /dios/sys/sched_null.hpp:163 [ 0:07] #200043058 in klee_boot (argc=2, argv=94087849744384) 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 void error(void) [ 0:07] 10 { [ 0:07] 11 [ 0:07] 12 { [ 0:07] 13 ERROR: __VERIFIER_error(); /* ERROR */ [ 0:07] 14 return; [ 0:07] 15 } [ 0:07] 16 } [ 0:07] 17 int m_pc = 0; [ 0:07] 18 int t1_pc = 0; [ 0:07] 19 int m_st ; [ 0:07] 20 int t1_st ; [ 0:07] 21 int m_i ; [ 0:07] 22 int t1_i ; [ 0:07] 23 int M_E = 2; [ 0:07] 24 int T1_E = 2; [ 0:07] 25 int E_1 = 2; [ 0:07] 26 int is_master_triggered(void) ; [ 0:07] 27 int is_transmit1_triggered(void) ; [ 0:07] 28 void immediate_notify(void) ; [ 0:07] 29 void master(void) [ 0:07] 30 { [ 0:07] 31 [ 0:07] 32 { [ 0:07] 33 if (m_pc == 0) { [ 0:07] 34 goto M_ENTRY; [ 0:07] 35 } else { [ 0:07] 36 if (m_pc == 1) { [ 0:07] 37 goto M_WAIT; [ 0:07] 38 } else { [ 0:07] 39 [ 0:07] 40 } [ 0:07] 41 } [ 0:07] 42 M_ENTRY: ; [ 0:07] 43 { [ 0:07] 44 while (1) { [ 0:07] 45 while_0_continue: /* CIL Label */ ; [ 0:07] 46 { [ 0:07] 47 E_1 = 1; [ 0:07] 48 immediate_notify(); [ 0:07] 49 E_1 = 2; [ 0:07] 50 } [ 0:07] 51 { [ 0:07] 52 while (1) { [ 0:07] 53 while_1_continue: /* CIL Label */ ; [ 0:07] 54 m_pc = 1; [ 0:07] 55 m_st = 2; [ 0:07] 56 [ 0:07] 57 goto return_label; [ 0:07] 58 M_WAIT: ; [ 0:07] 59 } [ 0:07] 60 while_1_break: /* CIL Label */ ; [ 0:07] 61 } [ 0:07] 62 } [ 0:07] 63 while_0_break: /* CIL Label */ ; [ 0:07] 64 } [ 0:07] 65 [ 0:07] 66 return_label: /* CIL Label */ [ 0:07] 67 return; [ 0:07] 68 } [ 0:07] 69 } [ 0:07] 70 void transmit1(void) [ 0:07] 71 { [ 0:07] 72 [ 0:07] 73 { [ 0:07] 74 if (t1_pc == 0) { [ 0:07] 75 goto T1_ENTRY; [ 0:07] 76 } else { [ 0:07] 77 if (t1_pc == 1) { [ 0:07] 78 goto T1_WAIT; [ 0:07] 79 } else { [ 0:07] 80 [ 0:07] 81 } [ 0:07] 82 } [ 0:07] 83 T1_ENTRY: ; [ 0:07] 84 { [ 0:07] 85 while (1) { [ 0:07] 86 while_2_continue: /* CIL Label */ ; [ 0:07] 87 t1_pc = 1; [ 0:07] 88 t1_st = 2; [ 0:07] 89 [ 0:07] 90 goto return_label; [ 0:07] 91 T1_WAIT: [ 0:07] 92 { [ 0:07] 93 error(); [ 0:07] 94 } [ 0:07] 95 } [ 0:07] 96 while_2_break: /* CIL Label */ ; [ 0:07] 97 } [ 0:07] 98 [ 0:07] 99 return_label: /* CIL Label */ [ 0:07] 100 return; [ 0:07] 101 } [ 0:07] 102 } [ 0:07] 103 int is_master_triggered(void) [ 0:07] 104 { int __retres1 ; [ 0:07] 105 [ 0:07] 106 { [ 0:07] 107 if (m_pc == 1) { [ 0:07] 108 if (M_E == 1) { [ 0:07] 109 __retres1 = 1; [ 0:07] 110 goto return_label; [ 0:07] 111 } else { [ 0:07] 112 [ 0:07] 113 } [ 0:07] 114 } else { [ 0:07] 115 [ 0:07] 116 } [ 0:07] 117 __retres1 = 0; [ 0:07] 118 return_label: /* CIL Label */ [ 0:07] 119 return (__retres1); [ 0:07] 120 } [ 0:07] 121 } [ 0:07] 122 int is_transmit1_triggered(void) [ 0:07] 123 { int __retres1 ; [ 0:07] 124 [ 0:07] 125 { [ 0:07] 126 if (t1_pc == 1) { [ 0:07] 127 if (E_1 == 1) { [ 0:07] 128 __retres1 = 1; [ 0:07] 129 goto return_label; [ 0:07] 130 } else { [ 0:07] 131 [ 0:07] 132 } [ 0:07] 133 } else { [ 0:07] 134 [ 0:07] 135 } [ 0:07] 136 __retres1 = 0; [ 0:07] 137 return_label: /* CIL Label */ [ 0:07] 138 return (__retres1); [ 0:07] 139 } [ 0:07] 140 } [ 0:07] 141 void update_channels(void) [ 0:07] 142 { [ 0:07] 143 [ 0:07] 144 { [ 0:07] 145 [ 0:07] 146 return; [ 0:07] 147 } [ 0:07] 148 } [ 0:07] 149 void init_threads(void) [ 0:07] 150 { [ 0:07] 151 [ 0:07] 152 { [ 0:07] 153 if (m_i == 1) { [ 0:07] 154 m_st = 0; [ 0:07] 155 } else { [ 0:07] 156 m_st = 2; [ 0:07] 157 } [ 0:07] 158 if (t1_i == 1) { [ 0:07] 159 t1_st = 0; [ 0:07] 160 } else { [ 0:07] 161 t1_st = 2; [ 0:07] 162 } [ 0:07] 163 [ 0:07] 164 return; [ 0:07] 165 } [ 0:07] 166 } [ 0:07] 167 int exists_runnable_thread(void) [ 0:07] 168 { int __retres1 ; [ 0:07] 169 [ 0:07] 170 { [ 0:07] 171 if (m_st == 0) { [ 0:07] 172 __retres1 = 1; [ 0:07] 173 goto return_label; [ 0:07] 174 } else { [ 0:07] 175 if (t1_st == 0) { [ 0:07] 176 __retres1 = 1; [ 0:07] 177 goto return_label; [ 0:07] 178 } else { [ 0:07] 179 [ 0:07] 180 } [ 0:07] 181 } [ 0:07] 182 __retres1 = 0; [ 0:07] 183 return_label: /* CIL Label */ [ 0:07] 184 return (__retres1); [ 0:07] 185 } [ 0:07] 186 } [ 0:07] 187 void eval(void) [ 0:07] 188 { [ 0:07] 189 int tmp ; [ 0:07] 190 [ 0:07] 191 { [ 0:07] 192 { [ 0:07] 193 while (1) { [ 0:07] 194 while_3_continue: /* CIL Label */ ; [ 0:07] 195 { [ 0:07] 196 tmp = exists_runnable_thread(); [ 0:07] 197 } [ 0:07] 198 if (tmp) { [ 0:07] 199 [ 0:07] 200 } else { [ 0:07] 201 goto while_3_break; [ 0:07] 202 } [ 0:07] 203 if (m_st == 0) { [ 0:07] 204 int tmp_ndt_1; [ 0:07] 205 tmp_ndt_1 = __VERIFIER_nondet_int(); [ 0:07] 206 if (tmp_ndt_1) { [ 0:07] 207 { [ 0:07] 208 m_st = 1; [ 0:07] 209 master(); [ 0:07] 210 } [ 0:07] 211 } else { [ 0:07] 212 [ 0:07] 213 } [ 0:07] 214 } else { [ 0:07] 215 [ 0:07] 216 } [ 0:07] 217 if (t1_st == 0) { [ 0:07] 218 int tmp_ndt_2; [ 0:07] 219 tmp_ndt_2 = __VERIFIER_nondet_int(); [ 0:07] 220 if (tmp_ndt_2) { [ 0:07] 221 { [ 0:07] 222 t1_st = 1; [ 0:07] 223 transmit1(); [ 0:07] 224 } [ 0:07] 225 } else { [ 0:07] 226 [ 0:07] 227 } [ 0:07] 228 } else { [ 0:07] 229 [ 0:07] 230 } [ 0:07] 231 } [ 0:07] 232 while_3_break: /* CIL Label */ ; [ 0:07] 233 } [ 0:07] 234 [ 0:07] 235 return; [ 0:07] 236 } [ 0:07] 237 } [ 0:07] 238 void fire_delta_events(void) [ 0:07] 239 { [ 0:07] 240 [ 0:07] 241 { [ 0:07] 242 if (M_E == 0) { [ 0:07] 243 M_E = 1; [ 0:07] 244 } else { [ 0:07] 245 [ 0:07] 246 } [ 0:07] 247 if (T1_E == 0) { [ 0:07] 248 T1_E = 1; [ 0:07] 249 } else { [ 0:07] 250 [ 0:07] 251 } [ 0:07] 252 if (E_1 == 0) { [ 0:07] 253 E_1 = 1; [ 0:07] 254 } else { [ 0:07] 255 [ 0:07] 256 } [ 0:07] 257 [ 0:07] 258 return; [ 0:07] 259 } [ 0:07] 260 } [ 0:07] 261 void reset_delta_events(void) [ 0:07] 262 { [ 0:07] 263 [ 0:07] 264 { [ 0:07] 265 if (M_E == 1) { [ 0:07] 266 M_E = 2; [ 0:07] 267 } else { [ 0:07] 268 [ 0:07] 269 } [ 0:07] 270 if (T1_E == 1) { [ 0:07] 271 T1_E = 2; [ 0:07] 272 } else { [ 0:07] 273 [ 0:07] 274 } [ 0:07] 275 if (E_1 == 1) { [ 0:07] 276 E_1 = 2; [ 0:07] 277 } else { [ 0:07] 278 [ 0:07] 279 } [ 0:07] 280 [ 0:07] 281 return; [ 0:07] 282 } [ 0:07] 283 } [ 0:07] 284 void activate_threads(void) [ 0:07] 285 { int tmp ; [ 0:07] 286 int tmp___0 ; [ 0:07] 287 [ 0:07] 288 { [ 0:07] 289 { [ 0:07] 290 tmp = is_master_triggered(); [ 0:07] 291 } [ 0:07] 292 if (tmp) { [ 0:07] 293 m_st = 0; [ 0:07] 294 } else { [ 0:07] 295 [ 0:07] 296 } [ 0:07] 297 { [ 0:07] 298 tmp___0 = is_transmit1_triggered(); [ 0:07] 299 } [ 0:07] 300 if (tmp___0) { [ 0:07] 301 t1_st = 0; [ 0:07] 302 } else { [ 0:07] 303 [ 0:07] 304 } [ 0:07] 305 [ 0:07] 306 return; [ 0:07] 307 } [ 0:07] 308 } [ 0:07] 309 void immediate_notify(void) [ 0:07] 310 { [ 0:07] 311 [ 0:07] 312 { [ 0:07] 313 { [ 0:07] 314 activate_threads(); [ 0:07] 315 } [ 0:07] 316 [ 0:07] 317 return; [ 0:07] 318 } [ 0:07] 319 } [ 0:07] 320 void fire_time_events(void) [ 0:07] 321 { [ 0:07] 322 [ 0:07] 323 { [ 0:07] 324 M_E = 1; [ 0:07] 325 [ 0:07] 326 return; [ 0:07] 327 } [ 0:07] 328 } [ 0:07] 329 void reset_time_events(void) [ 0:07] 330 { [ 0:07] 331 [ 0:07] 332 { [ 0:07] 333 if (M_E == 1) { [ 0:07] 334 M_E = 2; [ 0:07] 335 } else { [ 0:07] 336 [ 0:07] 337 } [ 0:07] 338 if (T1_E == 1) { [ 0:07] 339 T1_E = 2; [ 0:07] 340 } else { [ 0:07] 341 [ 0:07] 342 } [ 0:07] 343 if (E_1 == 1) { [ 0:07] 344 E_1 = 2; [ 0:07] 345 } else { [ 0:07] 346 [ 0:07] 347 } [ 0:07] 348 [ 0:07] 349 return; [ 0:07] 350 } [ 0:07] 351 } [ 0:07] 352 void init_model(void) [ 0:07] 353 { [ 0:07] 354 [ 0:07] 355 { [ 0:07] 356 m_i = 1; [ 0:07] 357 t1_i = 1; [ 0:07] 358 [ 0:07] 359 return; [ 0:07] 360 } [ 0:07] 361 } [ 0:07] 362 int stop_simulation(void) [ 0:07] 363 { int tmp ; [ 0:07] 364 int __retres2 ; [ 0:07] 365 [ 0:07] 366 { [ 0:07] 367 { [ 0:07] 368 tmp = exists_runnable_thread(); [ 0:07] 369 } [ 0:07] 370 if (tmp) { [ 0:07] 371 __retres2 = 0; [ 0:07] 372 goto return_label; [ 0:07] 373 } else { [ 0:07] 374 [ 0:07] 375 } [ 0:07] 376 __retres2 = 1; [ 0:07] 377 return_label: /* CIL Label */ [ 0:07] 378 return (__retres2); [ 0:07] 379 } [ 0:07] 380 } [ 0:07] 381 void start_simulation(void) [ 0:07] 382 { int kernel_st ; [ 0:07] 383 int tmp ; [ 0:07] 384 int tmp___0 ; [ 0:07] 385 [ 0:07] 386 { [ 0:07] 387 { [ 0:07] 388 kernel_st = 0; [ 0:07] 389 update_channels(); [ 0:07] 390 init_threads(); [ 0:07] 391 fire_delta_events(); [ 0:07] 392 activate_threads(); [ 0:07] 393 reset_delta_events(); [ 0:07] 394 } [ 0:07] 395 { [ 0:07] 396 while (1) { [ 0:07] 397 while_4_continue: /* CIL Label */ ; [ 0:07] 398 { [ 0:07] 399 kernel_st = 1; [ 0:07] 400 eval(); [ 0:07] 401 } [ 0:07] 402 { [ 0:07] 403 kernel_st = 2; [ 0:07] 404 update_channels(); [ 0:07] 405 } [ 0:07] 406 { [ 0:07] 407 kernel_st = 3; [ 0:07] 408 fire_delta_events(); [ 0:07] 409 activate_threads(); [ 0:07] 410 reset_delta_events(); [ 0:07] 411 } [ 0:07] 412 { [ 0:07] 413 tmp = exists_runnable_thread(); [ 0:07] 414 } [ 0:07] 415 if (tmp == 0) { [ 0:07] 416 { [ 0:07] 417 kernel_st = 4; [ 0:07] 418 fire_time_events(); [ 0:07] 419 activate_threads(); [ 0:07] 420 reset_time_events(); [ 0:07] 421 } [ 0:07] 422 } else { [ 0:07] 423 [ 0:07] 424 } [ 0:07] 425 { [ 0:07] 426 tmp___0 = stop_simulation(); [ 0:07] 427 } [ 0:07] 428 if (tmp___0) { [ 0:07] 429 goto while_4_break; [ 0:07] 430 } else { [ 0:07] 431 [ 0:07] 432 } [ 0:07] 433 } [ 0:07] 434 while_4_break: /* CIL Label */ ; [ 0:07] 435 } [ 0:07] 436 [ 0:07] 437 return; [ 0:07] 438 } [ 0:07] 439 } [ 0:07] 440 int main(void) [ 0:07] 441 { int __retres1 ; [ 0:07] 442 [ 0:07] 443 { [ 0:07] 444 { [ 0:07] 445 init_model(); [ 0:07] 446 start_simulation(); [ 0:07] 447 } [ 0:07] 448 __retres1 = 0; [ 0:07] 449 return (__retres1); [ 0:07] 450 } [ 0:07] 451 } [ 0:07] # expected error to be found at /home/xrockai/src/divine/nightly/test/svcomp/systemc/transmitter.01_false.cil.c:13, but it was not