[ 0:00] compiling /home/xrockai/src/divine/nightly/test/svcomp/product-lines/minepump_spec4_product45_false.cil.c [ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/minepump_spec4_product45_false.cil.c:328:44: warning: incompatible redeclaration of library function 'malloc' [ 0:00] extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ; [ 0:00] ^ [ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/minepump_spec4_product45_false.cil.c:328:44: note: 'malloc' is a builtin with type 'void *(unsigned long)' [ 0:00] 1 warning generated. [ 0:00] compiling /dios/lib/config/seqklee.bc [ 0:00] setting up pass: functionmeta, options = [ 0:01] setting up pass: fuse-ctors, options = [ 0:01] KLEE: output directory is "/var/obj/divine-nightly/semidbg/test/__test_work_dir.17/_klee_out" [ 0:03] KLEE: Using Z3 solver backend [ 0:03] WARNING: this target does not support the llvm.stacksave intrinsic. [ 0:03] 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:03] [ 0:03] KLEE: WARNING: undefined reference to function: __dios_tainted_init [ 0:05] KLEE: WARNING: undefined reference to function: klee_free [ 0:05] KLEE: WARNING: undefined reference to function: klee_malloc [ 0:05] i:1 [ 0:05] KLEE: WARNING ONCE: Alignment of memory from call "klee_malloc" is not modelled. Using alignment of 8. [ 0:05] about to __boot:0 [ 0:05] about to run the scheduler:0 [ 0:05] KLEE: WARNING ONCE: calling external: __dios_tainted_init() at /dios/libc/sys/start.cpp:49 5 [ 0:05] KLEE: ERROR: /dios/libc/sys/start.cpp:87: failed external call: __dios_tainted_init [ 0:05] KLEE: NOTE: now ignoring this error at this location [ 0:05] KLEE: ERROR: EXITING ON ERROR: [ 0:05] Error: failed external call: __dios_tainted_init [ 0:05] File: /dios/libc/sys/start.cpp [ 0:05] Line: 87 [ 0:05] assembly.ll line: 35807 [ 0:05] Stack: [ 0:05] #000035807 in __dios_start (l=0, argc=1, argv=94600239600136, envp=94600239677448) at /dios/libc/sys/start.cpp:87 [ 0:05] #100011777 in _ZN6__dios10sched_nullINS_5ClockINS_10NondetKleeINS_4BaseEEEEEE13run_schedulerINS_7ContextEEEvv () at /dios/sys/sched_null.hpp:163 [ 0:05] #200044140 in klee_boot (argc=2, argv=94600213617408) at /dios/arch/klee/boot.c:41 [ 0:05] [ 0:05] [ 0:05] 1 /* TAGS: error c sym */ [ 0:05] 2 /* VERIFY_OPTS: --symbolic -o nofail:malloc */ [ 0:05] 3 extern void __VERIFIER_error() __attribute__ ((__noreturn__)); [ 0:05] 4 [ 0:05] 5 extern int __VERIFIER_nondet_int(void); [ 0:05] 6 extern int printf (__const char *__restrict __format, ...); [ 0:05] 7 /* Generated by CIL v. 1.3.7 */ [ 0:05] 8 /* print_CIL_Input is true */ [ 0:05] 9 [ 0:05] 10 struct JoinPoint { [ 0:05] 11 void **(*fp)(struct JoinPoint * ) ; [ 0:05] 12 void **args ; [ 0:05] 13 int argsCount ; [ 0:05] 14 char const **argsType ; [ 0:05] 15 void *(*arg)(int , struct JoinPoint * ) ; [ 0:05] 16 char const *(*argType)(int , struct JoinPoint * ) ; [ 0:05] 17 void **retValue ; [ 0:05] 18 char const *retType ; [ 0:05] 19 char const *funcName ; [ 0:05] 20 char const *targetName ; [ 0:05] 21 char const *fileName ; [ 0:05] 22 char const *kind ; [ 0:05] 23 void *excep_return ; [ 0:05] 24 }; [ 0:05] 25 struct __UTAC__CFLOW_FUNC { [ 0:05] 26 int (*func)(int , int ) ; [ 0:05] 27 int val ; [ 0:05] 28 struct __UTAC__CFLOW_FUNC *next ; [ 0:05] 29 }; [ 0:05] 30 struct __UTAC__EXCEPTION { [ 0:05] 31 void *jumpbuf ; [ 0:05] 32 unsigned long long prtValue ; [ 0:05] 33 int pops ; [ 0:05] 34 struct __UTAC__CFLOW_FUNC *cflowfuncs ; [ 0:05] 35 }; [ 0:05] 36 typedef unsigned int size_t; [ 0:05] 37 struct __ACC__ERR { [ 0:05] 38 void *v ; [ 0:05] 39 struct __ACC__ERR *next ; [ 0:05] 40 }; [ 0:05] 41 #pragma merger(0,"scenario.i","") [ 0:05] 42 void waterRise(void) ; [ 0:05] 43 void changeMethaneLevel(void) ; [ 0:05] 44 void timeShift(void) ; [ 0:05] 45 void cleanup(void) ; [ 0:05] 46 void test(void) [ 0:05] 47 { int splverifierCounter ; [ 0:05] 48 int tmp ; [ 0:05] 49 int tmp___0 ; [ 0:05] 50 int tmp___1 ; [ 0:05] 51 int tmp___2 ; [ 0:05] 52 [ 0:05] 53 { [ 0:05] 54 splverifierCounter = 0; [ 0:05] 55 { [ 0:05] 56 while (1) { [ 0:05] 57 while_0_continue: /* CIL Label */ ; [ 0:05] 58 if (splverifierCounter < 4) { [ 0:05] 59 [ 0:05] 60 } else { [ 0:05] 61 goto while_0_break; [ 0:05] 62 } [ 0:05] 63 { [ 0:05] 64 tmp = __VERIFIER_nondet_int(); [ 0:05] 65 } [ 0:05] 66 if (tmp) { [ 0:05] 67 { [ 0:05] 68 waterRise(); [ 0:05] 69 } [ 0:05] 70 } else { [ 0:05] 71 [ 0:05] 72 } [ 0:05] 73 { [ 0:05] 74 tmp___0 = __VERIFIER_nondet_int(); [ 0:05] 75 } [ 0:05] 76 if (tmp___0) { [ 0:05] 77 { [ 0:05] 78 changeMethaneLevel(); [ 0:05] 79 } [ 0:05] 80 } else { [ 0:05] 81 [ 0:05] 82 } [ 0:05] 83 { [ 0:05] 84 tmp___2 = __VERIFIER_nondet_int(); [ 0:05] 85 } [ 0:05] 86 if (tmp___2) { [ 0:05] 87 [ 0:05] 88 } else { [ 0:05] 89 { [ 0:05] 90 tmp___1 = __VERIFIER_nondet_int(); [ 0:05] 91 } [ 0:05] 92 if (tmp___1) { [ 0:05] 93 [ 0:05] 94 } else { [ 0:05] 95 [ 0:05] 96 } [ 0:05] 97 } [ 0:05] 98 { [ 0:05] 99 timeShift(); [ 0:05] 100 } [ 0:05] 101 } [ 0:05] 102 while_0_break: /* CIL Label */ ; [ 0:05] 103 } [ 0:05] 104 { [ 0:05] 105 cleanup(); [ 0:05] 106 } [ 0:05] 107 return; [ 0:05] 108 } [ 0:05] 109 } [ 0:05] 110 #pragma merger(0,"MinePump.i","") [ 0:05] 111 void lowerWaterLevel(void) ; [ 0:05] 112 int isMethaneLevelCritical(void) ; [ 0:05] 113 void printEnvironment(void) ; [ 0:05] 114 int isHighWaterSensorDry(void) ; [ 0:05] 115 void activatePump(void) ; [ 0:05] 116 void deactivatePump(void) ; [ 0:05] 117 int isPumpRunning(void) ; [ 0:05] 118 void printPump(void) ; [ 0:05] 119 int pumpRunning = 0; [ 0:05] 120 int systemActive = 1; [ 0:05] 121 void __utac_acc__Specification4_spec__1(void) ; [ 0:05] 122 void processEnvironment(void) ; [ 0:05] 123 void timeShift(void) [ 0:05] 124 { [ 0:05] 125 [ 0:05] 126 { [ 0:05] 127 if (pumpRunning) { [ 0:05] 128 { [ 0:05] 129 lowerWaterLevel(); [ 0:05] 130 } [ 0:05] 131 } else { [ 0:05] 132 [ 0:05] 133 } [ 0:05] 134 if (systemActive) { [ 0:05] 135 { [ 0:05] 136 processEnvironment(); [ 0:05] 137 } [ 0:05] 138 } else { [ 0:05] 139 [ 0:05] 140 } [ 0:05] 141 { [ 0:05] 142 __utac_acc__Specification4_spec__1(); [ 0:05] 143 } [ 0:05] 144 return; [ 0:05] 145 } [ 0:05] 146 } [ 0:05] 147 void processEnvironment__wrappee__base(void) [ 0:05] 148 { [ 0:05] 149 [ 0:05] 150 { [ 0:05] 151 return; [ 0:05] 152 } [ 0:05] 153 } [ 0:05] 154 int isHighWaterLevel(void) ; [ 0:05] 155 void processEnvironment__wrappee__methaneQuery(void) [ 0:05] 156 { int tmp ; [ 0:05] 157 [ 0:05] 158 { [ 0:05] 159 if (! pumpRunning) { [ 0:05] 160 { [ 0:05] 161 tmp = isHighWaterLevel(); [ 0:05] 162 } [ 0:05] 163 if (tmp) { [ 0:05] 164 { [ 0:05] 165 activatePump(); [ 0:05] 166 } [ 0:05] 167 } else { [ 0:05] 168 { [ 0:05] 169 processEnvironment__wrappee__base(); [ 0:05] 170 } [ 0:05] 171 } [ 0:05] 172 } else { [ 0:05] 173 { [ 0:05] 174 processEnvironment__wrappee__base(); [ 0:05] 175 } [ 0:05] 176 } [ 0:05] 177 return; [ 0:05] 178 } [ 0:05] 179 } [ 0:05] 180 int isMethaneAlarm(void) ; [ 0:05] 181 void processEnvironment(void) [ 0:05] 182 { int tmp ; [ 0:05] 183 [ 0:05] 184 { [ 0:05] 185 if (pumpRunning) { [ 0:05] 186 { [ 0:05] 187 tmp = isMethaneAlarm(); [ 0:05] 188 } [ 0:05] 189 if (tmp) { [ 0:05] 190 { [ 0:05] 191 deactivatePump(); [ 0:05] 192 } [ 0:05] 193 } else { [ 0:05] 194 { [ 0:05] 195 processEnvironment__wrappee__methaneQuery(); [ 0:05] 196 } [ 0:05] 197 } [ 0:05] 198 } else { [ 0:05] 199 { [ 0:05] 200 processEnvironment__wrappee__methaneQuery(); [ 0:05] 201 } [ 0:05] 202 } [ 0:05] 203 return; [ 0:05] 204 } [ 0:05] 205 } [ 0:05] 206 void activatePump__wrappee__highWaterSensor(void) [ 0:05] 207 { [ 0:05] 208 [ 0:05] 209 { [ 0:05] 210 pumpRunning = 1; [ 0:05] 211 return; [ 0:05] 212 } [ 0:05] 213 } [ 0:05] 214 void activatePump(void) [ 0:05] 215 { int tmp ; [ 0:05] 216 [ 0:05] 217 { [ 0:05] 218 { [ 0:05] 219 tmp = isMethaneAlarm(); [ 0:05] 220 } [ 0:05] 221 if (tmp) { [ 0:05] 222 [ 0:05] 223 } else { [ 0:05] 224 { [ 0:05] 225 activatePump__wrappee__highWaterSensor(); [ 0:05] 226 } [ 0:05] 227 } [ 0:05] 228 return; [ 0:05] 229 } [ 0:05] 230 } [ 0:05] 231 void deactivatePump(void) [ 0:05] 232 { [ 0:05] 233 [ 0:05] 234 { [ 0:05] 235 pumpRunning = 0; [ 0:05] 236 return; [ 0:05] 237 } [ 0:05] 238 } [ 0:05] 239 int isMethaneAlarm(void) [ 0:05] 240 { int retValue_acc ; [ 0:05] 241 [ 0:05] 242 { [ 0:05] 243 { [ 0:05] 244 retValue_acc = isMethaneLevelCritical(); [ 0:05] 245 } [ 0:05] 246 return (retValue_acc); [ 0:05] 247 return (retValue_acc); [ 0:05] 248 } [ 0:05] 249 } [ 0:05] 250 int isPumpRunning(void) [ 0:05] 251 { int retValue_acc ; [ 0:05] 252 [ 0:05] 253 { [ 0:05] 254 retValue_acc = pumpRunning; [ 0:05] 255 return (retValue_acc); [ 0:05] 256 return (retValue_acc); [ 0:05] 257 } [ 0:05] 258 } [ 0:05] 259 void printPump(void) [ 0:05] 260 { [ 0:05] 261 [ 0:05] 262 { [ 0:05] 263 { [ 0:05] 264 printf("Pump(System:"); [ 0:05] 265 } [ 0:05] 266 if (systemActive) { [ 0:05] 267 { [ 0:05] 268 printf("On"); [ 0:05] 269 } [ 0:05] 270 } else { [ 0:05] 271 { [ 0:05] 272 printf("Off"); [ 0:05] 273 } [ 0:05] 274 } [ 0:05] 275 { [ 0:05] 276 printf(",Pump:"); [ 0:05] 277 } [ 0:05] 278 if (pumpRunning) { [ 0:05] 279 { [ 0:05] 280 printf("On"); [ 0:05] 281 } [ 0:05] 282 } else { [ 0:05] 283 { [ 0:05] 284 printf("Off"); [ 0:05] 285 } [ 0:05] 286 } [ 0:05] 287 { [ 0:05] 288 printf(") "); [ 0:05] 289 printEnvironment(); [ 0:05] 290 printf("\n"); [ 0:05] 291 } [ 0:05] 292 return; [ 0:05] 293 } [ 0:05] 294 } [ 0:05] 295 int isHighWaterLevel(void) [ 0:05] 296 { int retValue_acc ; [ 0:05] 297 int tmp ; [ 0:05] 298 int tmp___0 ; [ 0:05] 299 [ 0:05] 300 { [ 0:05] 301 { [ 0:05] 302 tmp = isHighWaterSensorDry(); [ 0:05] 303 } [ 0:05] 304 if (tmp) { [ 0:05] 305 tmp___0 = 0; [ 0:05] 306 } else { [ 0:05] 307 tmp___0 = 1; [ 0:05] 308 } [ 0:05] 309 retValue_acc = tmp___0; [ 0:05] 310 return (retValue_acc); [ 0:05] 311 return (retValue_acc); [ 0:05] 312 } [ 0:05] 313 } [ 0:05] 314 #pragma merger(0,"wsllib_check.i","") [ 0:05] 315 void __automaton_fail(void) [ 0:05] 316 { [ 0:05] 317 [ 0:05] 318 { [ 0:05] 319 ERROR: __VERIFIER_error(); /* ERROR */ [ 0:05] 320 return; [ 0:05] 321 } [ 0:05] 322 } [ 0:05] 323 #pragma merger(0,"libacc.i","") [ 0:05] 324 extern __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const *__assertion , [ 0:05] 325 char const *__file , [ 0:05] 326 unsigned int __line , [ 0:05] 327 char const *__function ) ; [ 0:05] 328 extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ; [ 0:05] 329 extern __attribute__((__nothrow__)) void free(void *__ptr ) ; [ 0:05] 330 void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int , [ 0:05] 331 int ) , [ 0:05] 332 int val ) [ 0:05] 333 { struct __UTAC__EXCEPTION *excep ; [ 0:05] 334 struct __UTAC__CFLOW_FUNC *cf ; [ 0:05] 335 void *tmp ; [ 0:05] 336 unsigned long __cil_tmp7 ; [ 0:05] 337 unsigned long __cil_tmp8 ; [ 0:05] 338 unsigned long __cil_tmp9 ; [ 0:05] 339 unsigned long __cil_tmp10 ; [ 0:05] 340 unsigned long __cil_tmp11 ; [ 0:05] 341 unsigned long __cil_tmp12 ; [ 0:05] 342 unsigned long __cil_tmp13 ; [ 0:05] 343 unsigned long __cil_tmp14 ; [ 0:05] 344 int (**mem_15)(int , int ) ; [ 0:05] 345 int *mem_16 ; [ 0:05] 346 struct __UTAC__CFLOW_FUNC **mem_17 ; [ 0:05] 347 struct __UTAC__CFLOW_FUNC **mem_18 ; [ 0:05] 348 struct __UTAC__CFLOW_FUNC **mem_19 ; [ 0:05] 349 [ 0:05] 350 { [ 0:05] 351 { [ 0:05] 352 excep = (struct __UTAC__EXCEPTION *)exception; [ 0:05] 353 tmp = malloc(24UL); [ 0:05] 354 cf = (struct __UTAC__CFLOW_FUNC *)tmp; [ 0:05] 355 mem_15 = (int (**)(int , int ))cf; [ 0:05] 356 *mem_15 = cflow_func; [ 0:05] 357 __cil_tmp7 = (unsigned long )cf; [ 0:05] 358 __cil_tmp8 = __cil_tmp7 + 8; [ 0:05] 359 mem_16 = (int *)__cil_tmp8; [ 0:05] 360 *mem_16 = val; [ 0:05] 361 __cil_tmp9 = (unsigned long )cf; [ 0:05] 362 __cil_tmp10 = __cil_tmp9 + 16; [ 0:05] 363 __cil_tmp11 = (unsigned long )excep; [ 0:05] 364 __cil_tmp12 = __cil_tmp11 + 24; [ 0:05] 365 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10; [ 0:05] 366 mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12; [ 0:05] 367 *mem_17 = *mem_18; [ 0:05] 368 __cil_tmp13 = (unsigned long )excep; [ 0:05] 369 __cil_tmp14 = __cil_tmp13 + 24; [ 0:05] 370 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14; [ 0:05] 371 *mem_19 = cf; [ 0:05] 372 } [ 0:05] 373 return; [ 0:05] 374 } [ 0:05] 375 } [ 0:05] 376 void __utac__exception__cf_handler_free(void *exception ) [ 0:05] 377 { struct __UTAC__EXCEPTION *excep ; [ 0:05] 378 struct __UTAC__CFLOW_FUNC *cf ; [ 0:05] 379 struct __UTAC__CFLOW_FUNC *tmp ; [ 0:05] 380 unsigned long __cil_tmp5 ; [ 0:05] 381 unsigned long __cil_tmp6 ; [ 0:05] 382 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ; [ 0:05] 383 unsigned long __cil_tmp8 ; [ 0:05] 384 unsigned long __cil_tmp9 ; [ 0:05] 385 unsigned long __cil_tmp10 ; [ 0:05] 386 unsigned long __cil_tmp11 ; [ 0:05] 387 void *__cil_tmp12 ; [ 0:05] 388 unsigned long __cil_tmp13 ; [ 0:05] 389 unsigned long __cil_tmp14 ; [ 0:05] 390 struct __UTAC__CFLOW_FUNC **mem_15 ; [ 0:05] 391 struct __UTAC__CFLOW_FUNC **mem_16 ; [ 0:05] 392 struct __UTAC__CFLOW_FUNC **mem_17 ; [ 0:05] 393 [ 0:05] 394 { [ 0:05] 395 excep = (struct __UTAC__EXCEPTION *)exception; [ 0:05] 396 __cil_tmp5 = (unsigned long )excep; [ 0:05] 397 __cil_tmp6 = __cil_tmp5 + 24; [ 0:05] 398 mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6; [ 0:05] 399 cf = *mem_15; [ 0:05] 400 { [ 0:05] 401 while (1) { [ 0:05] 402 while_1_continue: /* CIL Label */ ; [ 0:05] 403 { [ 0:05] 404 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0; [ 0:05] 405 __cil_tmp8 = (unsigned long )__cil_tmp7; [ 0:05] 406 __cil_tmp9 = (unsigned long )cf; [ 0:05] 407 if (__cil_tmp9 != __cil_tmp8) { [ 0:05] 408 [ 0:05] 409 } else { [ 0:05] 410 goto while_1_break; [ 0:05] 411 } [ 0:05] 412 } [ 0:05] 413 { [ 0:05] 414 tmp = cf; [ 0:05] 415 __cil_tmp10 = (unsigned long )cf; [ 0:05] 416 __cil_tmp11 = __cil_tmp10 + 16; [ 0:05] 417 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11; [ 0:05] 418 cf = *mem_16; [ 0:05] 419 __cil_tmp12 = (void *)tmp; [ 0:05] 420 free(__cil_tmp12); [ 0:05] 421 } [ 0:05] 422 } [ 0:05] 423 while_1_break: /* CIL Label */ ; [ 0:05] 424 } [ 0:05] 425 __cil_tmp13 = (unsigned long )excep; [ 0:05] 426 __cil_tmp14 = __cil_tmp13 + 24; [ 0:05] 427 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14; [ 0:05] 428 *mem_17 = (struct __UTAC__CFLOW_FUNC *)0; [ 0:05] 429 return; [ 0:05] 430 } [ 0:05] 431 } [ 0:05] 432 void __utac__exception__cf_handler_reset(void *exception ) [ 0:05] 433 { struct __UTAC__EXCEPTION *excep ; [ 0:05] 434 struct __UTAC__CFLOW_FUNC *cf ; [ 0:05] 435 unsigned long __cil_tmp5 ; [ 0:05] 436 unsigned long __cil_tmp6 ; [ 0:05] 437 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ; [ 0:05] 438 unsigned long __cil_tmp8 ; [ 0:05] 439 unsigned long __cil_tmp9 ; [ 0:05] 440 int (*__cil_tmp10)(int , int ) ; [ 0:05] 441 unsigned long __cil_tmp11 ; [ 0:05] 442 unsigned long __cil_tmp12 ; [ 0:05] 443 int __cil_tmp13 ; [ 0:05] 444 unsigned long __cil_tmp14 ; [ 0:05] 445 unsigned long __cil_tmp15 ; [ 0:05] 446 struct __UTAC__CFLOW_FUNC **mem_16 ; [ 0:05] 447 int (**mem_17)(int , int ) ; [ 0:05] 448 int *mem_18 ; [ 0:05] 449 struct __UTAC__CFLOW_FUNC **mem_19 ; [ 0:05] 450 [ 0:05] 451 { [ 0:05] 452 excep = (struct __UTAC__EXCEPTION *)exception; [ 0:05] 453 __cil_tmp5 = (unsigned long )excep; [ 0:05] 454 __cil_tmp6 = __cil_tmp5 + 24; [ 0:05] 455 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6; [ 0:05] 456 cf = *mem_16; [ 0:05] 457 { [ 0:05] 458 while (1) { [ 0:05] 459 while_2_continue: /* CIL Label */ ; [ 0:05] 460 { [ 0:05] 461 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0; [ 0:05] 462 __cil_tmp8 = (unsigned long )__cil_tmp7; [ 0:05] 463 __cil_tmp9 = (unsigned long )cf; [ 0:05] 464 if (__cil_tmp9 != __cil_tmp8) { [ 0:05] 465 [ 0:05] 466 } else { [ 0:05] 467 goto while_2_break; [ 0:05] 468 } [ 0:05] 469 } [ 0:05] 470 { [ 0:05] 471 mem_17 = (int (**)(int , int ))cf; [ 0:05] 472 __cil_tmp10 = *mem_17; [ 0:05] 473 __cil_tmp11 = (unsigned long )cf; [ 0:05] 474 __cil_tmp12 = __cil_tmp11 + 8; [ 0:05] 475 mem_18 = (int *)__cil_tmp12; [ 0:05] 476 __cil_tmp13 = *mem_18; [ 0:05] 477 (*__cil_tmp10)(4, __cil_tmp13); [ 0:05] 478 __cil_tmp14 = (unsigned long )cf; [ 0:05] 479 __cil_tmp15 = __cil_tmp14 + 16; [ 0:05] 480 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15; [ 0:05] 481 cf = *mem_19; [ 0:05] 482 } [ 0:05] 483 } [ 0:05] 484 while_2_break: /* CIL Label */ ; [ 0:05] 485 } [ 0:05] 486 { [ 0:05] 487 __utac__exception__cf_handler_free(exception); [ 0:05] 488 } [ 0:05] 489 return; [ 0:05] 490 } [ 0:05] 491 } [ 0:05] 492 void *__utac__error_stack_mgt(void *env , int mode , int count ) ; [ 0:05] 493 static struct __ACC__ERR *head = (struct __ACC__ERR *)0; [ 0:05] 494 void *__utac__error_stack_mgt(void *env , int mode , int count ) [ 0:05] 495 { void *retValue_acc ; [ 0:05] 496 struct __ACC__ERR *new ; [ 0:05] 497 void *tmp ; [ 0:05] 498 struct __ACC__ERR *temp ; [ 0:05] 499 struct __ACC__ERR *next ; [ 0:05] 500 void *excep ; [ 0:05] 501 unsigned long __cil_tmp10 ; [ 0:05] 502 unsigned long __cil_tmp11 ; [ 0:05] 503 unsigned long __cil_tmp12 ; [ 0:05] 504 unsigned long __cil_tmp13 ; [ 0:05] 505 void *__cil_tmp14 ; [ 0:05] 506 unsigned long __cil_tmp15 ; [ 0:05] 507 unsigned long __cil_tmp16 ; [ 0:05] 508 void *__cil_tmp17 ; [ 0:05] 509 void **mem_18 ; [ 0:05] 510 struct __ACC__ERR **mem_19 ; [ 0:05] 511 struct __ACC__ERR **mem_20 ; [ 0:05] 512 void **mem_21 ; [ 0:05] 513 struct __ACC__ERR **mem_22 ; [ 0:05] 514 void **mem_23 ; [ 0:05] 515 void **mem_24 ; [ 0:05] 516 [ 0:05] 517 { [ 0:05] 518 if (count == 0) { [ 0:05] 519 return (retValue_acc); [ 0:05] 520 } else { [ 0:05] 521 [ 0:05] 522 } [ 0:05] 523 if (mode == 0) { [ 0:05] 524 { [ 0:05] 525 tmp = malloc(16UL); [ 0:05] 526 new = (struct __ACC__ERR *)tmp; [ 0:05] 527 mem_18 = (void **)new; [ 0:05] 528 *mem_18 = env; [ 0:05] 529 __cil_tmp10 = (unsigned long )new; [ 0:05] 530 __cil_tmp11 = __cil_tmp10 + 8; [ 0:05] 531 mem_19 = (struct __ACC__ERR **)__cil_tmp11; [ 0:05] 532 *mem_19 = head; [ 0:05] 533 head = new; [ 0:05] 534 retValue_acc = (void *)new; [ 0:05] 535 } [ 0:05] 536 return (retValue_acc); [ 0:05] 537 } else { [ 0:05] 538 [ 0:05] 539 } [ 0:05] 540 if (mode == 1) { [ 0:05] 541 temp = head; [ 0:05] 542 { [ 0:05] 543 while (1) { [ 0:05] 544 while_3_continue: /* CIL Label */ ; [ 0:05] 545 if (count > 1) { [ 0:05] 546 [ 0:05] 547 } else { [ 0:05] 548 goto while_3_break; [ 0:05] 549 } [ 0:05] 550 { [ 0:05] 551 __cil_tmp12 = (unsigned long )temp; [ 0:05] 552 __cil_tmp13 = __cil_tmp12 + 8; [ 0:05] 553 mem_20 = (struct __ACC__ERR **)__cil_tmp13; [ 0:05] 554 next = *mem_20; [ 0:05] 555 mem_21 = (void **)temp; [ 0:05] 556 excep = *mem_21; [ 0:05] 557 __cil_tmp14 = (void *)temp; [ 0:05] 558 free(__cil_tmp14); [ 0:05] 559 __utac__exception__cf_handler_reset(excep); [ 0:05] 560 temp = next; [ 0:05] 561 count = count - 1; [ 0:05] 562 } [ 0:05] 563 } [ 0:05] 564 while_3_break: /* CIL Label */ ; [ 0:05] 565 } [ 0:05] 566 { [ 0:05] 567 __cil_tmp15 = (unsigned long )temp; [ 0:05] 568 __cil_tmp16 = __cil_tmp15 + 8; [ 0:05] 569 mem_22 = (struct __ACC__ERR **)__cil_tmp16; [ 0:05] 570 head = *mem_22; [ 0:05] 571 mem_23 = (void **)temp; [ 0:05] 572 excep = *mem_23; [ 0:05] 573 __cil_tmp17 = (void *)temp; [ 0:05] 574 free(__cil_tmp17); [ 0:05] 575 __utac__exception__cf_handler_reset(excep); [ 0:05] 576 retValue_acc = excep; [ 0:05] 577 } [ 0:05] 578 return (retValue_acc); [ 0:05] 579 } else { [ 0:05] 580 [ 0:05] 581 } [ 0:05] 582 if (mode == 2) { [ 0:05] 583 if (head) { [ 0:05] 584 mem_24 = (void **)head; [ 0:05] 585 retValue_acc = *mem_24; [ 0:05] 586 return (retValue_acc); [ 0:05] 587 } else { [ 0:05] 588 retValue_acc = (void *)0; [ 0:05] 589 return (retValue_acc); [ 0:05] 590 } [ 0:05] 591 } else { [ 0:05] 592 [ 0:05] 593 } [ 0:05] 594 return (retValue_acc); [ 0:05] 595 } [ 0:05] 596 } [ 0:05] 597 void *__utac__get_this_arg(int i , struct JoinPoint *this ) [ 0:05] 598 { void *retValue_acc ; [ 0:05] 599 unsigned long __cil_tmp4 ; [ 0:05] 600 unsigned long __cil_tmp5 ; [ 0:05] 601 int __cil_tmp6 ; [ 0:05] 602 int __cil_tmp7 ; [ 0:05] 603 unsigned long __cil_tmp8 ; [ 0:05] 604 unsigned long __cil_tmp9 ; [ 0:05] 605 void **__cil_tmp10 ; [ 0:05] 606 void **__cil_tmp11 ; [ 0:05] 607 int *mem_12 ; [ 0:05] 608 void ***mem_13 ; [ 0:05] 609 [ 0:05] 610 { [ 0:05] 611 if (i > 0) { [ 0:05] 612 { [ 0:05] 613 __cil_tmp4 = (unsigned long )this; [ 0:05] 614 __cil_tmp5 = __cil_tmp4 + 16; [ 0:05] 615 mem_12 = (int *)__cil_tmp5; [ 0:05] 616 __cil_tmp6 = *mem_12; [ 0:05] 617 if (i <= __cil_tmp6) { [ 0:05] 618 [ 0:05] 619 } else { [ 0:05] 620 { [ 0:05] 621 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c", [ 0:05] 622 123U, "__utac__get_this_arg"); [ 0:05] 623 } [ 0:05] 624 } [ 0:05] 625 } [ 0:05] 626 } else { [ 0:05] 627 { [ 0:05] 628 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c", [ 0:05] 629 123U, "__utac__get_this_arg"); [ 0:05] 630 } [ 0:05] 631 } [ 0:05] 632 __cil_tmp7 = i - 1; [ 0:05] 633 __cil_tmp8 = (unsigned long )this; [ 0:05] 634 __cil_tmp9 = __cil_tmp8 + 8; [ 0:05] 635 mem_13 = (void ***)__cil_tmp9; [ 0:05] 636 __cil_tmp10 = *mem_13; [ 0:05] 637 __cil_tmp11 = __cil_tmp10 + __cil_tmp7; [ 0:05] 638 retValue_acc = *__cil_tmp11; [ 0:05] 639 return (retValue_acc); [ 0:05] 640 return (retValue_acc); [ 0:05] 641 } [ 0:05] 642 } [ 0:05] 643 char const *__utac__get_this_argtype(int i , struct JoinPoint *this ) [ 0:05] 644 { char const *retValue_acc ; [ 0:05] 645 unsigned long __cil_tmp4 ; [ 0:05] 646 unsigned long __cil_tmp5 ; [ 0:05] 647 int __cil_tmp6 ; [ 0:05] 648 int __cil_tmp7 ; [ 0:05] 649 unsigned long __cil_tmp8 ; [ 0:05] 650 unsigned long __cil_tmp9 ; [ 0:05] 651 char const **__cil_tmp10 ; [ 0:05] 652 char const **__cil_tmp11 ; [ 0:05] 653 int *mem_12 ; [ 0:05] 654 char const ***mem_13 ; [ 0:05] 655 [ 0:05] 656 { [ 0:05] 657 if (i > 0) { [ 0:05] 658 { [ 0:05] 659 __cil_tmp4 = (unsigned long )this; [ 0:05] 660 __cil_tmp5 = __cil_tmp4 + 16; [ 0:05] 661 mem_12 = (int *)__cil_tmp5; [ 0:05] 662 __cil_tmp6 = *mem_12; [ 0:05] 663 if (i <= __cil_tmp6) { [ 0:05] 664 [ 0:05] 665 } else { [ 0:05] 666 { [ 0:05] 667 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c", [ 0:05] 668 131U, "__utac__get_this_argtype"); [ 0:05] 669 } [ 0:05] 670 } [ 0:05] 671 } [ 0:05] 672 } else { [ 0:05] 673 { [ 0:05] 674 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c", [ 0:05] 675 131U, "__utac__get_this_argtype"); [ 0:05] 676 } [ 0:05] 677 } [ 0:05] 678 __cil_tmp7 = i - 1; [ 0:05] 679 __cil_tmp8 = (unsigned long )this; [ 0:05] 680 __cil_tmp9 = __cil_tmp8 + 24; [ 0:05] 681 mem_13 = (char const ***)__cil_tmp9; [ 0:05] 682 __cil_tmp10 = *mem_13; [ 0:05] 683 __cil_tmp11 = __cil_tmp10 + __cil_tmp7; [ 0:05] 684 retValue_acc = *__cil_tmp11; [ 0:05] 685 return (retValue_acc); [ 0:05] 686 return (retValue_acc); [ 0:05] 687 } [ 0:05] 688 } [ 0:05] 689 #pragma merger(0,"Specification4_spec.i","") [ 0:05] 690 int getWaterLevel(void) ; [ 0:05] 691 void __utac_acc__Specification4_spec__1(void) [ 0:05] 692 { int tmp ; [ 0:05] 693 int tmp___0 ; [ 0:05] 694 [ 0:05] 695 { [ 0:05] 696 { [ 0:05] 697 tmp = getWaterLevel(); [ 0:05] 698 } [ 0:05] 699 if (tmp == 0) { [ 0:05] 700 { [ 0:05] 701 tmp___0 = isPumpRunning(); [ 0:05] 702 } [ 0:05] 703 if (tmp___0) { [ 0:05] 704 { [ 0:05] 705 __automaton_fail(); [ 0:05] 706 } [ 0:05] 707 } else { [ 0:05] 708 [ 0:05] 709 } [ 0:05] 710 } else { [ 0:05] 711 [ 0:05] 712 } [ 0:05] 713 return; [ 0:05] 714 } [ 0:05] 715 } [ 0:05] 716 #pragma merger(0,"Test.i","") [ 0:05] 717 int cleanupTimeShifts = 4; [ 0:05] 718 void cleanup(void) [ 0:05] 719 { int i ; [ 0:05] 720 int __cil_tmp2 ; [ 0:05] 721 [ 0:05] 722 { [ 0:05] 723 { [ 0:05] 724 timeShift(); [ 0:05] 725 i = 0; [ 0:05] 726 } [ 0:05] 727 { [ 0:05] 728 while (1) { [ 0:05] 729 while_4_continue: /* CIL Label */ ; [ 0:05] 730 { [ 0:05] 731 __cil_tmp2 = cleanupTimeShifts - 1; [ 0:05] 732 if (i < __cil_tmp2) { [ 0:05] 733 [ 0:05] 734 } else { [ 0:05] 735 goto while_4_break; [ 0:05] 736 } [ 0:05] 737 } [ 0:05] 738 { [ 0:05] 739 timeShift(); [ 0:05] 740 i = i + 1; [ 0:05] 741 } [ 0:05] 742 } [ 0:05] 743 while_4_break: /* CIL Label */ ; [ 0:05] 744 } [ 0:05] 745 return; [ 0:05] 746 } [ 0:05] 747 } [ 0:05] 748 void Specification2(void) [ 0:05] 749 { [ 0:05] 750 [ 0:05] 751 { [ 0:05] 752 { [ 0:05] 753 timeShift(); [ 0:05] 754 printPump(); [ 0:05] 755 timeShift(); [ 0:05] 756 printPump(); [ 0:05] 757 timeShift(); [ 0:05] 758 printPump(); [ 0:05] 759 waterRise(); [ 0:05] 760 printPump(); [ 0:05] 761 timeShift(); [ 0:05] 762 printPump(); [ 0:05] 763 changeMethaneLevel(); [ 0:05] 764 printPump(); [ 0:05] 765 timeShift(); [ 0:05] 766 printPump(); [ 0:05] 767 cleanup(); [ 0:05] 768 } [ 0:05] 769 return; [ 0:05] 770 } [ 0:05] 771 } [ 0:05] 772 void setup(void) [ 0:05] 773 { [ 0:05] 774 [ 0:05] 775 { [ 0:05] 776 return; [ 0:05] 777 } [ 0:05] 778 } [ 0:05] 779 void runTest(void) [ 0:05] 780 { [ 0:05] 781 [ 0:05] 782 { [ 0:05] 783 { [ 0:05] 784 test(); [ 0:05] 785 } [ 0:05] 786 return; [ 0:05] 787 } [ 0:05] 788 } [ 0:05] 789 void select_helpers(void) ; [ 0:05] 790 void select_features(void) ; [ 0:05] 791 int valid_product(void) ; [ 0:05] 792 int main(void) [ 0:05] 793 { int retValue_acc ; [ 0:05] 794 int tmp ; [ 0:05] 795 [ 0:05] 796 { [ 0:05] 797 { [ 0:05] 798 select_helpers(); [ 0:05] 799 select_features(); [ 0:05] 800 tmp = valid_product(); [ 0:05] 801 } [ 0:05] 802 if (tmp) { [ 0:05] 803 { [ 0:05] 804 setup(); [ 0:05] 805 runTest(); [ 0:05] 806 } [ 0:05] 807 } else { [ 0:05] 808 [ 0:05] 809 } [ 0:05] 810 retValue_acc = 0; [ 0:05] 811 return (retValue_acc); [ 0:05] 812 return (retValue_acc); [ 0:05] 813 } [ 0:05] 814 } [ 0:05] 815 #pragma merger(0,"Environment.i","") [ 0:05] 816 int waterLevel = 1; [ 0:05] 817 int methaneLevelCritical = 0; [ 0:05] 818 void lowerWaterLevel(void) [ 0:05] 819 { [ 0:05] 820 [ 0:05] 821 { [ 0:05] 822 if (waterLevel > 0) { [ 0:05] 823 waterLevel = waterLevel - 1; [ 0:05] 824 } else { [ 0:05] 825 [ 0:05] 826 } [ 0:05] 827 return; [ 0:05] 828 } [ 0:05] 829 } [ 0:05] 830 void waterRise(void) [ 0:05] 831 { [ 0:05] 832 [ 0:05] 833 { [ 0:05] 834 if (waterLevel < 2) { [ 0:05] 835 waterLevel = waterLevel + 1; [ 0:05] 836 } else { [ 0:05] 837 [ 0:05] 838 } [ 0:05] 839 return; [ 0:05] 840 } [ 0:05] 841 } [ 0:05] 842 void changeMethaneLevel(void) [ 0:05] 843 { [ 0:05] 844 [ 0:05] 845 { [ 0:05] 846 if (methaneLevelCritical) { [ 0:05] 847 methaneLevelCritical = 0; [ 0:05] 848 } else { [ 0:05] 849 methaneLevelCritical = 1; [ 0:05] 850 } [ 0:05] 851 return; [ 0:05] 852 } [ 0:05] 853 } [ 0:05] 854 int isMethaneLevelCritical(void) [ 0:05] 855 { int retValue_acc ; [ 0:05] 856 [ 0:05] 857 { [ 0:05] 858 retValue_acc = methaneLevelCritical; [ 0:05] 859 return (retValue_acc); [ 0:05] 860 return (retValue_acc); [ 0:05] 861 } [ 0:05] 862 } [ 0:05] 863 void printEnvironment(void) [ 0:05] 864 { [ 0:05] 865 [ 0:05] 866 { [ 0:05] 867 { [ 0:05] 868 printf("Env(Water:%i", waterLevel); [ 0:05] 869 printf(",Meth:"); [ 0:05] 870 } [ 0:05] 871 if (methaneLevelCritical) { [ 0:05] 872 { [ 0:05] 873 printf("CRIT"); [ 0:05] 874 } [ 0:05] 875 } else { [ 0:05] 876 { [ 0:05] 877 printf("OK"); [ 0:05] 878 } [ 0:05] 879 } [ 0:05] 880 { [ 0:05] 881 printf(")"); [ 0:05] 882 } [ 0:05] 883 return; [ 0:05] 884 } [ 0:05] 885 } [ 0:05] 886 int getWaterLevel(void) [ 0:05] 887 { int retValue_acc ; [ 0:05] 888 [ 0:05] 889 { [ 0:05] 890 retValue_acc = waterLevel; [ 0:05] 891 return (retValue_acc); [ 0:05] 892 return (retValue_acc); [ 0:05] 893 } [ 0:05] 894 } [ 0:05] 895 int isHighWaterSensorDry(void) [ 0:05] 896 { int retValue_acc ; [ 0:05] 897 [ 0:05] 898 { [ 0:05] 899 if (waterLevel < 2) { [ 0:05] 900 retValue_acc = 1; [ 0:05] 901 return (retValue_acc); [ 0:05] 902 } else { [ 0:05] 903 retValue_acc = 0; [ 0:05] 904 return (retValue_acc); [ 0:05] 905 } [ 0:05] 906 return (retValue_acc); [ 0:05] 907 } [ 0:05] 908 } [ 0:05] 909 #pragma merger(0,"featureselect.i","") [ 0:05] 910 int select_one(void) ; [ 0:05] 911 int select_one(void) [ 0:05] 912 { int retValue_acc ; [ 0:05] 913 int choice = __VERIFIER_nondet_int(); [ 0:05] 914 [ 0:05] 915 { [ 0:05] 916 retValue_acc = choice; [ 0:05] 917 return (retValue_acc); [ 0:05] 918 return (retValue_acc); [ 0:05] 919 } [ 0:05] 920 } [ 0:05] 921 void select_features(void) [ 0:05] 922 { [ 0:05] 923 [ 0:05] 924 { [ 0:05] 925 return; [ 0:05] 926 } [ 0:05] 927 } [ 0:05] 928 void select_helpers(void) [ 0:05] 929 { [ 0:05] 930 [ 0:05] 931 { [ 0:05] 932 return; [ 0:05] 933 } [ 0:05] 934 } [ 0:05] 935 int valid_product(void) [ 0:05] 936 { int retValue_acc ; [ 0:05] 937 [ 0:05] 938 { [ 0:05] 939 retValue_acc = 1; [ 0:05] 940 return (retValue_acc); [ 0:05] 941 return (retValue_acc); [ 0:05] 942 } [ 0:05] 943 } [ 0:05] # expected error to be found at /home/xrockai/src/divine/nightly/test/svcomp/product-lines/minepump_spec4_product45_false.cil.c:319, but it was not