[ 0:01] compiling /home/xrockai/src/divine/nightly/test/svcomp/systemc/pc_sfifo_1_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:06] KLEE: WARNING: undefined reference to function: klee_free [ 0:06] KLEE: WARNING: undefined reference to function: klee_malloc [ 0:06] 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: 34602 [ 0:07] Stack: [ 0:07] #000034602 in __dios_start (l=0, argc=1, argv=94749595980296, envp=94749596073992) at /dios/libc/sys/start.cpp:87 [ 0:07] #100010621 in _ZN6__dios10sched_nullINS_5ClockINS_10NondetKleeINS_4BaseEEEEEE13run_schedulerINS_7ContextEEEvv () at /dios/sys/sched_null.hpp:163 [ 0:07] #200042952 in klee_boot (argc=2, argv=94749569521664) 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 [ 0:07] 7 void error(void) [ 0:07] 8 { [ 0:07] 9 [ 0:07] 10 { [ 0:07] 11 ERROR: __VERIFIER_error(); /* ERROR */ [ 0:07] 12 return; [ 0:07] 13 } [ 0:07] 14 } [ 0:07] 15 [ 0:07] 16 int q_buf_0 ; [ 0:07] 17 int q_free ; [ 0:07] 18 int q_read_ev ; [ 0:07] 19 int q_write_ev ; [ 0:07] 20 int p_num_write ; [ 0:07] 21 int p_last_write ; [ 0:07] 22 int p_dw_st ; [ 0:07] 23 int p_dw_pc ; [ 0:07] 24 int p_dw_i ; [ 0:07] 25 int c_num_read ; [ 0:07] 26 int c_last_read ; [ 0:07] 27 int c_dr_st ; [ 0:07] 28 int c_dr_pc ; [ 0:07] 29 int c_dr_i ; [ 0:07] 30 int is_do_write_p_triggered(void) [ 0:07] 31 { int __retres1 ; [ 0:07] 32 [ 0:07] 33 { [ 0:07] 34 if ((int )p_dw_pc == 1) { [ 0:07] 35 if ((int )q_read_ev == 1) { [ 0:07] 36 __retres1 = 1; [ 0:07] 37 goto return_label; [ 0:07] 38 } else { [ 0:07] 39 [ 0:07] 40 } [ 0:07] 41 } else { [ 0:07] 42 [ 0:07] 43 } [ 0:07] 44 __retres1 = 0; [ 0:07] 45 return_label: /* CIL Label */ [ 0:07] 46 return (__retres1); [ 0:07] 47 } [ 0:07] 48 } [ 0:07] 49 int is_do_read_c_triggered(void) [ 0:07] 50 { int __retres1 ; [ 0:07] 51 [ 0:07] 52 { [ 0:07] 53 if ((int )c_dr_pc == 1) { [ 0:07] 54 if ((int )q_write_ev == 1) { [ 0:07] 55 __retres1 = 1; [ 0:07] 56 goto return_label; [ 0:07] 57 } else { [ 0:07] 58 [ 0:07] 59 } [ 0:07] 60 } else { [ 0:07] 61 [ 0:07] 62 } [ 0:07] 63 __retres1 = 0; [ 0:07] 64 return_label: /* CIL Label */ [ 0:07] 65 return (__retres1); [ 0:07] 66 } [ 0:07] 67 } [ 0:07] 68 void immediate_notify_threads(void) [ 0:07] 69 { int tmp ; [ 0:07] 70 int tmp___0 ; [ 0:07] 71 [ 0:07] 72 { [ 0:07] 73 { [ 0:07] 74 tmp = is_do_write_p_triggered(); [ 0:07] 75 } [ 0:07] 76 if (tmp) { [ 0:07] 77 p_dw_st = 0; [ 0:07] 78 } else { [ 0:07] 79 [ 0:07] 80 } [ 0:07] 81 { [ 0:07] 82 tmp___0 = is_do_read_c_triggered(); [ 0:07] 83 } [ 0:07] 84 if (tmp___0) { [ 0:07] 85 c_dr_st = 0; [ 0:07] 86 } else { [ 0:07] 87 [ 0:07] 88 } [ 0:07] 89 [ 0:07] 90 return; [ 0:07] 91 } [ 0:07] 92 } [ 0:07] 93 void do_write_p(void) [ 0:07] 94 { [ 0:07] 95 [ 0:07] 96 [ 0:07] 97 { [ 0:07] 98 if ((int )p_dw_pc == 0) { [ 0:07] 99 goto DW_ENTRY; [ 0:07] 100 } else { [ 0:07] 101 if ((int )p_dw_pc == 1) { [ 0:07] 102 goto DW_WAIT_READ; [ 0:07] 103 } else { [ 0:07] 104 [ 0:07] 105 } [ 0:07] 106 } [ 0:07] 107 DW_ENTRY: [ 0:07] 108 { [ 0:07] 109 while (1) { [ 0:07] 110 while_0_continue: /* CIL Label */ ; [ 0:07] 111 if ((int )q_free == 0) { [ 0:07] 112 p_dw_st = 2; [ 0:07] 113 p_dw_pc = 1; [ 0:07] 114 [ 0:07] 115 goto return_label; [ 0:07] 116 DW_WAIT_READ: ; [ 0:07] 117 } else { [ 0:07] 118 [ 0:07] 119 } [ 0:07] 120 { [ 0:07] 121 q_buf_0 = __VERIFIER_nondet_int(); [ 0:07] 122 p_last_write = q_buf_0; [ 0:07] 123 p_num_write += 1; [ 0:07] 124 q_free = 0; [ 0:07] 125 q_write_ev = 1; [ 0:07] 126 immediate_notify_threads(); [ 0:07] 127 q_write_ev = 2; [ 0:07] 128 } [ 0:07] 129 } [ 0:07] 130 while_0_break: /* CIL Label */ ; [ 0:07] 131 } [ 0:07] 132 return_label: /* CIL Label */ [ 0:07] 133 return; [ 0:07] 134 } [ 0:07] 135 } [ 0:07] 136 static int a_t ; [ 0:07] 137 void do_read_c(void) [ 0:07] 138 { int a ; [ 0:07] 139 [ 0:07] 140 { [ 0:07] 141 if ((int )c_dr_pc == 0) { [ 0:07] 142 goto DR_ENTRY; [ 0:07] 143 } else { [ 0:07] 144 if ((int )c_dr_pc == 1) { [ 0:07] 145 goto DR_WAIT_WRITE; [ 0:07] 146 } else { [ 0:07] 147 [ 0:07] 148 } [ 0:07] 149 } [ 0:07] 150 DR_ENTRY: [ 0:07] 151 { [ 0:07] 152 while (1) { [ 0:07] 153 while_1_continue: /* CIL Label */ ; [ 0:07] 154 if ((int )q_free == 1) { [ 0:07] 155 c_dr_st = 2; [ 0:07] 156 c_dr_pc = 1; [ 0:07] 157 a_t = a; [ 0:07] 158 [ 0:07] 159 goto return_label; [ 0:07] 160 DR_WAIT_WRITE: [ 0:07] 161 a = a_t; [ 0:07] 162 } else { [ 0:07] 163 [ 0:07] 164 } [ 0:07] 165 { [ 0:07] 166 a = q_buf_0; [ 0:07] 167 c_last_read = a; [ 0:07] 168 c_num_read += 1; [ 0:07] 169 q_free = 1; [ 0:07] 170 q_read_ev = 1; [ 0:07] 171 immediate_notify_threads(); [ 0:07] 172 q_read_ev = 2; [ 0:07] 173 } [ 0:07] 174 if (p_last_write == c_last_read) { [ 0:07] 175 if (p_num_write == c_num_read) { [ 0:07] 176 [ 0:07] 177 } else { [ 0:07] 178 { [ 0:07] 179 error(); [ 0:07] 180 } [ 0:07] 181 } [ 0:07] 182 } else { [ 0:07] 183 { [ 0:07] 184 error(); [ 0:07] 185 } [ 0:07] 186 } [ 0:07] 187 } [ 0:07] 188 while_1_break: /* CIL Label */ ; [ 0:07] 189 } [ 0:07] 190 return_label: /* CIL Label */ [ 0:07] 191 return; [ 0:07] 192 } [ 0:07] 193 } [ 0:07] 194 void init_threads(void) [ 0:07] 195 { [ 0:07] 196 [ 0:07] 197 { [ 0:07] 198 if ((int )p_dw_i == 1) { [ 0:07] 199 p_dw_st = 0; [ 0:07] 200 } else { [ 0:07] 201 p_dw_st = 2; [ 0:07] 202 } [ 0:07] 203 if ((int )c_dr_i == 1) { [ 0:07] 204 c_dr_st = 0; [ 0:07] 205 } else { [ 0:07] 206 c_dr_st = 2; [ 0:07] 207 } [ 0:07] 208 [ 0:07] 209 return; [ 0:07] 210 } [ 0:07] 211 } [ 0:07] 212 int exists_runnable_thread(void) [ 0:07] 213 { int __retres1 ; [ 0:07] 214 [ 0:07] 215 { [ 0:07] 216 if ((int )p_dw_st == 0) { [ 0:07] 217 __retres1 = 1; [ 0:07] 218 goto return_label; [ 0:07] 219 } else { [ 0:07] 220 if ((int )c_dr_st == 0) { [ 0:07] 221 __retres1 = 1; [ 0:07] 222 goto return_label; [ 0:07] 223 } else { [ 0:07] 224 [ 0:07] 225 } [ 0:07] 226 } [ 0:07] 227 __retres1 = 0; [ 0:07] 228 return_label: /* CIL Label */ [ 0:07] 229 return (__retres1); [ 0:07] 230 } [ 0:07] 231 } [ 0:07] 232 void eval(void) [ 0:07] 233 { int tmp ; [ 0:07] 234 int tmp___0 ; [ 0:07] 235 int tmp___1 ; [ 0:07] 236 [ 0:07] 237 { [ 0:07] 238 { [ 0:07] 239 while (1) { [ 0:07] 240 while_2_continue: /* CIL Label */ ; [ 0:07] 241 { [ 0:07] 242 tmp___1 = exists_runnable_thread(); [ 0:07] 243 } [ 0:07] 244 if (tmp___1) { [ 0:07] 245 [ 0:07] 246 } else { [ 0:07] 247 goto while_2_break; [ 0:07] 248 } [ 0:07] 249 if ((int )p_dw_st == 0) { [ 0:07] 250 { [ 0:07] 251 tmp = __VERIFIER_nondet_int(); [ 0:07] 252 } [ 0:07] 253 if (tmp) { [ 0:07] 254 { [ 0:07] 255 p_dw_st = 1; [ 0:07] 256 do_write_p(); [ 0:07] 257 } [ 0:07] 258 } else { [ 0:07] 259 error(); [ 0:07] 260 } [ 0:07] 261 } else { [ 0:07] 262 [ 0:07] 263 } [ 0:07] 264 if ((int )c_dr_st == 0) { [ 0:07] 265 { [ 0:07] 266 tmp___0 = __VERIFIER_nondet_int(); [ 0:07] 267 } [ 0:07] 268 if (tmp___0) { [ 0:07] 269 { [ 0:07] 270 c_dr_st = 1; [ 0:07] 271 do_read_c(); [ 0:07] 272 } [ 0:07] 273 } else { [ 0:07] 274 [ 0:07] 275 } [ 0:07] 276 } else { [ 0:07] 277 [ 0:07] 278 } [ 0:07] 279 } [ 0:07] 280 while_2_break: /* CIL Label */ ; [ 0:07] 281 } [ 0:07] 282 [ 0:07] 283 return; [ 0:07] 284 } [ 0:07] 285 } [ 0:07] 286 int stop_simulation(void) [ 0:07] 287 { int tmp ; [ 0:07] 288 int __retres2 ; [ 0:07] 289 [ 0:07] 290 { [ 0:07] 291 { [ 0:07] 292 tmp = exists_runnable_thread(); [ 0:07] 293 } [ 0:07] 294 if (tmp) { [ 0:07] 295 __retres2 = 0; [ 0:07] 296 goto return_label; [ 0:07] 297 } else { [ 0:07] 298 [ 0:07] 299 } [ 0:07] 300 __retres2 = 1; [ 0:07] 301 return_label: /* CIL Label */ [ 0:07] 302 return (__retres2); [ 0:07] 303 } [ 0:07] 304 } [ 0:07] 305 void start_simulation(void) [ 0:07] 306 { int kernel_st ; [ 0:07] 307 int tmp ; [ 0:07] 308 [ 0:07] 309 { [ 0:07] 310 { [ 0:07] 311 kernel_st = 0; [ 0:07] 312 init_threads(); [ 0:07] 313 } [ 0:07] 314 { [ 0:07] 315 while (1) { [ 0:07] 316 while_3_continue: /* CIL Label */ ; [ 0:07] 317 { [ 0:07] 318 kernel_st = 1; [ 0:07] 319 eval(); [ 0:07] 320 tmp = stop_simulation(); [ 0:07] 321 } [ 0:07] 322 if (tmp) { [ 0:07] 323 goto while_3_break; [ 0:07] 324 } else { [ 0:07] 325 [ 0:07] 326 } [ 0:07] 327 } [ 0:07] 328 while_3_break: /* CIL Label */ ; [ 0:07] 329 } [ 0:07] 330 [ 0:07] 331 return; [ 0:07] 332 } [ 0:07] 333 } [ 0:07] 334 void init_model(void) [ 0:07] 335 { [ 0:07] 336 [ 0:07] 337 { [ 0:07] 338 q_free = 1; [ 0:07] 339 q_write_ev = 2; [ 0:07] 340 q_read_ev = q_write_ev; [ 0:07] 341 p_num_write = 0; [ 0:07] 342 p_dw_pc = 0; [ 0:07] 343 p_dw_i = 1; [ 0:07] 344 c_num_read = 0; [ 0:07] 345 c_dr_pc = 0; [ 0:07] 346 c_dr_i = 1; [ 0:07] 347 [ 0:07] 348 return; [ 0:07] 349 } [ 0:07] 350 } [ 0:07] 351 int main(void) [ 0:07] 352 { int __retres1 ; [ 0:07] 353 [ 0:07] 354 { [ 0:07] 355 { [ 0:07] 356 init_model(); [ 0:07] 357 start_simulation(); [ 0:07] 358 } [ 0:07] 359 __retres1 = 0; [ 0:07] 360 return (__retres1); [ 0:07] 361 } [ 0:07] 362 } [ 0:07] # expected error to be found at /home/xrockai/src/divine/nightly/test/svcomp/systemc/pc_sfifo_1_false.cil.c:11, but it was not