[ 0:00] compiling /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c [ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1611:10: warning: format string is not a string literal (potentially insecure) [ 0:00] printf(__cil_tmp6); [ 0:00] ^~~~~~~~~~ [ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1611:10: note: treat the string as an argument to avoid this [ 0:00] printf(__cil_tmp6); [ 0:00] ^ [ 0:00] "%s", [ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1616:12: warning: format string is not a string literal (potentially insecure) [ 0:00] printf(__cil_tmp7); [ 0:00] ^~~~~~~~~~ [ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1616:12: note: treat the string as an argument to avoid this [ 0:00] printf(__cil_tmp7); [ 0:00] ^ [ 0:00] "%s", [ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1621:12: warning: format string is not a string literal (potentially insecure) [ 0:00] printf(__cil_tmp8); [ 0:00] ^~~~~~~~~~ [ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1621:12: note: treat the string as an argument to avoid this [ 0:00] printf(__cil_tmp8); [ 0:00] ^ [ 0:00] "%s", [ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1626:10: warning: format string is not a string literal (potentially insecure) [ 0:00] printf(__cil_tmp9); [ 0:00] ^~~~~~~~~~ [ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1626:10: note: treat the string as an argument to avoid this [ 0:00] printf(__cil_tmp9); [ 0:00] ^ [ 0:00] "%s", [ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1630:10: warning: format string is not a string literal (potentially insecure) [ 0:00] printf(__cil_tmp11); [ 0:00] ^~~~~~~~~~~ [ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1630:10: note: treat the string as an argument to avoid this [ 0:00] printf(__cil_tmp11); [ 0:00] ^ [ 0:00] "%s", [ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1635:12: warning: format string is not a string literal (potentially insecure) [ 0:00] printf(__cil_tmp12); [ 0:00] ^~~~~~~~~~~ [ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1635:12: note: treat the string as an argument to avoid this [ 0:00] printf(__cil_tmp12); [ 0:00] ^ [ 0:00] "%s", [ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1640:12: warning: format string is not a string literal (potentially insecure) [ 0:00] printf(__cil_tmp13); [ 0:00] ^~~~~~~~~~~ [ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1640:12: note: treat the string as an argument to avoid this [ 0:00] printf(__cil_tmp13); [ 0:00] ^ [ 0:00] "%s", [ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1645:10: warning: format string is not a string literal (potentially insecure) [ 0:00] printf(__cil_tmp14); [ 0:00] ^~~~~~~~~~~ [ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1645:10: note: treat the string as an argument to avoid this [ 0:00] printf(__cil_tmp14); [ 0:00] ^ [ 0:00] "%s", [ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1689:10: warning: format string is not a string literal (potentially insecure) [ 0:00] printf(__cil_tmp20); [ 0:00] ^~~~~~~~~~~ [ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1689:10: note: treat the string as an argument to avoid this [ 0:00] printf(__cil_tmp20); [ 0:00] ^ [ 0:00] "%s", [ 0:00] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1746:10: warning: format string is not a string literal (potentially insecure) [ 0:01] printf(__cil_tmp26); [ 0:01] ^~~~~~~~~~~ [ 0:01] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1746:10: note: treat the string as an argument to avoid this [ 0:01] printf(__cil_tmp26); [ 0:01] ^ [ 0:01] "%s", [ 0:01] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1762:12: warning: format string is not a string literal (potentially insecure) [ 0:01] printf(__cil_tmp2); [ 0:01] ^~~~~~~~~~ [ 0:01] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:1762:12: note: treat the string as an argument to avoid this [ 0:01] printf(__cil_tmp2); [ 0:01] ^ [ 0:01] "%s", [ 0:01] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:2067:44: warning: incompatible redeclaration of library function 'malloc' [ 0:01] extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ; [ 0:01] ^ [ 0:01] /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:2067:44: note: 'malloc' is a builtin with type 'void *(unsigned long)' [ 0:01] 12 warnings generated. [ 0:01] compiling /dios/lib/config/seqklee.bc [ 0:01] 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.1/_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:06] KLEE: WARNING ONCE: Alignment of memory from call "klee_malloc" is not modelled. Using alignment of 8. [ 0:06] about to __boot:0 [ 0:06] about to run the scheduler:0 [ 0:06] KLEE: WARNING ONCE: calling external: __dios_tainted_init() at /dios/libc/sys/start.cpp:49 5 [ 0:06] KLEE: ERROR: /dios/libc/sys/start.cpp:87: failed external call: __dios_tainted_init [ 0:06] KLEE: NOTE: now ignoring this error at this location [ 0:06] KLEE: ERROR: EXITING ON ERROR: [ 0:06] Error: failed external call: __dios_tainted_init [ 0:06] File: /dios/libc/sys/start.cpp [ 0:06] Line: 87 [ 0:06] assembly.ll line: 41537 [ 0:06] Stack: [ 0:06] #000041537 in __dios_start (l=0, argc=1, argv=94191860748808, envp=94191860817928) at /dios/libc/sys/start.cpp:87 [ 0:06] #100017499 in _ZN6__dios10sched_nullINS_5ClockINS_10NondetKleeINS_4BaseEEEEEE13run_schedulerINS_7ContextEEEvv () at /dios/sys/sched_null.hpp:163 [ 0:06] #200049862 in klee_boot (argc=2, argv=94191833709312) at /dios/arch/klee/boot.c:41 [ 0:06] [ 0:06] [ 0:06] 1 /* TAGS: error c sym */ [ 0:06] 2 /* VERIFY_OPTS: --symbolic -o nofail:malloc */ [ 0:06] 3 extern void __VERIFIER_error() __attribute__ ((__noreturn__)); [ 0:06] 4 [ 0:06] 5 extern int __VERIFIER_nondet_int(void); [ 0:06] 6 /* Generated by CIL v. 1.3.7 */ [ 0:06] 7 /* print_CIL_Input is true */ [ 0:06] 8 [ 0:06] 9 struct JoinPoint { [ 0:06] 10 void **(*fp)(struct JoinPoint * ) ; [ 0:06] 11 void **args ; [ 0:06] 12 int argsCount ; [ 0:06] 13 char const **argsType ; [ 0:06] 14 void *(*arg)(int , struct JoinPoint * ) ; [ 0:06] 15 char const *(*argType)(int , struct JoinPoint * ) ; [ 0:06] 16 void **retValue ; [ 0:06] 17 char const *retType ; [ 0:06] 18 char const *funcName ; [ 0:06] 19 char const *targetName ; [ 0:06] 20 char const *fileName ; [ 0:06] 21 char const *kind ; [ 0:06] 22 void *excep_return ; [ 0:06] 23 }; [ 0:06] 24 struct __UTAC__CFLOW_FUNC { [ 0:06] 25 int (*func)(int , int ) ; [ 0:06] 26 int val ; [ 0:06] 27 struct __UTAC__CFLOW_FUNC *next ; [ 0:06] 28 }; [ 0:06] 29 struct __UTAC__EXCEPTION { [ 0:06] 30 void *jumpbuf ; [ 0:06] 31 unsigned long long prtValue ; [ 0:06] 32 int pops ; [ 0:06] 33 struct __UTAC__CFLOW_FUNC *cflowfuncs ; [ 0:06] 34 }; [ 0:06] 35 typedef unsigned int size_t; [ 0:06] 36 struct __ACC__ERR { [ 0:06] 37 void *v ; [ 0:06] 38 struct __ACC__ERR *next ; [ 0:06] 39 }; [ 0:06] 40 #pragma merger(0,"Test.i","") [ 0:06] 41 extern __attribute__((__nothrow__, __noreturn__)) void exit(int __status ) ; [ 0:06] 42 int cleanupTimeShifts = 12; [ 0:06] 43 int get_nondetMinMax07(void) [ 0:06] 44 { int retValue_acc ; [ 0:06] 45 int nd ; [ 0:06] 46 nd = __VERIFIER_nondet_int(); [ 0:06] 47 [ 0:06] 48 { [ 0:06] 49 if (nd == 0) { [ 0:06] 50 retValue_acc = 0; [ 0:06] 51 return (retValue_acc); [ 0:06] 52 } else { [ 0:06] 53 if (nd == 1) { [ 0:06] 54 retValue_acc = 1; [ 0:06] 55 return (retValue_acc); [ 0:06] 56 } else { [ 0:06] 57 if (nd == 2) { [ 0:06] 58 retValue_acc = 2; [ 0:06] 59 return (retValue_acc); [ 0:06] 60 } else { [ 0:06] 61 if (nd == 3) { [ 0:06] 62 retValue_acc = 3; [ 0:06] 63 return (retValue_acc); [ 0:06] 64 } else { [ 0:06] 65 if (nd == 4) { [ 0:06] 66 retValue_acc = 4; [ 0:06] 67 return (retValue_acc); [ 0:06] 68 } else { [ 0:06] 69 if (nd == 5) { [ 0:06] 70 retValue_acc = 5; [ 0:06] 71 return (retValue_acc); [ 0:06] 72 } else { [ 0:06] 73 if (nd == 6) { [ 0:06] 74 retValue_acc = 6; [ 0:06] 75 return (retValue_acc); [ 0:06] 76 } else { [ 0:06] 77 if (nd == 7) { [ 0:06] 78 retValue_acc = 7; [ 0:06] 79 return (retValue_acc); [ 0:06] 80 } else { [ 0:06] 81 { [ 0:06] 82 exit(0); [ 0:06] 83 } [ 0:06] 84 } [ 0:06] 85 } [ 0:06] 86 } [ 0:06] 87 } [ 0:06] 88 } [ 0:06] 89 } [ 0:06] 90 } [ 0:06] 91 } [ 0:06] 92 return (retValue_acc); [ 0:06] 93 } [ 0:06] 94 } [ 0:06] 95 void initPersonOnFloor(int person , int floor ) ; [ 0:06] 96 int getOrigin(int person ) ; [ 0:06] 97 void bobCall(void) [ 0:06] 98 { int tmp ; [ 0:06] 99 [ 0:06] 100 { [ 0:06] 101 { [ 0:06] 102 tmp = getOrigin(0); [ 0:06] 103 initPersonOnFloor(0, tmp); [ 0:06] 104 } [ 0:06] 105 return; [ 0:06] 106 } [ 0:06] 107 } [ 0:06] 108 void aliceCall(void) [ 0:06] 109 { int tmp ; [ 0:06] 110 [ 0:06] 111 { [ 0:06] 112 { [ 0:06] 113 tmp = getOrigin(1); [ 0:06] 114 initPersonOnFloor(1, tmp); [ 0:06] 115 } [ 0:06] 116 return; [ 0:06] 117 } [ 0:06] 118 } [ 0:06] 119 void angelinaCall(void) [ 0:06] 120 { int tmp ; [ 0:06] 121 [ 0:06] 122 { [ 0:06] 123 { [ 0:06] 124 tmp = getOrigin(2); [ 0:06] 125 initPersonOnFloor(2, tmp); [ 0:06] 126 } [ 0:06] 127 return; [ 0:06] 128 } [ 0:06] 129 } [ 0:06] 130 void chuckCall(void) [ 0:06] 131 { int tmp ; [ 0:06] 132 [ 0:06] 133 { [ 0:06] 134 { [ 0:06] 135 tmp = getOrigin(3); [ 0:06] 136 initPersonOnFloor(3, tmp); [ 0:06] 137 } [ 0:06] 138 return; [ 0:06] 139 } [ 0:06] 140 } [ 0:06] 141 void monicaCall(void) [ 0:06] 142 { int tmp ; [ 0:06] 143 [ 0:06] 144 { [ 0:06] 145 { [ 0:06] 146 tmp = getOrigin(4); [ 0:06] 147 initPersonOnFloor(4, tmp); [ 0:06] 148 } [ 0:06] 149 return; [ 0:06] 150 } [ 0:06] 151 } [ 0:06] 152 void bigMacCall(void) [ 0:06] 153 { int tmp ; [ 0:06] 154 [ 0:06] 155 { [ 0:06] 156 { [ 0:06] 157 tmp = getOrigin(5); [ 0:06] 158 initPersonOnFloor(5, tmp); [ 0:06] 159 } [ 0:06] 160 return; [ 0:06] 161 } [ 0:06] 162 } [ 0:06] 163 void timeShift(void) ; [ 0:06] 164 void threeTS(void) [ 0:06] 165 { [ 0:06] 166 [ 0:06] 167 { [ 0:06] 168 { [ 0:06] 169 timeShift(); [ 0:06] 170 timeShift(); [ 0:06] 171 timeShift(); [ 0:06] 172 } [ 0:06] 173 return; [ 0:06] 174 } [ 0:06] 175 } [ 0:06] 176 int isIdle(void) ; [ 0:06] 177 int isBlocked(void) ; [ 0:06] 178 void cleanup(void) [ 0:06] 179 { int i ; [ 0:06] 180 int tmp ; [ 0:06] 181 int tmp___0 ; [ 0:06] 182 int __cil_tmp4 ; [ 0:06] 183 [ 0:06] 184 { [ 0:06] 185 { [ 0:06] 186 timeShift(); [ 0:06] 187 i = 0; [ 0:06] 188 } [ 0:06] 189 { [ 0:06] 190 while (1) { [ 0:06] 191 while_0_continue: /* CIL Label */ ; [ 0:06] 192 { [ 0:06] 193 __cil_tmp4 = cleanupTimeShifts - 1; [ 0:06] 194 if (i < __cil_tmp4) { [ 0:06] 195 { [ 0:06] 196 tmp___0 = isBlocked(); [ 0:06] 197 } [ 0:06] 198 if (tmp___0 != 1) { [ 0:06] 199 [ 0:06] 200 } else { [ 0:06] 201 goto while_0_break; [ 0:06] 202 } [ 0:06] 203 } else { [ 0:06] 204 goto while_0_break; [ 0:06] 205 } [ 0:06] 206 } [ 0:06] 207 { [ 0:06] 208 tmp = isIdle(); [ 0:06] 209 } [ 0:06] 210 if (tmp) { [ 0:06] 211 return; [ 0:06] 212 } else { [ 0:06] 213 { [ 0:06] 214 timeShift(); [ 0:06] 215 } [ 0:06] 216 } [ 0:06] 217 i = i + 1; [ 0:06] 218 } [ 0:06] 219 while_0_break: /* CIL Label */ ; [ 0:06] 220 } [ 0:06] 221 return; [ 0:06] 222 } [ 0:06] 223 } [ 0:06] 224 void initTopDown(void) ; [ 0:06] 225 void initBottomUp(void) ; [ 0:06] 226 void randomSequenceOfActions(void) [ 0:06] 227 { int maxLength ; [ 0:06] 228 int tmp ; [ 0:06] 229 int counter ; [ 0:06] 230 int action ; [ 0:06] 231 int tmp___0 ; [ 0:06] 232 int origin ; [ 0:06] 233 int tmp___1 ; [ 0:06] 234 int tmp___2 ; [ 0:06] 235 [ 0:06] 236 { [ 0:06] 237 { [ 0:06] 238 maxLength = 4; [ 0:06] 239 tmp = __VERIFIER_nondet_int(); [ 0:06] 240 } [ 0:06] 241 if (tmp) { [ 0:06] 242 { [ 0:06] 243 initTopDown(); [ 0:06] 244 } [ 0:06] 245 } else { [ 0:06] 246 { [ 0:06] 247 initBottomUp(); [ 0:06] 248 } [ 0:06] 249 } [ 0:06] 250 counter = 0; [ 0:06] 251 { [ 0:06] 252 while (1) { [ 0:06] 253 while_1_continue: /* CIL Label */ ; [ 0:06] 254 if (counter < maxLength) { [ 0:06] 255 [ 0:06] 256 } else { [ 0:06] 257 goto while_1_break; [ 0:06] 258 } [ 0:06] 259 { [ 0:06] 260 counter = counter + 1; [ 0:06] 261 tmp___0 = get_nondetMinMax07(); [ 0:06] 262 action = tmp___0; [ 0:06] 263 } [ 0:06] 264 if (action < 6) { [ 0:06] 265 { [ 0:06] 266 tmp___1 = getOrigin(action); [ 0:06] 267 origin = tmp___1; [ 0:06] 268 initPersonOnFloor(action, origin); [ 0:06] 269 } [ 0:06] 270 } else { [ 0:06] 271 if (action == 6) { [ 0:06] 272 { [ 0:06] 273 timeShift(); [ 0:06] 274 } [ 0:06] 275 } else { [ 0:06] 276 if (action == 7) { [ 0:06] 277 { [ 0:06] 278 timeShift(); [ 0:06] 279 timeShift(); [ 0:06] 280 timeShift(); [ 0:06] 281 } [ 0:06] 282 } else { [ 0:06] 283 [ 0:06] 284 } [ 0:06] 285 } [ 0:06] 286 } [ 0:06] 287 { [ 0:06] 288 tmp___2 = isBlocked(); [ 0:06] 289 } [ 0:06] 290 if (tmp___2) { [ 0:06] 291 return; [ 0:06] 292 } else { [ 0:06] 293 [ 0:06] 294 } [ 0:06] 295 } [ 0:06] 296 while_1_break: /* CIL Label */ ; [ 0:06] 297 } [ 0:06] 298 { [ 0:06] 299 cleanup(); [ 0:06] 300 } [ 0:06] 301 return; [ 0:06] 302 } [ 0:06] 303 } [ 0:06] 304 void runTest_Simple(void) [ 0:06] 305 { [ 0:06] 306 [ 0:06] 307 { [ 0:06] 308 { [ 0:06] 309 bigMacCall(); [ 0:06] 310 angelinaCall(); [ 0:06] 311 cleanup(); [ 0:06] 312 } [ 0:06] 313 return; [ 0:06] 314 } [ 0:06] 315 } [ 0:06] 316 void Specification1(void) [ 0:06] 317 { [ 0:06] 318 [ 0:06] 319 { [ 0:06] 320 { [ 0:06] 321 bigMacCall(); [ 0:06] 322 angelinaCall(); [ 0:06] 323 cleanup(); [ 0:06] 324 } [ 0:06] 325 return; [ 0:06] 326 } [ 0:06] 327 } [ 0:06] 328 void Specification2(void) [ 0:06] 329 { [ 0:06] 330 [ 0:06] 331 { [ 0:06] 332 { [ 0:06] 333 bigMacCall(); [ 0:06] 334 cleanup(); [ 0:06] 335 } [ 0:06] 336 return; [ 0:06] 337 } [ 0:06] 338 } [ 0:06] 339 void Specification3(void) [ 0:06] 340 { [ 0:06] 341 [ 0:06] 342 { [ 0:06] 343 { [ 0:06] 344 bobCall(); [ 0:06] 345 timeShift(); [ 0:06] 346 timeShift(); [ 0:06] 347 timeShift(); [ 0:06] 348 timeShift(); [ 0:06] 349 timeShift(); [ 0:06] 350 bobCall(); [ 0:06] 351 cleanup(); [ 0:06] 352 } [ 0:06] 353 return; [ 0:06] 354 } [ 0:06] 355 } [ 0:06] 356 void setup(void) [ 0:06] 357 { [ 0:06] 358 [ 0:06] 359 { [ 0:06] 360 return; [ 0:06] 361 } [ 0:06] 362 } [ 0:06] 363 void __utac_acc__Specification2_spec__1(void) ; [ 0:06] 364 void __utac_acc__Specification2_spec__4(void) ; [ 0:06] 365 void test(void) ; [ 0:06] 366 void runTest(void) [ 0:06] 367 { [ 0:06] 368 [ 0:06] 369 { [ 0:06] 370 { [ 0:06] 371 __utac_acc__Specification2_spec__1(); [ 0:06] 372 test(); [ 0:06] 373 __utac_acc__Specification2_spec__4(); [ 0:06] 374 } [ 0:06] 375 return; [ 0:06] 376 } [ 0:06] 377 } [ 0:06] 378 void select_helpers(void) ; [ 0:06] 379 void select_features(void) ; [ 0:06] 380 int valid_product(void) ; [ 0:06] 381 int main(void) [ 0:06] 382 { int retValue_acc ; [ 0:06] 383 int tmp ; [ 0:06] 384 [ 0:06] 385 { [ 0:06] 386 { [ 0:06] 387 select_helpers(); [ 0:06] 388 select_features(); [ 0:06] 389 tmp = valid_product(); [ 0:06] 390 } [ 0:06] 391 if (tmp) { [ 0:06] 392 { [ 0:06] 393 setup(); [ 0:06] 394 runTest(); [ 0:06] 395 } [ 0:06] 396 } else { [ 0:06] 397 [ 0:06] 398 } [ 0:06] 399 retValue_acc = 0; [ 0:06] 400 return (retValue_acc); [ 0:06] 401 return (retValue_acc); [ 0:06] 402 } [ 0:06] 403 } [ 0:06] 404 #pragma merger(0,"Elevator.i","") [ 0:06] 405 extern int printf(char const * __restrict __format , ...) ; [ 0:06] 406 int getWeight(int person ) ; [ 0:06] 407 int getDestination(int person ) ; [ 0:06] 408 void enterElevator(int p ) ; [ 0:06] 409 int isFloorCalling(int floorID ) ; [ 0:06] 410 void resetCallOnFloor(int floorID ) ; [ 0:06] 411 int isPersonOnFloor(int person , int floor ) ; [ 0:06] 412 void removePersonFromFloor(int person , int floor ) ; [ 0:06] 413 int isTopFloor(int floorID ) ; [ 0:06] 414 void initFloors(void) ; [ 0:06] 415 void printState(void) ; [ 0:06] 416 int isEmpty(void) ; [ 0:06] 417 int isAnyLiftButtonPressed(void) ; [ 0:06] 418 int buttonForFloorIsPressed(int floorID ) ; [ 0:06] 419 int areDoorsOpen(void) ; [ 0:06] 420 int getCurrentFloorID(void) ; [ 0:06] 421 int weight = 0; [ 0:06] 422 int maximumWeight = 100; [ 0:06] 423 int blocked = 0; [ 0:06] 424 int currentHeading = 1; [ 0:06] 425 int currentFloorID = 0; [ 0:06] 426 int persons_0 ; [ 0:06] 427 int persons_1 ; [ 0:06] 428 int persons_2 ; [ 0:06] 429 int persons_3 ; [ 0:06] 430 int persons_4 ; [ 0:06] 431 int persons_5 ; [ 0:06] 432 int doorState = 1; [ 0:06] 433 int floorButtons_0 ; [ 0:06] 434 int floorButtons_1 ; [ 0:06] 435 int floorButtons_2 ; [ 0:06] 436 int floorButtons_3 ; [ 0:06] 437 int floorButtons_4 ; [ 0:06] 438 void initTopDown(void) [ 0:06] 439 { [ 0:06] 440 [ 0:06] 441 { [ 0:06] 442 { [ 0:06] 443 currentFloorID = 4; [ 0:06] 444 currentHeading = 0; [ 0:06] 445 floorButtons_0 = 0; [ 0:06] 446 floorButtons_1 = 0; [ 0:06] 447 floorButtons_2 = 0; [ 0:06] 448 floorButtons_3 = 0; [ 0:06] 449 floorButtons_4 = 0; [ 0:06] 450 persons_0 = 0; [ 0:06] 451 persons_1 = 0; [ 0:06] 452 persons_2 = 0; [ 0:06] 453 persons_3 = 0; [ 0:06] 454 persons_4 = 0; [ 0:06] 455 persons_5 = 0; [ 0:06] 456 initFloors(); [ 0:06] 457 } [ 0:06] 458 return; [ 0:06] 459 } [ 0:06] 460 } [ 0:06] 461 void initBottomUp(void) [ 0:06] 462 { [ 0:06] 463 [ 0:06] 464 { [ 0:06] 465 { [ 0:06] 466 currentFloorID = 0; [ 0:06] 467 currentHeading = 1; [ 0:06] 468 floorButtons_0 = 0; [ 0:06] 469 floorButtons_1 = 0; [ 0:06] 470 floorButtons_2 = 0; [ 0:06] 471 floorButtons_3 = 0; [ 0:06] 472 floorButtons_4 = 0; [ 0:06] 473 persons_0 = 0; [ 0:06] 474 persons_1 = 0; [ 0:06] 475 persons_2 = 0; [ 0:06] 476 persons_3 = 0; [ 0:06] 477 persons_4 = 0; [ 0:06] 478 persons_5 = 0; [ 0:06] 479 initFloors(); [ 0:06] 480 } [ 0:06] 481 return; [ 0:06] 482 } [ 0:06] 483 } [ 0:06] 484 int isBlocked(void) [ 0:06] 485 { int retValue_acc ; [ 0:06] 486 [ 0:06] 487 { [ 0:06] 488 retValue_acc = blocked; [ 0:06] 489 return (retValue_acc); [ 0:06] 490 return (retValue_acc); [ 0:06] 491 } [ 0:06] 492 } [ 0:06] 493 void enterElevator__wrappee__base(int p ) [ 0:06] 494 { [ 0:06] 495 [ 0:06] 496 { [ 0:06] 497 if (p == 0) { [ 0:06] 498 persons_0 = 1; [ 0:06] 499 } else { [ 0:06] 500 if (p == 1) { [ 0:06] 501 persons_1 = 1; [ 0:06] 502 } else { [ 0:06] 503 if (p == 2) { [ 0:06] 504 persons_2 = 1; [ 0:06] 505 } else { [ 0:06] 506 if (p == 3) { [ 0:06] 507 persons_3 = 1; [ 0:06] 508 } else { [ 0:06] 509 if (p == 4) { [ 0:06] 510 persons_4 = 1; [ 0:06] 511 } else { [ 0:06] 512 if (p == 5) { [ 0:06] 513 persons_5 = 1; [ 0:06] 514 } else { [ 0:06] 515 [ 0:06] 516 } [ 0:06] 517 } [ 0:06] 518 } [ 0:06] 519 } [ 0:06] 520 } [ 0:06] 521 } [ 0:06] 522 return; [ 0:06] 523 } [ 0:06] 524 } [ 0:06] 525 void enterElevator(int p ) [ 0:06] 526 { int tmp ; [ 0:06] 527 [ 0:06] 528 { [ 0:06] 529 { [ 0:06] 530 enterElevator__wrappee__base(p); [ 0:06] 531 tmp = getWeight(p); [ 0:06] 532 weight = weight + tmp; [ 0:06] 533 } [ 0:06] 534 return; [ 0:06] 535 } [ 0:06] 536 } [ 0:06] 537 void leaveElevator__wrappee__base(int p ) [ 0:06] 538 { [ 0:06] 539 [ 0:06] 540 { [ 0:06] 541 if (p == 0) { [ 0:06] 542 persons_0 = 0; [ 0:06] 543 } else { [ 0:06] 544 if (p == 1) { [ 0:06] 545 persons_1 = 0; [ 0:06] 546 } else { [ 0:06] 547 if (p == 2) { [ 0:06] 548 persons_2 = 0; [ 0:06] 549 } else { [ 0:06] 550 if (p == 3) { [ 0:06] 551 persons_3 = 0; [ 0:06] 552 } else { [ 0:06] 553 if (p == 4) { [ 0:06] 554 persons_4 = 0; [ 0:06] 555 } else { [ 0:06] 556 if (p == 5) { [ 0:06] 557 persons_5 = 0; [ 0:06] 558 } else { [ 0:06] 559 [ 0:06] 560 } [ 0:06] 561 } [ 0:06] 562 } [ 0:06] 563 } [ 0:06] 564 } [ 0:06] 565 } [ 0:06] 566 return; [ 0:06] 567 } [ 0:06] 568 } [ 0:06] 569 void leaveElevator__wrappee__weight(int p ) [ 0:06] 570 { int tmp ; [ 0:06] 571 [ 0:06] 572 { [ 0:06] 573 { [ 0:06] 574 leaveElevator__wrappee__base(p); [ 0:06] 575 tmp = getWeight(p); [ 0:06] 576 weight = weight - tmp; [ 0:06] 577 } [ 0:06] 578 return; [ 0:06] 579 } [ 0:06] 580 } [ 0:06] 581 void leaveElevator(int p ) [ 0:06] 582 { int tmp ; [ 0:06] 583 [ 0:06] 584 { [ 0:06] 585 { [ 0:06] 586 leaveElevator__wrappee__weight(p); [ 0:06] 587 tmp = isEmpty(); [ 0:06] 588 } [ 0:06] 589 if (tmp) { [ 0:06] 590 floorButtons_0 = 0; [ 0:06] 591 floorButtons_1 = 0; [ 0:06] 592 floorButtons_2 = 0; [ 0:06] 593 floorButtons_3 = 0; [ 0:06] 594 floorButtons_4 = 0; [ 0:06] 595 } else { [ 0:06] 596 [ 0:06] 597 } [ 0:06] 598 return; [ 0:06] 599 } [ 0:06] 600 } [ 0:06] 601 void __utac_acc__Specification2_spec__2(int floor ) ; [ 0:06] 602 void pressInLiftFloorButton(int floorID ) [ 0:06] 603 { int __utac__ad__arg1 ; [ 0:06] 604 [ 0:06] 605 { [ 0:06] 606 { [ 0:06] 607 __utac__ad__arg1 = floorID; [ 0:06] 608 __utac_acc__Specification2_spec__2(__utac__ad__arg1); [ 0:06] 609 } [ 0:06] 610 if (floorID == 0) { [ 0:06] 611 floorButtons_0 = 1; [ 0:06] 612 } else { [ 0:06] 613 if (floorID == 1) { [ 0:06] 614 floorButtons_1 = 1; [ 0:06] 615 } else { [ 0:06] 616 if (floorID == 2) { [ 0:06] 617 floorButtons_2 = 1; [ 0:06] 618 } else { [ 0:06] 619 if (floorID == 3) { [ 0:06] 620 floorButtons_3 = 1; [ 0:06] 621 } else { [ 0:06] 622 if (floorID == 4) { [ 0:06] 623 floorButtons_4 = 1; [ 0:06] 624 } else { [ 0:06] 625 [ 0:06] 626 } [ 0:06] 627 } [ 0:06] 628 } [ 0:06] 629 } [ 0:06] 630 } [ 0:06] 631 return; [ 0:06] 632 } [ 0:06] 633 } [ 0:06] 634 void resetFloorButton(int floorID ) [ 0:06] 635 { [ 0:06] 636 [ 0:06] 637 { [ 0:06] 638 if (floorID == 0) { [ 0:06] 639 floorButtons_0 = 0; [ 0:06] 640 } else { [ 0:06] 641 if (floorID == 1) { [ 0:06] 642 floorButtons_1 = 0; [ 0:06] 643 } else { [ 0:06] 644 if (floorID == 2) { [ 0:06] 645 floorButtons_2 = 0; [ 0:06] 646 } else { [ 0:06] 647 if (floorID == 3) { [ 0:06] 648 floorButtons_3 = 0; [ 0:06] 649 } else { [ 0:06] 650 if (floorID == 4) { [ 0:06] 651 floorButtons_4 = 0; [ 0:06] 652 } else { [ 0:06] 653 [ 0:06] 654 } [ 0:06] 655 } [ 0:06] 656 } [ 0:06] 657 } [ 0:06] 658 } [ 0:06] 659 return; [ 0:06] 660 } [ 0:06] 661 } [ 0:06] 662 int getCurrentFloorID(void) [ 0:06] 663 { int retValue_acc ; [ 0:06] 664 [ 0:06] 665 { [ 0:06] 666 retValue_acc = currentFloorID; [ 0:06] 667 return (retValue_acc); [ 0:06] 668 return (retValue_acc); [ 0:06] 669 } [ 0:06] 670 } [ 0:06] 671 int areDoorsOpen(void) [ 0:06] 672 { int retValue_acc ; [ 0:06] 673 [ 0:06] 674 { [ 0:06] 675 retValue_acc = doorState; [ 0:06] 676 return (retValue_acc); [ 0:06] 677 return (retValue_acc); [ 0:06] 678 } [ 0:06] 679 } [ 0:06] 680 int buttonForFloorIsPressed(int floorID ) [ 0:06] 681 { int retValue_acc ; [ 0:06] 682 [ 0:06] 683 { [ 0:06] 684 if (floorID == 0) { [ 0:06] 685 retValue_acc = floorButtons_0; [ 0:06] 686 return (retValue_acc); [ 0:06] 687 } else { [ 0:06] 688 if (floorID == 1) { [ 0:06] 689 retValue_acc = floorButtons_1; [ 0:06] 690 return (retValue_acc); [ 0:06] 691 } else { [ 0:06] 692 if (floorID == 2) { [ 0:06] 693 retValue_acc = floorButtons_2; [ 0:06] 694 return (retValue_acc); [ 0:06] 695 } else { [ 0:06] 696 if (floorID == 3) { [ 0:06] 697 retValue_acc = floorButtons_3; [ 0:06] 698 return (retValue_acc); [ 0:06] 699 } else { [ 0:06] 700 if (floorID == 4) { [ 0:06] 701 retValue_acc = floorButtons_4; [ 0:06] 702 return (retValue_acc); [ 0:06] 703 } else { [ 0:06] 704 retValue_acc = 0; [ 0:06] 705 return (retValue_acc); [ 0:06] 706 } [ 0:06] 707 } [ 0:06] 708 } [ 0:06] 709 } [ 0:06] 710 } [ 0:06] 711 return (retValue_acc); [ 0:06] 712 } [ 0:06] 713 } [ 0:06] 714 int getCurrentHeading(void) [ 0:06] 715 { int retValue_acc ; [ 0:06] 716 [ 0:06] 717 { [ 0:06] 718 retValue_acc = currentHeading; [ 0:06] 719 return (retValue_acc); [ 0:06] 720 return (retValue_acc); [ 0:06] 721 } [ 0:06] 722 } [ 0:06] 723 int isEmpty(void) [ 0:06] 724 { int retValue_acc ; [ 0:06] 725 [ 0:06] 726 { [ 0:06] 727 if (persons_0 == 1) { [ 0:06] 728 retValue_acc = 0; [ 0:06] 729 return (retValue_acc); [ 0:06] 730 } else { [ 0:06] 731 if (persons_1 == 1) { [ 0:06] 732 retValue_acc = 0; [ 0:06] 733 return (retValue_acc); [ 0:06] 734 } else { [ 0:06] 735 if (persons_2 == 1) { [ 0:06] 736 retValue_acc = 0; [ 0:06] 737 return (retValue_acc); [ 0:06] 738 } else { [ 0:06] 739 if (persons_3 == 1) { [ 0:06] 740 retValue_acc = 0; [ 0:06] 741 return (retValue_acc); [ 0:06] 742 } else { [ 0:06] 743 if (persons_4 == 1) { [ 0:06] 744 retValue_acc = 0; [ 0:06] 745 return (retValue_acc); [ 0:06] 746 } else { [ 0:06] 747 if (persons_5 == 1) { [ 0:06] 748 retValue_acc = 0; [ 0:06] 749 return (retValue_acc); [ 0:06] 750 } else { [ 0:06] 751 [ 0:06] 752 } [ 0:06] 753 } [ 0:06] 754 } [ 0:06] 755 } [ 0:06] 756 } [ 0:06] 757 } [ 0:06] 758 retValue_acc = 1; [ 0:06] 759 return (retValue_acc); [ 0:06] 760 return (retValue_acc); [ 0:06] 761 } [ 0:06] 762 } [ 0:06] 763 int anyStopRequested(void) [ 0:06] 764 { int retValue_acc ; [ 0:06] 765 int tmp ; [ 0:06] 766 int tmp___0 ; [ 0:06] 767 int tmp___1 ; [ 0:06] 768 int tmp___2 ; [ 0:06] 769 int tmp___3 ; [ 0:06] 770 [ 0:06] 771 { [ 0:06] 772 { [ 0:06] 773 tmp___3 = isFloorCalling(0); [ 0:06] 774 } [ 0:06] 775 if (tmp___3) { [ 0:06] 776 retValue_acc = 1; [ 0:06] 777 return (retValue_acc); [ 0:06] 778 } else { [ 0:06] 779 if (floorButtons_0) { [ 0:06] 780 retValue_acc = 1; [ 0:06] 781 return (retValue_acc); [ 0:06] 782 } else { [ 0:06] 783 { [ 0:06] 784 tmp___2 = isFloorCalling(1); [ 0:06] 785 } [ 0:06] 786 if (tmp___2) { [ 0:06] 787 retValue_acc = 1; [ 0:06] 788 return (retValue_acc); [ 0:06] 789 } else { [ 0:06] 790 if (floorButtons_1) { [ 0:06] 791 retValue_acc = 1; [ 0:06] 792 return (retValue_acc); [ 0:06] 793 } else { [ 0:06] 794 { [ 0:06] 795 tmp___1 = isFloorCalling(2); [ 0:06] 796 } [ 0:06] 797 if (tmp___1) { [ 0:06] 798 retValue_acc = 1; [ 0:06] 799 return (retValue_acc); [ 0:06] 800 } else { [ 0:06] 801 if (floorButtons_2) { [ 0:06] 802 retValue_acc = 1; [ 0:06] 803 return (retValue_acc); [ 0:06] 804 } else { [ 0:06] 805 { [ 0:06] 806 tmp___0 = isFloorCalling(3); [ 0:06] 807 } [ 0:06] 808 if (tmp___0) { [ 0:06] 809 retValue_acc = 1; [ 0:06] 810 return (retValue_acc); [ 0:06] 811 } else { [ 0:06] 812 if (floorButtons_3) { [ 0:06] 813 retValue_acc = 1; [ 0:06] 814 return (retValue_acc); [ 0:06] 815 } else { [ 0:06] 816 { [ 0:06] 817 tmp = isFloorCalling(4); [ 0:06] 818 } [ 0:06] 819 if (tmp) { [ 0:06] 820 retValue_acc = 1; [ 0:06] 821 return (retValue_acc); [ 0:06] 822 } else { [ 0:06] 823 if (floorButtons_4) { [ 0:06] 824 retValue_acc = 1; [ 0:06] 825 return (retValue_acc); [ 0:06] 826 } else { [ 0:06] 827 [ 0:06] 828 } [ 0:06] 829 } [ 0:06] 830 } [ 0:06] 831 } [ 0:06] 832 } [ 0:06] 833 } [ 0:06] 834 } [ 0:06] 835 } [ 0:06] 836 } [ 0:06] 837 } [ 0:06] 838 retValue_acc = 0; [ 0:06] 839 return (retValue_acc); [ 0:06] 840 return (retValue_acc); [ 0:06] 841 } [ 0:06] 842 } [ 0:06] 843 int isIdle(void) [ 0:06] 844 { int retValue_acc ; [ 0:06] 845 int tmp ; [ 0:06] 846 [ 0:06] 847 { [ 0:06] 848 { [ 0:06] 849 tmp = anyStopRequested(); [ 0:06] 850 retValue_acc = tmp == 0; [ 0:06] 851 } [ 0:06] 852 return (retValue_acc); [ 0:06] 853 return (retValue_acc); [ 0:06] 854 } [ 0:06] 855 } [ 0:06] 856 int stopRequestedInDirection(int dir , int respectFloorCalls , int respectInLiftCalls ) [ 0:06] 857 { int retValue_acc ; [ 0:06] 858 int tmp ; [ 0:06] 859 int tmp___0 ; [ 0:06] 860 int tmp___1 ; [ 0:06] 861 int tmp___2 ; [ 0:06] 862 int tmp___3 ; [ 0:06] 863 int tmp___4 ; [ 0:06] 864 int tmp___5 ; [ 0:06] 865 int tmp___6 ; [ 0:06] 866 int tmp___7 ; [ 0:06] 867 int tmp___8 ; [ 0:06] 868 int tmp___9 ; [ 0:06] 869 [ 0:06] 870 { [ 0:06] 871 if (dir == 1) { [ 0:06] 872 { [ 0:06] 873 tmp = isTopFloor(currentFloorID); [ 0:06] 874 } [ 0:06] 875 if (tmp) { [ 0:06] 876 retValue_acc = 0; [ 0:06] 877 return (retValue_acc); [ 0:06] 878 } else { [ 0:06] 879 [ 0:06] 880 } [ 0:06] 881 if (currentFloorID < 0) { [ 0:06] 882 if (respectFloorCalls) { [ 0:06] 883 { [ 0:06] 884 tmp___4 = isFloorCalling(0); [ 0:06] 885 } [ 0:06] 886 if (tmp___4) { [ 0:06] 887 retValue_acc = 1; [ 0:06] 888 return (retValue_acc); [ 0:06] 889 } else { [ 0:06] 890 goto _L___16; [ 0:06] 891 } [ 0:06] 892 } else { [ 0:06] 893 goto _L___16; [ 0:06] 894 } [ 0:06] 895 } else { [ 0:06] 896 _L___16: /* CIL Label */ [ 0:06] 897 if (currentFloorID < 0) { [ 0:06] 898 if (respectInLiftCalls) { [ 0:06] 899 if (floorButtons_0) { [ 0:06] 900 retValue_acc = 1; [ 0:06] 901 return (retValue_acc); [ 0:06] 902 } else { [ 0:06] 903 goto _L___14; [ 0:06] 904 } [ 0:06] 905 } else { [ 0:06] 906 goto _L___14; [ 0:06] 907 } [ 0:06] 908 } else { [ 0:06] 909 _L___14: /* CIL Label */ [ 0:06] 910 if (currentFloorID < 1) { [ 0:06] 911 if (respectFloorCalls) { [ 0:06] 912 { [ 0:06] 913 tmp___3 = isFloorCalling(1); [ 0:06] 914 } [ 0:06] 915 if (tmp___3) { [ 0:06] 916 retValue_acc = 1; [ 0:06] 917 return (retValue_acc); [ 0:06] 918 } else { [ 0:06] 919 goto _L___12; [ 0:06] 920 } [ 0:06] 921 } else { [ 0:06] 922 goto _L___12; [ 0:06] 923 } [ 0:06] 924 } else { [ 0:06] 925 _L___12: /* CIL Label */ [ 0:06] 926 if (currentFloorID < 1) { [ 0:06] 927 if (respectInLiftCalls) { [ 0:06] 928 if (floorButtons_1) { [ 0:06] 929 retValue_acc = 1; [ 0:06] 930 return (retValue_acc); [ 0:06] 931 } else { [ 0:06] 932 goto _L___10; [ 0:06] 933 } [ 0:06] 934 } else { [ 0:06] 935 goto _L___10; [ 0:06] 936 } [ 0:06] 937 } else { [ 0:06] 938 _L___10: /* CIL Label */ [ 0:06] 939 if (currentFloorID < 2) { [ 0:06] 940 if (respectFloorCalls) { [ 0:06] 941 { [ 0:06] 942 tmp___2 = isFloorCalling(2); [ 0:06] 943 } [ 0:06] 944 if (tmp___2) { [ 0:06] 945 retValue_acc = 1; [ 0:06] 946 return (retValue_acc); [ 0:06] 947 } else { [ 0:06] 948 goto _L___8; [ 0:06] 949 } [ 0:06] 950 } else { [ 0:06] 951 goto _L___8; [ 0:06] 952 } [ 0:06] 953 } else { [ 0:06] 954 _L___8: /* CIL Label */ [ 0:06] 955 if (currentFloorID < 2) { [ 0:06] 956 if (respectInLiftCalls) { [ 0:06] 957 if (floorButtons_2) { [ 0:06] 958 retValue_acc = 1; [ 0:06] 959 return (retValue_acc); [ 0:06] 960 } else { [ 0:06] 961 goto _L___6; [ 0:06] 962 } [ 0:06] 963 } else { [ 0:06] 964 goto _L___6; [ 0:06] 965 } [ 0:06] 966 } else { [ 0:06] 967 _L___6: /* CIL Label */ [ 0:06] 968 if (currentFloorID < 3) { [ 0:06] 969 if (respectFloorCalls) { [ 0:06] 970 { [ 0:06] 971 tmp___1 = isFloorCalling(3); [ 0:06] 972 } [ 0:06] 973 if (tmp___1) { [ 0:06] 974 retValue_acc = 1; [ 0:06] 975 return (retValue_acc); [ 0:06] 976 } else { [ 0:06] 977 goto _L___4; [ 0:06] 978 } [ 0:06] 979 } else { [ 0:06] 980 goto _L___4; [ 0:06] 981 } [ 0:06] 982 } else { [ 0:06] 983 _L___4: /* CIL Label */ [ 0:06] 984 if (currentFloorID < 3) { [ 0:06] 985 if (respectInLiftCalls) { [ 0:06] 986 if (floorButtons_3) { [ 0:06] 987 retValue_acc = 1; [ 0:06] 988 return (retValue_acc); [ 0:06] 989 } else { [ 0:06] 990 goto _L___2; [ 0:06] 991 } [ 0:06] 992 } else { [ 0:06] 993 goto _L___2; [ 0:06] 994 } [ 0:06] 995 } else { [ 0:06] 996 _L___2: /* CIL Label */ [ 0:06] 997 if (currentFloorID < 4) { [ 0:06] 998 if (respectFloorCalls) { [ 0:06] 999 { [ 0:06] 1000 tmp___0 = isFloorCalling(4); [ 0:06] 1001 } [ 0:06] 1002 if (tmp___0) { [ 0:06] 1003 retValue_acc = 1; [ 0:06] 1004 return (retValue_acc); [ 0:06] 1005 } else { [ 0:06] 1006 goto _L___0; [ 0:06] 1007 } [ 0:06] 1008 } else { [ 0:06] 1009 goto _L___0; [ 0:06] 1010 } [ 0:06] 1011 } else { [ 0:06] 1012 _L___0: /* CIL Label */ [ 0:06] 1013 if (currentFloorID < 4) { [ 0:06] 1014 if (respectInLiftCalls) { [ 0:06] 1015 if (floorButtons_4) { [ 0:06] 1016 retValue_acc = 1; [ 0:06] 1017 return (retValue_acc); [ 0:06] 1018 } else { [ 0:06] 1019 retValue_acc = 0; [ 0:06] 1020 return (retValue_acc); [ 0:06] 1021 } [ 0:06] 1022 } else { [ 0:06] 1023 retValue_acc = 0; [ 0:06] 1024 return (retValue_acc); [ 0:06] 1025 } [ 0:06] 1026 } else { [ 0:06] 1027 retValue_acc = 0; [ 0:06] 1028 return (retValue_acc); [ 0:06] 1029 } [ 0:06] 1030 } [ 0:06] 1031 } [ 0:06] 1032 } [ 0:06] 1033 } [ 0:06] 1034 } [ 0:06] 1035 } [ 0:06] 1036 } [ 0:06] 1037 } [ 0:06] 1038 } [ 0:06] 1039 } else { [ 0:06] 1040 if (currentFloorID == 0) { [ 0:06] 1041 retValue_acc = 0; [ 0:06] 1042 return (retValue_acc); [ 0:06] 1043 } else { [ 0:06] 1044 [ 0:06] 1045 } [ 0:06] 1046 if (currentFloorID > 0) { [ 0:06] 1047 if (respectFloorCalls) { [ 0:06] 1048 { [ 0:06] 1049 tmp___9 = isFloorCalling(0); [ 0:06] 1050 } [ 0:06] 1051 if (tmp___9) { [ 0:06] 1052 retValue_acc = 1; [ 0:06] 1053 return (retValue_acc); [ 0:06] 1054 } else { [ 0:06] 1055 goto _L___34; [ 0:06] 1056 } [ 0:06] 1057 } else { [ 0:06] 1058 goto _L___34; [ 0:06] 1059 } [ 0:06] 1060 } else { [ 0:06] 1061 _L___34: /* CIL Label */ [ 0:06] 1062 if (currentFloorID > 0) { [ 0:06] 1063 if (respectInLiftCalls) { [ 0:06] 1064 if (floorButtons_0) { [ 0:06] 1065 retValue_acc = 1; [ 0:06] 1066 return (retValue_acc); [ 0:06] 1067 } else { [ 0:06] 1068 goto _L___32; [ 0:06] 1069 } [ 0:06] 1070 } else { [ 0:06] 1071 goto _L___32; [ 0:06] 1072 } [ 0:06] 1073 } else { [ 0:06] 1074 _L___32: /* CIL Label */ [ 0:06] 1075 if (currentFloorID > 1) { [ 0:06] 1076 if (respectFloorCalls) { [ 0:06] 1077 { [ 0:06] 1078 tmp___8 = isFloorCalling(1); [ 0:06] 1079 } [ 0:06] 1080 if (tmp___8) { [ 0:06] 1081 retValue_acc = 1; [ 0:06] 1082 return (retValue_acc); [ 0:06] 1083 } else { [ 0:06] 1084 goto _L___30; [ 0:06] 1085 } [ 0:06] 1086 } else { [ 0:06] 1087 goto _L___30; [ 0:06] 1088 } [ 0:06] 1089 } else { [ 0:06] 1090 _L___30: /* CIL Label */ [ 0:06] 1091 if (currentFloorID > 1) { [ 0:06] 1092 if (respectInLiftCalls) { [ 0:06] 1093 if (floorButtons_1) { [ 0:06] 1094 retValue_acc = 1; [ 0:06] 1095 return (retValue_acc); [ 0:06] 1096 } else { [ 0:06] 1097 goto _L___28; [ 0:06] 1098 } [ 0:06] 1099 } else { [ 0:06] 1100 goto _L___28; [ 0:06] 1101 } [ 0:06] 1102 } else { [ 0:06] 1103 _L___28: /* CIL Label */ [ 0:06] 1104 if (currentFloorID > 2) { [ 0:06] 1105 if (respectFloorCalls) { [ 0:06] 1106 { [ 0:06] 1107 tmp___7 = isFloorCalling(2); [ 0:06] 1108 } [ 0:06] 1109 if (tmp___7) { [ 0:06] 1110 retValue_acc = 1; [ 0:06] 1111 return (retValue_acc); [ 0:06] 1112 } else { [ 0:06] 1113 goto _L___26; [ 0:06] 1114 } [ 0:06] 1115 } else { [ 0:06] 1116 goto _L___26; [ 0:06] 1117 } [ 0:06] 1118 } else { [ 0:06] 1119 _L___26: /* CIL Label */ [ 0:06] 1120 if (currentFloorID > 2) { [ 0:06] 1121 if (respectInLiftCalls) { [ 0:06] 1122 if (floorButtons_2) { [ 0:06] 1123 retValue_acc = 1; [ 0:06] 1124 return (retValue_acc); [ 0:06] 1125 } else { [ 0:06] 1126 goto _L___24; [ 0:06] 1127 } [ 0:06] 1128 } else { [ 0:06] 1129 goto _L___24; [ 0:06] 1130 } [ 0:06] 1131 } else { [ 0:06] 1132 _L___24: /* CIL Label */ [ 0:06] 1133 if (currentFloorID > 3) { [ 0:06] 1134 if (respectFloorCalls) { [ 0:06] 1135 { [ 0:06] 1136 tmp___6 = isFloorCalling(3); [ 0:06] 1137 } [ 0:06] 1138 if (tmp___6) { [ 0:06] 1139 retValue_acc = 1; [ 0:06] 1140 return (retValue_acc); [ 0:06] 1141 } else { [ 0:06] 1142 goto _L___22; [ 0:06] 1143 } [ 0:06] 1144 } else { [ 0:06] 1145 goto _L___22; [ 0:06] 1146 } [ 0:06] 1147 } else { [ 0:06] 1148 _L___22: /* CIL Label */ [ 0:06] 1149 if (currentFloorID > 3) { [ 0:06] 1150 if (respectInLiftCalls) { [ 0:06] 1151 if (floorButtons_3) { [ 0:06] 1152 retValue_acc = 1; [ 0:06] 1153 return (retValue_acc); [ 0:06] 1154 } else { [ 0:06] 1155 goto _L___20; [ 0:06] 1156 } [ 0:06] 1157 } else { [ 0:06] 1158 goto _L___20; [ 0:06] 1159 } [ 0:06] 1160 } else { [ 0:06] 1161 _L___20: /* CIL Label */ [ 0:06] 1162 if (currentFloorID > 4) { [ 0:06] 1163 if (respectFloorCalls) { [ 0:06] 1164 { [ 0:06] 1165 tmp___5 = isFloorCalling(4); [ 0:06] 1166 } [ 0:06] 1167 if (tmp___5) { [ 0:06] 1168 retValue_acc = 1; [ 0:06] 1169 return (retValue_acc); [ 0:06] 1170 } else { [ 0:06] 1171 goto _L___18; [ 0:06] 1172 } [ 0:06] 1173 } else { [ 0:06] 1174 goto _L___18; [ 0:06] 1175 } [ 0:06] 1176 } else { [ 0:06] 1177 _L___18: /* CIL Label */ [ 0:06] 1178 if (currentFloorID > 4) { [ 0:06] 1179 if (respectInLiftCalls) { [ 0:06] 1180 if (floorButtons_4) { [ 0:06] 1181 retValue_acc = 1; [ 0:06] 1182 return (retValue_acc); [ 0:06] 1183 } else { [ 0:06] 1184 retValue_acc = 0; [ 0:06] 1185 return (retValue_acc); [ 0:06] 1186 } [ 0:06] 1187 } else { [ 0:06] 1188 retValue_acc = 0; [ 0:06] 1189 return (retValue_acc); [ 0:06] 1190 } [ 0:06] 1191 } else { [ 0:06] 1192 retValue_acc = 0; [ 0:06] 1193 return (retValue_acc); [ 0:06] 1194 } [ 0:06] 1195 } [ 0:06] 1196 } [ 0:06] 1197 } [ 0:06] 1198 } [ 0:06] 1199 } [ 0:06] 1200 } [ 0:06] 1201 } [ 0:06] 1202 } [ 0:06] 1203 } [ 0:06] 1204 } [ 0:06] 1205 return (retValue_acc); [ 0:06] 1206 } [ 0:06] 1207 } [ 0:06] 1208 int isAnyLiftButtonPressed(void) [ 0:06] 1209 { int retValue_acc ; [ 0:06] 1210 [ 0:06] 1211 { [ 0:06] 1212 if (floorButtons_0) { [ 0:06] 1213 retValue_acc = 1; [ 0:06] 1214 return (retValue_acc); [ 0:06] 1215 } else { [ 0:06] 1216 if (floorButtons_1) { [ 0:06] 1217 retValue_acc = 1; [ 0:06] 1218 return (retValue_acc); [ 0:06] 1219 } else { [ 0:06] 1220 if (floorButtons_2) { [ 0:06] 1221 retValue_acc = 1; [ 0:06] 1222 return (retValue_acc); [ 0:06] 1223 } else { [ 0:06] 1224 if (floorButtons_3) { [ 0:06] 1225 retValue_acc = 1; [ 0:06] 1226 return (retValue_acc); [ 0:06] 1227 } else { [ 0:06] 1228 if (floorButtons_4) { [ 0:06] 1229 retValue_acc = 1; [ 0:06] 1230 return (retValue_acc); [ 0:06] 1231 } else { [ 0:06] 1232 retValue_acc = 0; [ 0:06] 1233 return (retValue_acc); [ 0:06] 1234 } [ 0:06] 1235 } [ 0:06] 1236 } [ 0:06] 1237 } [ 0:06] 1238 } [ 0:06] 1239 return (retValue_acc); [ 0:06] 1240 } [ 0:06] 1241 } [ 0:06] 1242 void continueInDirection(int dir ) [ 0:06] 1243 { int tmp ; [ 0:06] 1244 [ 0:06] 1245 { [ 0:06] 1246 currentHeading = dir; [ 0:06] 1247 if (currentHeading == 1) { [ 0:06] 1248 { [ 0:06] 1249 tmp = isTopFloor(currentFloorID); [ 0:06] 1250 } [ 0:06] 1251 if (tmp) { [ 0:06] 1252 currentHeading = 0; [ 0:06] 1253 } else { [ 0:06] 1254 [ 0:06] 1255 } [ 0:06] 1256 } else { [ 0:06] 1257 if (currentFloorID == 0) { [ 0:06] 1258 currentHeading = 1; [ 0:06] 1259 } else { [ 0:06] 1260 [ 0:06] 1261 } [ 0:06] 1262 } [ 0:06] 1263 if (currentHeading == 1) { [ 0:06] 1264 currentFloorID = currentFloorID + 1; [ 0:06] 1265 } else { [ 0:06] 1266 currentFloorID = currentFloorID - 1; [ 0:06] 1267 } [ 0:06] 1268 return; [ 0:06] 1269 } [ 0:06] 1270 } [ 0:06] 1271 int stopRequestedAtCurrentFloor(void) [ 0:06] 1272 { int retValue_acc ; [ 0:06] 1273 int tmp ; [ 0:06] 1274 int tmp___0 ; [ 0:06] 1275 [ 0:06] 1276 { [ 0:06] 1277 { [ 0:06] 1278 tmp___0 = isFloorCalling(currentFloorID); [ 0:06] 1279 } [ 0:06] 1280 if (tmp___0) { [ 0:06] 1281 retValue_acc = 1; [ 0:06] 1282 return (retValue_acc); [ 0:06] 1283 } else { [ 0:06] 1284 { [ 0:06] 1285 tmp = buttonForFloorIsPressed(currentFloorID); [ 0:06] 1286 } [ 0:06] 1287 if (tmp) { [ 0:06] 1288 retValue_acc = 1; [ 0:06] 1289 return (retValue_acc); [ 0:06] 1290 } else { [ 0:06] 1291 retValue_acc = 0; [ 0:06] 1292 return (retValue_acc); [ 0:06] 1293 } [ 0:06] 1294 } [ 0:06] 1295 return (retValue_acc); [ 0:06] 1296 } [ 0:06] 1297 } [ 0:06] 1298 int getReverseHeading(int ofHeading ) [ 0:06] 1299 { int retValue_acc ; [ 0:06] 1300 [ 0:06] 1301 { [ 0:06] 1302 if (ofHeading == 0) { [ 0:06] 1303 retValue_acc = 1; [ 0:06] 1304 return (retValue_acc); [ 0:06] 1305 } else { [ 0:06] 1306 retValue_acc = 0; [ 0:06] 1307 return (retValue_acc); [ 0:06] 1308 } [ 0:06] 1309 return (retValue_acc); [ 0:06] 1310 } [ 0:06] 1311 } [ 0:06] 1312 void processWaitingOnFloor(int floorID ) [ 0:06] 1313 { int tmp ; [ 0:06] 1314 int tmp___0 ; [ 0:06] 1315 int tmp___1 ; [ 0:06] 1316 int tmp___2 ; [ 0:06] 1317 int tmp___3 ; [ 0:06] 1318 int tmp___4 ; [ 0:06] 1319 int tmp___5 ; [ 0:06] 1320 int tmp___6 ; [ 0:06] 1321 int tmp___7 ; [ 0:06] 1322 int tmp___8 ; [ 0:06] 1323 int tmp___9 ; [ 0:06] 1324 int tmp___10 ; [ 0:06] 1325 [ 0:06] 1326 { [ 0:06] 1327 { [ 0:06] 1328 tmp___0 = isPersonOnFloor(0, floorID); [ 0:06] 1329 } [ 0:06] 1330 if (tmp___0) { [ 0:06] 1331 { [ 0:06] 1332 removePersonFromFloor(0, floorID); [ 0:06] 1333 tmp = getDestination(0); [ 0:06] 1334 pressInLiftFloorButton(tmp); [ 0:06] 1335 enterElevator(0); [ 0:06] 1336 } [ 0:06] 1337 } else { [ 0:06] 1338 [ 0:06] 1339 } [ 0:06] 1340 { [ 0:06] 1341 tmp___2 = isPersonOnFloor(1, floorID); [ 0:06] 1342 } [ 0:06] 1343 if (tmp___2) { [ 0:06] 1344 { [ 0:06] 1345 removePersonFromFloor(1, floorID); [ 0:06] 1346 tmp___1 = getDestination(1); [ 0:06] 1347 pressInLiftFloorButton(tmp___1); [ 0:06] 1348 enterElevator(1); [ 0:06] 1349 } [ 0:06] 1350 } else { [ 0:06] 1351 [ 0:06] 1352 } [ 0:06] 1353 { [ 0:06] 1354 tmp___4 = isPersonOnFloor(2, floorID); [ 0:06] 1355 } [ 0:06] 1356 if (tmp___4) { [ 0:06] 1357 { [ 0:06] 1358 removePersonFromFloor(2, floorID); [ 0:06] 1359 tmp___3 = getDestination(2); [ 0:06] 1360 pressInLiftFloorButton(tmp___3); [ 0:06] 1361 enterElevator(2); [ 0:06] 1362 } [ 0:06] 1363 } else { [ 0:06] 1364 [ 0:06] 1365 } [ 0:06] 1366 { [ 0:06] 1367 tmp___6 = isPersonOnFloor(3, floorID); [ 0:06] 1368 } [ 0:06] 1369 if (tmp___6) { [ 0:06] 1370 { [ 0:06] 1371 removePersonFromFloor(3, floorID); [ 0:06] 1372 tmp___5 = getDestination(3); [ 0:06] 1373 pressInLiftFloorButton(tmp___5); [ 0:06] 1374 enterElevator(3); [ 0:06] 1375 } [ 0:06] 1376 } else { [ 0:06] 1377 [ 0:06] 1378 } [ 0:06] 1379 { [ 0:06] 1380 tmp___8 = isPersonOnFloor(4, floorID); [ 0:06] 1381 } [ 0:06] 1382 if (tmp___8) { [ 0:06] 1383 { [ 0:06] 1384 removePersonFromFloor(4, floorID); [ 0:06] 1385 tmp___7 = getDestination(4); [ 0:06] 1386 pressInLiftFloorButton(tmp___7); [ 0:06] 1387 enterElevator(4); [ 0:06] 1388 } [ 0:06] 1389 } else { [ 0:06] 1390 [ 0:06] 1391 } [ 0:06] 1392 { [ 0:06] 1393 tmp___10 = isPersonOnFloor(5, floorID); [ 0:06] 1394 } [ 0:06] 1395 if (tmp___10) { [ 0:06] 1396 { [ 0:06] 1397 removePersonFromFloor(5, floorID); [ 0:06] 1398 tmp___9 = getDestination(5); [ 0:06] 1399 pressInLiftFloorButton(tmp___9); [ 0:06] 1400 enterElevator(5); [ 0:06] 1401 } [ 0:06] 1402 } else { [ 0:06] 1403 [ 0:06] 1404 } [ 0:06] 1405 { [ 0:06] 1406 resetCallOnFloor(floorID); [ 0:06] 1407 } [ 0:06] 1408 return; [ 0:06] 1409 } [ 0:06] 1410 } [ 0:06] 1411 void timeShift__wrappee__empty(void) [ 0:06] 1412 { int tmp ; [ 0:06] 1413 int tmp___0 ; [ 0:06] 1414 int tmp___1 ; [ 0:06] 1415 int tmp___2 ; [ 0:06] 1416 int tmp___3 ; [ 0:06] 1417 int tmp___4 ; [ 0:06] 1418 int tmp___5 ; [ 0:06] 1419 int tmp___6 ; [ 0:06] 1420 int tmp___7 ; [ 0:06] 1421 int tmp___8 ; [ 0:06] 1422 int tmp___9 ; [ 0:06] 1423 [ 0:06] 1424 { [ 0:06] 1425 { [ 0:06] 1426 tmp___9 = stopRequestedAtCurrentFloor(); [ 0:06] 1427 } [ 0:06] 1428 if (tmp___9) { [ 0:06] 1429 doorState = 1; [ 0:06] 1430 if (persons_0) { [ 0:06] 1431 { [ 0:06] 1432 tmp = getDestination(0); [ 0:06] 1433 } [ 0:06] 1434 if (tmp == currentFloorID) { [ 0:06] 1435 { [ 0:06] 1436 leaveElevator(0); [ 0:06] 1437 } [ 0:06] 1438 } else { [ 0:06] 1439 [ 0:06] 1440 } [ 0:06] 1441 } else { [ 0:06] 1442 [ 0:06] 1443 } [ 0:06] 1444 if (persons_1) { [ 0:06] 1445 { [ 0:06] 1446 tmp___0 = getDestination(1); [ 0:06] 1447 } [ 0:06] 1448 if (tmp___0 == currentFloorID) { [ 0:06] 1449 { [ 0:06] 1450 leaveElevator(1); [ 0:06] 1451 } [ 0:06] 1452 } else { [ 0:06] 1453 [ 0:06] 1454 } [ 0:06] 1455 } else { [ 0:06] 1456 [ 0:06] 1457 } [ 0:06] 1458 if (persons_2) { [ 0:06] 1459 { [ 0:06] 1460 tmp___1 = getDestination(2); [ 0:06] 1461 } [ 0:06] 1462 if (tmp___1 == currentFloorID) { [ 0:06] 1463 { [ 0:06] 1464 leaveElevator(2); [ 0:06] 1465 } [ 0:06] 1466 } else { [ 0:06] 1467 [ 0:06] 1468 } [ 0:06] 1469 } else { [ 0:06] 1470 [ 0:06] 1471 } [ 0:06] 1472 if (persons_3) { [ 0:06] 1473 { [ 0:06] 1474 tmp___2 = getDestination(3); [ 0:06] 1475 } [ 0:06] 1476 if (tmp___2 == currentFloorID) { [ 0:06] 1477 { [ 0:06] 1478 leaveElevator(3); [ 0:06] 1479 } [ 0:06] 1480 } else { [ 0:06] 1481 [ 0:06] 1482 } [ 0:06] 1483 } else { [ 0:06] 1484 [ 0:06] 1485 } [ 0:06] 1486 if (persons_4) { [ 0:06] 1487 { [ 0:06] 1488 tmp___3 = getDestination(4); [ 0:06] 1489 } [ 0:06] 1490 if (tmp___3 == currentFloorID) { [ 0:06] 1491 { [ 0:06] 1492 leaveElevator(4); [ 0:06] 1493 } [ 0:06] 1494 } else { [ 0:06] 1495 [ 0:06] 1496 } [ 0:06] 1497 } else { [ 0:06] 1498 [ 0:06] 1499 } [ 0:06] 1500 if (persons_5) { [ 0:06] 1501 { [ 0:06] 1502 tmp___4 = getDestination(5); [ 0:06] 1503 } [ 0:06] 1504 if (tmp___4 == currentFloorID) { [ 0:06] 1505 { [ 0:06] 1506 leaveElevator(5); [ 0:06] 1507 } [ 0:06] 1508 } else { [ 0:06] 1509 [ 0:06] 1510 } [ 0:06] 1511 } else { [ 0:06] 1512 [ 0:06] 1513 } [ 0:06] 1514 { [ 0:06] 1515 processWaitingOnFloor(currentFloorID); [ 0:06] 1516 resetFloorButton(currentFloorID); [ 0:06] 1517 } [ 0:06] 1518 } else { [ 0:06] 1519 if (doorState == 1) { [ 0:06] 1520 doorState = 0; [ 0:06] 1521 } else { [ 0:06] 1522 [ 0:06] 1523 } [ 0:06] 1524 { [ 0:06] 1525 tmp___8 = stopRequestedInDirection(currentHeading, 1, 1); [ 0:06] 1526 } [ 0:06] 1527 if (tmp___8) { [ 0:06] 1528 { [ 0:06] 1529 continueInDirection(currentHeading); [ 0:06] 1530 } [ 0:06] 1531 } else { [ 0:06] 1532 { [ 0:06] 1533 tmp___6 = getReverseHeading(currentHeading); [ 0:06] 1534 tmp___7 = stopRequestedInDirection(tmp___6, 1, 1); [ 0:06] 1535 } [ 0:06] 1536 if (tmp___7) { [ 0:06] 1537 { [ 0:06] 1538 tmp___5 = getReverseHeading(currentHeading); [ 0:06] 1539 continueInDirection(tmp___5); [ 0:06] 1540 } [ 0:06] 1541 } else { [ 0:06] 1542 { [ 0:06] 1543 continueInDirection(currentHeading); [ 0:06] 1544 } [ 0:06] 1545 } [ 0:06] 1546 } [ 0:06] 1547 } [ 0:06] 1548 return; [ 0:06] 1549 } [ 0:06] 1550 } [ 0:06] 1551 void __utac_acc__Specification2_spec__3(void) ; [ 0:06] 1552 void timeShift(void) [ 0:06] 1553 { int tmp ; [ 0:06] 1554 [ 0:06] 1555 { [ 0:06] 1556 { [ 0:06] 1557 tmp = areDoorsOpen(); [ 0:06] 1558 } [ 0:06] 1559 if (tmp) { [ 0:06] 1560 if (weight > maximumWeight) { [ 0:06] 1561 blocked = 1; [ 0:06] 1562 } else { [ 0:06] 1563 { [ 0:06] 1564 blocked = 0; [ 0:06] 1565 timeShift__wrappee__empty(); [ 0:06] 1566 } [ 0:06] 1567 } [ 0:06] 1568 } else { [ 0:06] 1569 { [ 0:06] 1570 blocked = 0; [ 0:06] 1571 timeShift__wrappee__empty(); [ 0:06] 1572 } [ 0:06] 1573 } [ 0:06] 1574 { [ 0:06] 1575 __utac_acc__Specification2_spec__3(); [ 0:06] 1576 } [ 0:06] 1577 return; [ 0:06] 1578 } [ 0:06] 1579 } [ 0:06] 1580 void printState__wrappee__empty(void) [ 0:06] 1581 { int tmp ; [ 0:06] 1582 int tmp___0 ; [ 0:06] 1583 int tmp___1 ; [ 0:06] 1584 int tmp___2 ; [ 0:06] 1585 int tmp___3 ; [ 0:06] 1586 char const * __restrict __cil_tmp6 ; [ 0:06] 1587 char const * __restrict __cil_tmp7 ; [ 0:06] 1588 char const * __restrict __cil_tmp8 ; [ 0:06] 1589 char const * __restrict __cil_tmp9 ; [ 0:06] 1590 char const * __restrict __cil_tmp10 ; [ 0:06] 1591 char const * __restrict __cil_tmp11 ; [ 0:06] 1592 char const * __restrict __cil_tmp12 ; [ 0:06] 1593 char const * __restrict __cil_tmp13 ; [ 0:06] 1594 char const * __restrict __cil_tmp14 ; [ 0:06] 1595 char const * __restrict __cil_tmp15 ; [ 0:06] 1596 char const * __restrict __cil_tmp16 ; [ 0:06] 1597 char const * __restrict __cil_tmp17 ; [ 0:06] 1598 char const * __restrict __cil_tmp18 ; [ 0:06] 1599 char const * __restrict __cil_tmp19 ; [ 0:06] 1600 char const * __restrict __cil_tmp20 ; [ 0:06] 1601 char const * __restrict __cil_tmp21 ; [ 0:06] 1602 char const * __restrict __cil_tmp22 ; [ 0:06] 1603 char const * __restrict __cil_tmp23 ; [ 0:06] 1604 char const * __restrict __cil_tmp24 ; [ 0:06] 1605 char const * __restrict __cil_tmp25 ; [ 0:06] 1606 char const * __restrict __cil_tmp26 ; [ 0:06] 1607 [ 0:06] 1608 { [ 0:06] 1609 { [ 0:06] 1610 __cil_tmp6 = (char const * __restrict )"Elevator "; [ 0:06] 1611 printf(__cil_tmp6); [ 0:06] 1612 } [ 0:06] 1613 if (doorState) { [ 0:06] 1614 { [ 0:06] 1615 __cil_tmp7 = (char const * __restrict )"[_]"; [ 0:06] 1616 printf(__cil_tmp7); [ 0:06] 1617 } [ 0:06] 1618 } else { [ 0:06] 1619 { [ 0:06] 1620 __cil_tmp8 = (char const * __restrict )"[] "; [ 0:06] 1621 printf(__cil_tmp8); [ 0:06] 1622 } [ 0:06] 1623 } [ 0:06] 1624 { [ 0:06] 1625 __cil_tmp9 = (char const * __restrict )" at "; [ 0:06] 1626 printf(__cil_tmp9); [ 0:06] 1627 __cil_tmp10 = (char const * __restrict )"%i"; [ 0:06] 1628 printf(__cil_tmp10, currentFloorID); [ 0:06] 1629 __cil_tmp11 = (char const * __restrict )" heading "; [ 0:06] 1630 printf(__cil_tmp11); [ 0:06] 1631 } [ 0:06] 1632 if (currentHeading) { [ 0:06] 1633 { [ 0:06] 1634 __cil_tmp12 = (char const * __restrict )"up"; [ 0:06] 1635 printf(__cil_tmp12); [ 0:06] 1636 } [ 0:06] 1637 } else { [ 0:06] 1638 { [ 0:06] 1639 __cil_tmp13 = (char const * __restrict )"down"; [ 0:06] 1640 printf(__cil_tmp13); [ 0:06] 1641 } [ 0:06] 1642 } [ 0:06] 1643 { [ 0:06] 1644 __cil_tmp14 = (char const * __restrict )" IL_p:"; [ 0:06] 1645 printf(__cil_tmp14); [ 0:06] 1646 } [ 0:06] 1647 if (floorButtons_0) { [ 0:06] 1648 { [ 0:06] 1649 __cil_tmp15 = (char const * __restrict )" %i"; [ 0:06] 1650 printf(__cil_tmp15, 0); [ 0:06] 1651 } [ 0:06] 1652 } else { [ 0:06] 1653 [ 0:06] 1654 } [ 0:06] 1655 if (floorButtons_1) { [ 0:06] 1656 { [ 0:06] 1657 __cil_tmp16 = (char const * __restrict )" %i"; [ 0:06] 1658 printf(__cil_tmp16, 1); [ 0:06] 1659 } [ 0:06] 1660 } else { [ 0:06] 1661 [ 0:06] 1662 } [ 0:06] 1663 if (floorButtons_2) { [ 0:06] 1664 { [ 0:06] 1665 __cil_tmp17 = (char const * __restrict )" %i"; [ 0:06] 1666 printf(__cil_tmp17, 2); [ 0:06] 1667 } [ 0:06] 1668 } else { [ 0:06] 1669 [ 0:06] 1670 } [ 0:06] 1671 if (floorButtons_3) { [ 0:06] 1672 { [ 0:06] 1673 __cil_tmp18 = (char const * __restrict )" %i"; [ 0:06] 1674 printf(__cil_tmp18, 3); [ 0:06] 1675 } [ 0:06] 1676 } else { [ 0:06] 1677 [ 0:06] 1678 } [ 0:06] 1679 if (floorButtons_4) { [ 0:06] 1680 { [ 0:06] 1681 __cil_tmp19 = (char const * __restrict )" %i"; [ 0:06] 1682 printf(__cil_tmp19, 4); [ 0:06] 1683 } [ 0:06] 1684 } else { [ 0:06] 1685 [ 0:06] 1686 } [ 0:06] 1687 { [ 0:06] 1688 __cil_tmp20 = (char const * __restrict )" F_p:"; [ 0:06] 1689 printf(__cil_tmp20); [ 0:06] 1690 tmp = isFloorCalling(0); [ 0:06] 1691 } [ 0:06] 1692 if (tmp) { [ 0:06] 1693 { [ 0:06] 1694 __cil_tmp21 = (char const * __restrict )" %i"; [ 0:06] 1695 printf(__cil_tmp21, 0); [ 0:06] 1696 } [ 0:06] 1697 } else { [ 0:06] 1698 [ 0:06] 1699 } [ 0:06] 1700 { [ 0:06] 1701 tmp___0 = isFloorCalling(1); [ 0:06] 1702 } [ 0:06] 1703 if (tmp___0) { [ 0:06] 1704 { [ 0:06] 1705 __cil_tmp22 = (char const * __restrict )" %i"; [ 0:06] 1706 printf(__cil_tmp22, 1); [ 0:06] 1707 } [ 0:06] 1708 } else { [ 0:06] 1709 [ 0:06] 1710 } [ 0:06] 1711 { [ 0:06] 1712 tmp___1 = isFloorCalling(2); [ 0:06] 1713 } [ 0:06] 1714 if (tmp___1) { [ 0:06] 1715 { [ 0:06] 1716 __cil_tmp23 = (char const * __restrict )" %i"; [ 0:06] 1717 printf(__cil_tmp23, 2); [ 0:06] 1718 } [ 0:06] 1719 } else { [ 0:06] 1720 [ 0:06] 1721 } [ 0:06] 1722 { [ 0:06] 1723 tmp___2 = isFloorCalling(3); [ 0:06] 1724 } [ 0:06] 1725 if (tmp___2) { [ 0:06] 1726 { [ 0:06] 1727 __cil_tmp24 = (char const * __restrict )" %i"; [ 0:06] 1728 printf(__cil_tmp24, 3); [ 0:06] 1729 } [ 0:06] 1730 } else { [ 0:06] 1731 [ 0:06] 1732 } [ 0:06] 1733 { [ 0:06] 1734 tmp___3 = isFloorCalling(4); [ 0:06] 1735 } [ 0:06] 1736 if (tmp___3) { [ 0:06] 1737 { [ 0:06] 1738 __cil_tmp25 = (char const * __restrict )" %i"; [ 0:06] 1739 printf(__cil_tmp25, 4); [ 0:06] 1740 } [ 0:06] 1741 } else { [ 0:06] 1742 [ 0:06] 1743 } [ 0:06] 1744 { [ 0:06] 1745 __cil_tmp26 = (char const * __restrict )"\n"; [ 0:06] 1746 printf(__cil_tmp26); [ 0:06] 1747 } [ 0:06] 1748 return; [ 0:06] 1749 } [ 0:06] 1750 } [ 0:06] 1751 void printState(void) [ 0:06] 1752 { int tmp ; [ 0:06] 1753 char const * __restrict __cil_tmp2 ; [ 0:06] 1754 [ 0:06] 1755 { [ 0:06] 1756 { [ 0:06] 1757 tmp = isBlocked(); [ 0:06] 1758 } [ 0:06] 1759 if (tmp) { [ 0:06] 1760 { [ 0:06] 1761 __cil_tmp2 = (char const * __restrict )"Blocked "; [ 0:06] 1762 printf(__cil_tmp2); [ 0:06] 1763 } [ 0:06] 1764 } else { [ 0:06] 1765 [ 0:06] 1766 } [ 0:06] 1767 { [ 0:06] 1768 printState__wrappee__empty(); [ 0:06] 1769 } [ 0:06] 1770 return; [ 0:06] 1771 } [ 0:06] 1772 } [ 0:06] 1773 int existInLiftCallsInDirection(int d ) [ 0:06] 1774 { int retValue_acc ; [ 0:06] 1775 int i ; [ 0:06] 1776 int i___0 ; [ 0:06] 1777 [ 0:06] 1778 { [ 0:06] 1779 if (d == 1) { [ 0:06] 1780 i = 0; [ 0:06] 1781 i = currentFloorID + 1; [ 0:06] 1782 { [ 0:06] 1783 while (1) { [ 0:06] 1784 while_2_continue: /* CIL Label */ ; [ 0:06] 1785 if (i < 5) { [ 0:06] 1786 [ 0:06] 1787 } else { [ 0:06] 1788 goto while_2_break; [ 0:06] 1789 } [ 0:06] 1790 if (i == 0) { [ 0:06] 1791 if (floorButtons_0) { [ 0:06] 1792 retValue_acc = 1; [ 0:06] 1793 return (retValue_acc); [ 0:06] 1794 } else { [ 0:06] 1795 goto _L___2; [ 0:06] 1796 } [ 0:06] 1797 } else { [ 0:06] 1798 _L___2: /* CIL Label */ [ 0:06] 1799 if (i == 1) { [ 0:06] 1800 if (floorButtons_1) { [ 0:06] 1801 retValue_acc = 1; [ 0:06] 1802 return (retValue_acc); [ 0:06] 1803 } else { [ 0:06] 1804 goto _L___1; [ 0:06] 1805 } [ 0:06] 1806 } else { [ 0:06] 1807 _L___1: /* CIL Label */ [ 0:06] 1808 if (i == 2) { [ 0:06] 1809 if (floorButtons_2) { [ 0:06] 1810 retValue_acc = 1; [ 0:06] 1811 return (retValue_acc); [ 0:06] 1812 } else { [ 0:06] 1813 goto _L___0; [ 0:06] 1814 } [ 0:06] 1815 } else { [ 0:06] 1816 _L___0: /* CIL Label */ [ 0:06] 1817 if (i == 3) { [ 0:06] 1818 if (floorButtons_3) { [ 0:06] 1819 retValue_acc = 1; [ 0:06] 1820 return (retValue_acc); [ 0:06] 1821 } else { [ 0:06] 1822 goto _L; [ 0:06] 1823 } [ 0:06] 1824 } else { [ 0:06] 1825 _L: /* CIL Label */ [ 0:06] 1826 if (i == 4) { [ 0:06] 1827 if (floorButtons_4) { [ 0:06] 1828 retValue_acc = 1; [ 0:06] 1829 return (retValue_acc); [ 0:06] 1830 } else { [ 0:06] 1831 [ 0:06] 1832 } [ 0:06] 1833 } else { [ 0:06] 1834 [ 0:06] 1835 } [ 0:06] 1836 } [ 0:06] 1837 } [ 0:06] 1838 } [ 0:06] 1839 } [ 0:06] 1840 i = i + 1; [ 0:06] 1841 } [ 0:06] 1842 while_2_break: /* CIL Label */ ; [ 0:06] 1843 } [ 0:06] 1844 } else { [ 0:06] 1845 if (d == 0) { [ 0:06] 1846 i___0 = 0; [ 0:06] 1847 i___0 = currentFloorID - 1; [ 0:06] 1848 { [ 0:06] 1849 while (1) { [ 0:06] 1850 while_3_continue: /* CIL Label */ ; [ 0:06] 1851 if (i___0 >= 0) { [ 0:06] 1852 [ 0:06] 1853 } else { [ 0:06] 1854 goto while_3_break; [ 0:06] 1855 } [ 0:06] 1856 i___0 = currentFloorID + 1; [ 0:06] 1857 { [ 0:06] 1858 while (1) { [ 0:06] 1859 while_4_continue: /* CIL Label */ ; [ 0:06] 1860 if (i___0 < 5) { [ 0:06] 1861 [ 0:06] 1862 } else { [ 0:06] 1863 goto while_4_break; [ 0:06] 1864 } [ 0:06] 1865 if (i___0 == 0) { [ 0:06] 1866 if (floorButtons_0) { [ 0:06] 1867 retValue_acc = 1; [ 0:06] 1868 return (retValue_acc); [ 0:06] 1869 } else { [ 0:06] 1870 goto _L___6; [ 0:06] 1871 } [ 0:06] 1872 } else { [ 0:06] 1873 _L___6: /* CIL Label */ [ 0:06] 1874 if (i___0 == 1) { [ 0:06] 1875 if (floorButtons_1) { [ 0:06] 1876 retValue_acc = 1; [ 0:06] 1877 return (retValue_acc); [ 0:06] 1878 } else { [ 0:06] 1879 goto _L___5; [ 0:06] 1880 } [ 0:06] 1881 } else { [ 0:06] 1882 _L___5: /* CIL Label */ [ 0:06] 1883 if (i___0 == 2) { [ 0:06] 1884 if (floorButtons_2) { [ 0:06] 1885 retValue_acc = 1; [ 0:06] 1886 return (retValue_acc); [ 0:06] 1887 } else { [ 0:06] 1888 goto _L___4; [ 0:06] 1889 } [ 0:06] 1890 } else { [ 0:06] 1891 _L___4: /* CIL Label */ [ 0:06] 1892 if (i___0 == 3) { [ 0:06] 1893 if (floorButtons_3) { [ 0:06] 1894 retValue_acc = 1; [ 0:06] 1895 return (retValue_acc); [ 0:06] 1896 } else { [ 0:06] 1897 goto _L___3; [ 0:06] 1898 } [ 0:06] 1899 } else { [ 0:06] 1900 _L___3: /* CIL Label */ [ 0:06] 1901 if (i___0 == 4) { [ 0:06] 1902 if (floorButtons_4) { [ 0:06] 1903 retValue_acc = 1; [ 0:06] 1904 return (retValue_acc); [ 0:06] 1905 } else { [ 0:06] 1906 [ 0:06] 1907 } [ 0:06] 1908 } else { [ 0:06] 1909 [ 0:06] 1910 } [ 0:06] 1911 } [ 0:06] 1912 } [ 0:06] 1913 } [ 0:06] 1914 } [ 0:06] 1915 i___0 = i___0 + 1; [ 0:06] 1916 } [ 0:06] 1917 while_4_break: /* CIL Label */ ; [ 0:06] 1918 } [ 0:06] 1919 i___0 = i___0 - 1; [ 0:06] 1920 } [ 0:06] 1921 while_3_break: /* CIL Label */ ; [ 0:06] 1922 } [ 0:06] 1923 } else { [ 0:06] 1924 [ 0:06] 1925 } [ 0:06] 1926 } [ 0:06] 1927 retValue_acc = 0; [ 0:06] 1928 return (retValue_acc); [ 0:06] 1929 return (retValue_acc); [ 0:06] 1930 } [ 0:06] 1931 } [ 0:06] 1932 #pragma merger(0,"Person.i","") [ 0:06] 1933 int getWeight(int person ) [ 0:06] 1934 { int retValue_acc ; [ 0:06] 1935 [ 0:06] 1936 { [ 0:06] 1937 if (person == 0) { [ 0:06] 1938 retValue_acc = 40; [ 0:06] 1939 return (retValue_acc); [ 0:06] 1940 } else { [ 0:06] 1941 if (person == 1) { [ 0:06] 1942 retValue_acc = 40; [ 0:06] 1943 return (retValue_acc); [ 0:06] 1944 } else { [ 0:06] 1945 if (person == 2) { [ 0:06] 1946 retValue_acc = 40; [ 0:06] 1947 return (retValue_acc); [ 0:06] 1948 } else { [ 0:06] 1949 if (person == 3) { [ 0:06] 1950 retValue_acc = 40; [ 0:06] 1951 return (retValue_acc); [ 0:06] 1952 } else { [ 0:06] 1953 if (person == 4) { [ 0:06] 1954 retValue_acc = 30; [ 0:06] 1955 return (retValue_acc); [ 0:06] 1956 } else { [ 0:06] 1957 if (person == 5) { [ 0:06] 1958 retValue_acc = 150; [ 0:06] 1959 return (retValue_acc); [ 0:06] 1960 } else { [ 0:06] 1961 retValue_acc = 0; [ 0:06] 1962 return (retValue_acc); [ 0:06] 1963 } [ 0:06] 1964 } [ 0:06] 1965 } [ 0:06] 1966 } [ 0:06] 1967 } [ 0:06] 1968 } [ 0:06] 1969 return (retValue_acc); [ 0:06] 1970 } [ 0:06] 1971 } [ 0:06] 1972 int getOrigin(int person ) [ 0:06] 1973 { int retValue_acc ; [ 0:06] 1974 [ 0:06] 1975 { [ 0:06] 1976 if (person == 0) { [ 0:06] 1977 retValue_acc = 4; [ 0:06] 1978 return (retValue_acc); [ 0:06] 1979 } else { [ 0:06] 1980 if (person == 1) { [ 0:06] 1981 retValue_acc = 3; [ 0:06] 1982 return (retValue_acc); [ 0:06] 1983 } else { [ 0:06] 1984 if (person == 2) { [ 0:06] 1985 retValue_acc = 2; [ 0:06] 1986 return (retValue_acc); [ 0:06] 1987 } else { [ 0:06] 1988 if (person == 3) { [ 0:06] 1989 retValue_acc = 1; [ 0:06] 1990 return (retValue_acc); [ 0:06] 1991 } else { [ 0:06] 1992 if (person == 4) { [ 0:06] 1993 retValue_acc = 0; [ 0:06] 1994 return (retValue_acc); [ 0:06] 1995 } else { [ 0:06] 1996 if (person == 5) { [ 0:06] 1997 retValue_acc = 1; [ 0:06] 1998 return (retValue_acc); [ 0:06] 1999 } else { [ 0:06] 2000 retValue_acc = 0; [ 0:06] 2001 return (retValue_acc); [ 0:06] 2002 } [ 0:06] 2003 } [ 0:06] 2004 } [ 0:06] 2005 } [ 0:06] 2006 } [ 0:06] 2007 } [ 0:06] 2008 return (retValue_acc); [ 0:06] 2009 } [ 0:06] 2010 } [ 0:06] 2011 int getDestination(int person ) [ 0:06] 2012 { int retValue_acc ; [ 0:06] 2013 [ 0:06] 2014 { [ 0:06] 2015 if (person == 0) { [ 0:06] 2016 retValue_acc = 0; [ 0:06] 2017 return (retValue_acc); [ 0:06] 2018 } else { [ 0:06] 2019 if (person == 1) { [ 0:06] 2020 retValue_acc = 0; [ 0:06] 2021 return (retValue_acc); [ 0:06] 2022 } else { [ 0:06] 2023 if (person == 2) { [ 0:06] 2024 retValue_acc = 1; [ 0:06] 2025 return (retValue_acc); [ 0:06] 2026 } else { [ 0:06] 2027 if (person == 3) { [ 0:06] 2028 retValue_acc = 3; [ 0:06] 2029 return (retValue_acc); [ 0:06] 2030 } else { [ 0:06] 2031 if (person == 4) { [ 0:06] 2032 retValue_acc = 1; [ 0:06] 2033 return (retValue_acc); [ 0:06] 2034 } else { [ 0:06] 2035 if (person == 5) { [ 0:06] 2036 retValue_acc = 3; [ 0:06] 2037 return (retValue_acc); [ 0:06] 2038 } else { [ 0:06] 2039 retValue_acc = 0; [ 0:06] 2040 return (retValue_acc); [ 0:06] 2041 } [ 0:06] 2042 } [ 0:06] 2043 } [ 0:06] 2044 } [ 0:06] 2045 } [ 0:06] 2046 } [ 0:06] 2047 return (retValue_acc); [ 0:06] 2048 } [ 0:06] 2049 } [ 0:06] 2050 #pragma merger(0,"scenario.i","") [ 0:06] 2051 void test(void) [ 0:06] 2052 { [ 0:06] 2053 [ 0:06] 2054 { [ 0:06] 2055 { [ 0:06] 2056 bigMacCall(); [ 0:06] 2057 cleanup(); [ 0:06] 2058 } [ 0:06] 2059 return; [ 0:06] 2060 } [ 0:06] 2061 } [ 0:06] 2062 #pragma merger(0,"libacc.i","") [ 0:06] 2063 extern __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const *__assertion , [ 0:06] 2064 char const *__file , [ 0:06] 2065 unsigned int __line , [ 0:06] 2066 char const *__function ) ; [ 0:06] 2067 extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ; [ 0:06] 2068 extern __attribute__((__nothrow__)) void free(void *__ptr ) ; [ 0:06] 2069 void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int , [ 0:06] 2070 int ) , [ 0:06] 2071 int val ) [ 0:06] 2072 { struct __UTAC__EXCEPTION *excep ; [ 0:06] 2073 struct __UTAC__CFLOW_FUNC *cf ; [ 0:06] 2074 void *tmp ; [ 0:06] 2075 unsigned long __cil_tmp7 ; [ 0:06] 2076 unsigned long __cil_tmp8 ; [ 0:06] 2077 unsigned long __cil_tmp9 ; [ 0:06] 2078 unsigned long __cil_tmp10 ; [ 0:06] 2079 unsigned long __cil_tmp11 ; [ 0:06] 2080 unsigned long __cil_tmp12 ; [ 0:06] 2081 unsigned long __cil_tmp13 ; [ 0:06] 2082 unsigned long __cil_tmp14 ; [ 0:06] 2083 int (**mem_15)(int , int ) ; [ 0:06] 2084 int *mem_16 ; [ 0:06] 2085 struct __UTAC__CFLOW_FUNC **mem_17 ; [ 0:06] 2086 struct __UTAC__CFLOW_FUNC **mem_18 ; [ 0:06] 2087 struct __UTAC__CFLOW_FUNC **mem_19 ; [ 0:06] 2088 [ 0:06] 2089 { [ 0:06] 2090 { [ 0:06] 2091 excep = (struct __UTAC__EXCEPTION *)exception; [ 0:06] 2092 tmp = malloc(24UL); [ 0:06] 2093 cf = (struct __UTAC__CFLOW_FUNC *)tmp; [ 0:06] 2094 mem_15 = (int (**)(int , int ))cf; [ 0:06] 2095 *mem_15 = cflow_func; [ 0:06] 2096 __cil_tmp7 = (unsigned long )cf; [ 0:06] 2097 __cil_tmp8 = __cil_tmp7 + 8; [ 0:06] 2098 mem_16 = (int *)__cil_tmp8; [ 0:06] 2099 *mem_16 = val; [ 0:06] 2100 __cil_tmp9 = (unsigned long )cf; [ 0:06] 2101 __cil_tmp10 = __cil_tmp9 + 16; [ 0:06] 2102 __cil_tmp11 = (unsigned long )excep; [ 0:06] 2103 __cil_tmp12 = __cil_tmp11 + 24; [ 0:06] 2104 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10; [ 0:06] 2105 mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12; [ 0:06] 2106 *mem_17 = *mem_18; [ 0:06] 2107 __cil_tmp13 = (unsigned long )excep; [ 0:06] 2108 __cil_tmp14 = __cil_tmp13 + 24; [ 0:06] 2109 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14; [ 0:06] 2110 *mem_19 = cf; [ 0:06] 2111 } [ 0:06] 2112 return; [ 0:06] 2113 } [ 0:06] 2114 } [ 0:06] 2115 void __utac__exception__cf_handler_free(void *exception ) [ 0:06] 2116 { struct __UTAC__EXCEPTION *excep ; [ 0:06] 2117 struct __UTAC__CFLOW_FUNC *cf ; [ 0:06] 2118 struct __UTAC__CFLOW_FUNC *tmp ; [ 0:06] 2119 unsigned long __cil_tmp5 ; [ 0:06] 2120 unsigned long __cil_tmp6 ; [ 0:06] 2121 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ; [ 0:06] 2122 unsigned long __cil_tmp8 ; [ 0:06] 2123 unsigned long __cil_tmp9 ; [ 0:06] 2124 unsigned long __cil_tmp10 ; [ 0:06] 2125 unsigned long __cil_tmp11 ; [ 0:06] 2126 void *__cil_tmp12 ; [ 0:06] 2127 unsigned long __cil_tmp13 ; [ 0:06] 2128 unsigned long __cil_tmp14 ; [ 0:06] 2129 struct __UTAC__CFLOW_FUNC **mem_15 ; [ 0:06] 2130 struct __UTAC__CFLOW_FUNC **mem_16 ; [ 0:06] 2131 struct __UTAC__CFLOW_FUNC **mem_17 ; [ 0:06] 2132 [ 0:06] 2133 { [ 0:06] 2134 excep = (struct __UTAC__EXCEPTION *)exception; [ 0:06] 2135 __cil_tmp5 = (unsigned long )excep; [ 0:06] 2136 __cil_tmp6 = __cil_tmp5 + 24; [ 0:06] 2137 mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6; [ 0:06] 2138 cf = *mem_15; [ 0:06] 2139 { [ 0:06] 2140 while (1) { [ 0:06] 2141 while_5_continue: /* CIL Label */ ; [ 0:06] 2142 { [ 0:06] 2143 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0; [ 0:06] 2144 __cil_tmp8 = (unsigned long )__cil_tmp7; [ 0:06] 2145 __cil_tmp9 = (unsigned long )cf; [ 0:06] 2146 if (__cil_tmp9 != __cil_tmp8) { [ 0:06] 2147 [ 0:06] 2148 } else { [ 0:06] 2149 goto while_5_break; [ 0:06] 2150 } [ 0:06] 2151 } [ 0:06] 2152 { [ 0:06] 2153 tmp = cf; [ 0:06] 2154 __cil_tmp10 = (unsigned long )cf; [ 0:06] 2155 __cil_tmp11 = __cil_tmp10 + 16; [ 0:06] 2156 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11; [ 0:06] 2157 cf = *mem_16; [ 0:06] 2158 __cil_tmp12 = (void *)tmp; [ 0:06] 2159 free(__cil_tmp12); [ 0:06] 2160 } [ 0:06] 2161 } [ 0:06] 2162 while_5_break: /* CIL Label */ ; [ 0:06] 2163 } [ 0:06] 2164 __cil_tmp13 = (unsigned long )excep; [ 0:06] 2165 __cil_tmp14 = __cil_tmp13 + 24; [ 0:06] 2166 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14; [ 0:06] 2167 *mem_17 = (struct __UTAC__CFLOW_FUNC *)0; [ 0:06] 2168 return; [ 0:06] 2169 } [ 0:06] 2170 } [ 0:06] 2171 void __utac__exception__cf_handler_reset(void *exception ) [ 0:06] 2172 { struct __UTAC__EXCEPTION *excep ; [ 0:06] 2173 struct __UTAC__CFLOW_FUNC *cf ; [ 0:06] 2174 unsigned long __cil_tmp5 ; [ 0:06] 2175 unsigned long __cil_tmp6 ; [ 0:06] 2176 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ; [ 0:06] 2177 unsigned long __cil_tmp8 ; [ 0:06] 2178 unsigned long __cil_tmp9 ; [ 0:06] 2179 int (*__cil_tmp10)(int , int ) ; [ 0:06] 2180 unsigned long __cil_tmp11 ; [ 0:06] 2181 unsigned long __cil_tmp12 ; [ 0:06] 2182 int __cil_tmp13 ; [ 0:06] 2183 unsigned long __cil_tmp14 ; [ 0:06] 2184 unsigned long __cil_tmp15 ; [ 0:06] 2185 struct __UTAC__CFLOW_FUNC **mem_16 ; [ 0:06] 2186 int (**mem_17)(int , int ) ; [ 0:06] 2187 int *mem_18 ; [ 0:06] 2188 struct __UTAC__CFLOW_FUNC **mem_19 ; [ 0:06] 2189 [ 0:06] 2190 { [ 0:06] 2191 excep = (struct __UTAC__EXCEPTION *)exception; [ 0:06] 2192 __cil_tmp5 = (unsigned long )excep; [ 0:06] 2193 __cil_tmp6 = __cil_tmp5 + 24; [ 0:06] 2194 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6; [ 0:06] 2195 cf = *mem_16; [ 0:06] 2196 { [ 0:06] 2197 while (1) { [ 0:06] 2198 while_6_continue: /* CIL Label */ ; [ 0:06] 2199 { [ 0:06] 2200 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0; [ 0:06] 2201 __cil_tmp8 = (unsigned long )__cil_tmp7; [ 0:06] 2202 __cil_tmp9 = (unsigned long )cf; [ 0:06] 2203 if (__cil_tmp9 != __cil_tmp8) { [ 0:06] 2204 [ 0:06] 2205 } else { [ 0:06] 2206 goto while_6_break; [ 0:06] 2207 } [ 0:06] 2208 } [ 0:06] 2209 { [ 0:06] 2210 mem_17 = (int (**)(int , int ))cf; [ 0:06] 2211 __cil_tmp10 = *mem_17; [ 0:06] 2212 __cil_tmp11 = (unsigned long )cf; [ 0:06] 2213 __cil_tmp12 = __cil_tmp11 + 8; [ 0:06] 2214 mem_18 = (int *)__cil_tmp12; [ 0:06] 2215 __cil_tmp13 = *mem_18; [ 0:06] 2216 (*__cil_tmp10)(4, __cil_tmp13); [ 0:06] 2217 __cil_tmp14 = (unsigned long )cf; [ 0:06] 2218 __cil_tmp15 = __cil_tmp14 + 16; [ 0:06] 2219 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15; [ 0:06] 2220 cf = *mem_19; [ 0:06] 2221 } [ 0:06] 2222 } [ 0:06] 2223 while_6_break: /* CIL Label */ ; [ 0:06] 2224 } [ 0:06] 2225 { [ 0:06] 2226 __utac__exception__cf_handler_free(exception); [ 0:06] 2227 } [ 0:06] 2228 return; [ 0:06] 2229 } [ 0:06] 2230 } [ 0:06] 2231 void *__utac__error_stack_mgt(void *env , int mode , int count ) ; [ 0:06] 2232 static struct __ACC__ERR *head = (struct __ACC__ERR *)0; [ 0:06] 2233 void *__utac__error_stack_mgt(void *env , int mode , int count ) [ 0:06] 2234 { void *retValue_acc ; [ 0:06] 2235 struct __ACC__ERR *new ; [ 0:06] 2236 void *tmp ; [ 0:06] 2237 struct __ACC__ERR *temp ; [ 0:06] 2238 struct __ACC__ERR *next ; [ 0:06] 2239 void *excep ; [ 0:06] 2240 unsigned long __cil_tmp10 ; [ 0:06] 2241 unsigned long __cil_tmp11 ; [ 0:06] 2242 unsigned long __cil_tmp12 ; [ 0:06] 2243 unsigned long __cil_tmp13 ; [ 0:06] 2244 void *__cil_tmp14 ; [ 0:06] 2245 unsigned long __cil_tmp15 ; [ 0:06] 2246 unsigned long __cil_tmp16 ; [ 0:06] 2247 void *__cil_tmp17 ; [ 0:06] 2248 void **mem_18 ; [ 0:06] 2249 struct __ACC__ERR **mem_19 ; [ 0:06] 2250 struct __ACC__ERR **mem_20 ; [ 0:06] 2251 void **mem_21 ; [ 0:06] 2252 struct __ACC__ERR **mem_22 ; [ 0:06] 2253 void **mem_23 ; [ 0:06] 2254 void **mem_24 ; [ 0:06] 2255 [ 0:06] 2256 { [ 0:06] 2257 if (count == 0) { [ 0:06] 2258 return (retValue_acc); [ 0:06] 2259 } else { [ 0:06] 2260 [ 0:06] 2261 } [ 0:06] 2262 if (mode == 0) { [ 0:06] 2263 { [ 0:06] 2264 tmp = malloc(16UL); [ 0:06] 2265 new = (struct __ACC__ERR *)tmp; [ 0:06] 2266 mem_18 = (void **)new; [ 0:06] 2267 *mem_18 = env; [ 0:06] 2268 __cil_tmp10 = (unsigned long )new; [ 0:06] 2269 __cil_tmp11 = __cil_tmp10 + 8; [ 0:06] 2270 mem_19 = (struct __ACC__ERR **)__cil_tmp11; [ 0:06] 2271 *mem_19 = head; [ 0:06] 2272 head = new; [ 0:06] 2273 retValue_acc = (void *)new; [ 0:06] 2274 } [ 0:06] 2275 return (retValue_acc); [ 0:06] 2276 } else { [ 0:06] 2277 [ 0:06] 2278 } [ 0:06] 2279 if (mode == 1) { [ 0:06] 2280 temp = head; [ 0:06] 2281 { [ 0:06] 2282 while (1) { [ 0:06] 2283 while_7_continue: /* CIL Label */ ; [ 0:06] 2284 if (count > 1) { [ 0:06] 2285 [ 0:06] 2286 } else { [ 0:06] 2287 goto while_7_break; [ 0:06] 2288 } [ 0:06] 2289 { [ 0:06] 2290 __cil_tmp12 = (unsigned long )temp; [ 0:06] 2291 __cil_tmp13 = __cil_tmp12 + 8; [ 0:06] 2292 mem_20 = (struct __ACC__ERR **)__cil_tmp13; [ 0:06] 2293 next = *mem_20; [ 0:06] 2294 mem_21 = (void **)temp; [ 0:06] 2295 excep = *mem_21; [ 0:06] 2296 __cil_tmp14 = (void *)temp; [ 0:06] 2297 free(__cil_tmp14); [ 0:06] 2298 __utac__exception__cf_handler_reset(excep); [ 0:06] 2299 temp = next; [ 0:06] 2300 count = count - 1; [ 0:06] 2301 } [ 0:06] 2302 } [ 0:06] 2303 while_7_break: /* CIL Label */ ; [ 0:06] 2304 } [ 0:06] 2305 { [ 0:06] 2306 __cil_tmp15 = (unsigned long )temp; [ 0:06] 2307 __cil_tmp16 = __cil_tmp15 + 8; [ 0:06] 2308 mem_22 = (struct __ACC__ERR **)__cil_tmp16; [ 0:06] 2309 head = *mem_22; [ 0:06] 2310 mem_23 = (void **)temp; [ 0:06] 2311 excep = *mem_23; [ 0:06] 2312 __cil_tmp17 = (void *)temp; [ 0:06] 2313 free(__cil_tmp17); [ 0:06] 2314 __utac__exception__cf_handler_reset(excep); [ 0:06] 2315 retValue_acc = excep; [ 0:06] 2316 } [ 0:06] 2317 return (retValue_acc); [ 0:06] 2318 } else { [ 0:06] 2319 [ 0:06] 2320 } [ 0:06] 2321 if (mode == 2) { [ 0:06] 2322 if (head) { [ 0:06] 2323 mem_24 = (void **)head; [ 0:06] 2324 retValue_acc = *mem_24; [ 0:06] 2325 return (retValue_acc); [ 0:06] 2326 } else { [ 0:06] 2327 retValue_acc = (void *)0; [ 0:06] 2328 return (retValue_acc); [ 0:06] 2329 } [ 0:06] 2330 } else { [ 0:06] 2331 [ 0:06] 2332 } [ 0:06] 2333 return (retValue_acc); [ 0:06] 2334 } [ 0:06] 2335 } [ 0:06] 2336 void *__utac__get_this_arg(int i , struct JoinPoint *this ) [ 0:06] 2337 { void *retValue_acc ; [ 0:06] 2338 unsigned long __cil_tmp4 ; [ 0:06] 2339 unsigned long __cil_tmp5 ; [ 0:06] 2340 int __cil_tmp6 ; [ 0:06] 2341 int __cil_tmp7 ; [ 0:06] 2342 unsigned long __cil_tmp8 ; [ 0:06] 2343 unsigned long __cil_tmp9 ; [ 0:06] 2344 void **__cil_tmp10 ; [ 0:06] 2345 void **__cil_tmp11 ; [ 0:06] 2346 int *mem_12 ; [ 0:06] 2347 void ***mem_13 ; [ 0:06] 2348 [ 0:06] 2349 { [ 0:06] 2350 if (i > 0) { [ 0:06] 2351 { [ 0:06] 2352 __cil_tmp4 = (unsigned long )this; [ 0:06] 2353 __cil_tmp5 = __cil_tmp4 + 16; [ 0:06] 2354 mem_12 = (int *)__cil_tmp5; [ 0:06] 2355 __cil_tmp6 = *mem_12; [ 0:06] 2356 if (i <= __cil_tmp6) { [ 0:06] 2357 [ 0:06] 2358 } else { [ 0:06] 2359 { [ 0:06] 2360 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c", [ 0:06] 2361 123U, "__utac__get_this_arg"); [ 0:06] 2362 } [ 0:06] 2363 } [ 0:06] 2364 } [ 0:06] 2365 } else { [ 0:06] 2366 { [ 0:06] 2367 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c", [ 0:06] 2368 123U, "__utac__get_this_arg"); [ 0:06] 2369 } [ 0:06] 2370 } [ 0:06] 2371 __cil_tmp7 = i - 1; [ 0:06] 2372 __cil_tmp8 = (unsigned long )this; [ 0:06] 2373 __cil_tmp9 = __cil_tmp8 + 8; [ 0:06] 2374 mem_13 = (void ***)__cil_tmp9; [ 0:06] 2375 __cil_tmp10 = *mem_13; [ 0:06] 2376 __cil_tmp11 = __cil_tmp10 + __cil_tmp7; [ 0:06] 2377 retValue_acc = *__cil_tmp11; [ 0:06] 2378 return (retValue_acc); [ 0:06] 2379 return (retValue_acc); [ 0:06] 2380 } [ 0:06] 2381 } [ 0:06] 2382 char const *__utac__get_this_argtype(int i , struct JoinPoint *this ) [ 0:06] 2383 { char const *retValue_acc ; [ 0:06] 2384 unsigned long __cil_tmp4 ; [ 0:06] 2385 unsigned long __cil_tmp5 ; [ 0:06] 2386 int __cil_tmp6 ; [ 0:06] 2387 int __cil_tmp7 ; [ 0:06] 2388 unsigned long __cil_tmp8 ; [ 0:06] 2389 unsigned long __cil_tmp9 ; [ 0:06] 2390 char const **__cil_tmp10 ; [ 0:06] 2391 char const **__cil_tmp11 ; [ 0:06] 2392 int *mem_12 ; [ 0:06] 2393 char const ***mem_13 ; [ 0:06] 2394 [ 0:06] 2395 { [ 0:06] 2396 if (i > 0) { [ 0:06] 2397 { [ 0:06] 2398 __cil_tmp4 = (unsigned long )this; [ 0:06] 2399 __cil_tmp5 = __cil_tmp4 + 16; [ 0:06] 2400 mem_12 = (int *)__cil_tmp5; [ 0:06] 2401 __cil_tmp6 = *mem_12; [ 0:06] 2402 if (i <= __cil_tmp6) { [ 0:06] 2403 [ 0:06] 2404 } else { [ 0:06] 2405 { [ 0:06] 2406 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c", [ 0:06] 2407 131U, "__utac__get_this_argtype"); [ 0:06] 2408 } [ 0:06] 2409 } [ 0:06] 2410 } [ 0:06] 2411 } else { [ 0:06] 2412 { [ 0:06] 2413 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c", [ 0:06] 2414 131U, "__utac__get_this_argtype"); [ 0:06] 2415 } [ 0:06] 2416 } [ 0:06] 2417 __cil_tmp7 = i - 1; [ 0:06] 2418 __cil_tmp8 = (unsigned long )this; [ 0:06] 2419 __cil_tmp9 = __cil_tmp8 + 24; [ 0:06] 2420 mem_13 = (char const ***)__cil_tmp9; [ 0:06] 2421 __cil_tmp10 = *mem_13; [ 0:06] 2422 __cil_tmp11 = __cil_tmp10 + __cil_tmp7; [ 0:06] 2423 retValue_acc = *__cil_tmp11; [ 0:06] 2424 return (retValue_acc); [ 0:06] 2425 return (retValue_acc); [ 0:06] 2426 } [ 0:06] 2427 } [ 0:06] 2428 #pragma merger(0,"featureselect.i","") [ 0:06] 2429 int select_one(void) ; [ 0:06] 2430 int select_one(void) [ 0:06] 2431 { int retValue_acc ; [ 0:06] 2432 int choice = __VERIFIER_nondet_int(); [ 0:06] 2433 [ 0:06] 2434 { [ 0:06] 2435 retValue_acc = choice; [ 0:06] 2436 return (retValue_acc); [ 0:06] 2437 return (retValue_acc); [ 0:06] 2438 } [ 0:06] 2439 } [ 0:06] 2440 void select_features(void) [ 0:06] 2441 { [ 0:06] 2442 [ 0:06] 2443 { [ 0:06] 2444 return; [ 0:06] 2445 } [ 0:06] 2446 } [ 0:06] 2447 void select_helpers(void) [ 0:06] 2448 { [ 0:06] 2449 [ 0:06] 2450 { [ 0:06] 2451 return; [ 0:06] 2452 } [ 0:06] 2453 } [ 0:06] 2454 int valid_product(void) [ 0:06] 2455 { int retValue_acc ; [ 0:06] 2456 [ 0:06] 2457 { [ 0:06] 2458 retValue_acc = 1; [ 0:06] 2459 return (retValue_acc); [ 0:06] 2460 return (retValue_acc); [ 0:06] 2461 } [ 0:06] 2462 } [ 0:06] 2463 #pragma merger(0,"Floor.i","") [ 0:06] 2464 void callOnFloor(int floorID ) ; [ 0:06] 2465 int calls_0 ; [ 0:06] 2466 int calls_1 ; [ 0:06] 2467 int calls_2 ; [ 0:06] 2468 int calls_3 ; [ 0:06] 2469 int calls_4 ; [ 0:06] 2470 int personOnFloor_0_0 ; [ 0:06] 2471 int personOnFloor_0_1 ; [ 0:06] 2472 int personOnFloor_0_2 ; [ 0:06] 2473 int personOnFloor_0_3 ; [ 0:06] 2474 int personOnFloor_0_4 ; [ 0:06] 2475 int personOnFloor_1_0 ; [ 0:06] 2476 int personOnFloor_1_1 ; [ 0:06] 2477 int personOnFloor_1_2 ; [ 0:06] 2478 int personOnFloor_1_3 ; [ 0:06] 2479 int personOnFloor_1_4 ; [ 0:06] 2480 int personOnFloor_2_0 ; [ 0:06] 2481 int personOnFloor_2_1 ; [ 0:06] 2482 int personOnFloor_2_2 ; [ 0:06] 2483 int personOnFloor_2_3 ; [ 0:06] 2484 int personOnFloor_2_4 ; [ 0:06] 2485 int personOnFloor_3_0 ; [ 0:06] 2486 int personOnFloor_3_1 ; [ 0:06] 2487 int personOnFloor_3_2 ; [ 0:06] 2488 int personOnFloor_3_3 ; [ 0:06] 2489 int personOnFloor_3_4 ; [ 0:06] 2490 int personOnFloor_4_0 ; [ 0:06] 2491 int personOnFloor_4_1 ; [ 0:06] 2492 int personOnFloor_4_2 ; [ 0:06] 2493 int personOnFloor_4_3 ; [ 0:06] 2494 int personOnFloor_4_4 ; [ 0:06] 2495 int personOnFloor_5_0 ; [ 0:06] 2496 int personOnFloor_5_1 ; [ 0:06] 2497 int personOnFloor_5_2 ; [ 0:06] 2498 int personOnFloor_5_3 ; [ 0:06] 2499 int personOnFloor_5_4 ; [ 0:06] 2500 void initFloors(void) [ 0:06] 2501 { [ 0:06] 2502 [ 0:06] 2503 { [ 0:06] 2504 calls_0 = 0; [ 0:06] 2505 calls_1 = 0; [ 0:06] 2506 calls_2 = 0; [ 0:06] 2507 calls_3 = 0; [ 0:06] 2508 calls_4 = 0; [ 0:06] 2509 personOnFloor_0_0 = 0; [ 0:06] 2510 personOnFloor_0_1 = 0; [ 0:06] 2511 personOnFloor_0_2 = 0; [ 0:06] 2512 personOnFloor_0_3 = 0; [ 0:06] 2513 personOnFloor_0_4 = 0; [ 0:06] 2514 personOnFloor_1_0 = 0; [ 0:06] 2515 personOnFloor_1_1 = 0; [ 0:06] 2516 personOnFloor_1_2 = 0; [ 0:06] 2517 personOnFloor_1_3 = 0; [ 0:06] 2518 personOnFloor_1_4 = 0; [ 0:06] 2519 personOnFloor_2_0 = 0; [ 0:06] 2520 personOnFloor_2_1 = 0; [ 0:06] 2521 personOnFloor_2_2 = 0; [ 0:06] 2522 personOnFloor_2_3 = 0; [ 0:06] 2523 personOnFloor_2_4 = 0; [ 0:06] 2524 personOnFloor_3_0 = 0; [ 0:06] 2525 personOnFloor_3_1 = 0; [ 0:06] 2526 personOnFloor_3_2 = 0; [ 0:06] 2527 personOnFloor_3_3 = 0; [ 0:06] 2528 personOnFloor_3_4 = 0; [ 0:06] 2529 personOnFloor_4_0 = 0; [ 0:06] 2530 personOnFloor_4_1 = 0; [ 0:06] 2531 personOnFloor_4_2 = 0; [ 0:06] 2532 personOnFloor_4_3 = 0; [ 0:06] 2533 personOnFloor_4_4 = 0; [ 0:06] 2534 personOnFloor_5_0 = 0; [ 0:06] 2535 personOnFloor_5_1 = 0; [ 0:06] 2536 personOnFloor_5_2 = 0; [ 0:06] 2537 personOnFloor_5_3 = 0; [ 0:06] 2538 personOnFloor_5_4 = 0; [ 0:06] 2539 return; [ 0:06] 2540 } [ 0:06] 2541 } [ 0:06] 2542 int isFloorCalling(int floorID ) [ 0:06] 2543 { int retValue_acc ; [ 0:06] 2544 [ 0:06] 2545 { [ 0:06] 2546 if (floorID == 0) { [ 0:06] 2547 retValue_acc = calls_0; [ 0:06] 2548 return (retValue_acc); [ 0:06] 2549 } else { [ 0:06] 2550 if (floorID == 1) { [ 0:06] 2551 retValue_acc = calls_1; [ 0:06] 2552 return (retValue_acc); [ 0:06] 2553 } else { [ 0:06] 2554 if (floorID == 2) { [ 0:06] 2555 retValue_acc = calls_2; [ 0:06] 2556 return (retValue_acc); [ 0:06] 2557 } else { [ 0:06] 2558 if (floorID == 3) { [ 0:06] 2559 retValue_acc = calls_3; [ 0:06] 2560 return (retValue_acc); [ 0:06] 2561 } else { [ 0:06] 2562 if (floorID == 4) { [ 0:06] 2563 retValue_acc = calls_4; [ 0:06] 2564 return (retValue_acc); [ 0:06] 2565 } else { [ 0:06] 2566 [ 0:06] 2567 } [ 0:06] 2568 } [ 0:06] 2569 } [ 0:06] 2570 } [ 0:06] 2571 } [ 0:06] 2572 retValue_acc = 0; [ 0:06] 2573 return (retValue_acc); [ 0:06] 2574 return (retValue_acc); [ 0:06] 2575 } [ 0:06] 2576 } [ 0:06] 2577 void resetCallOnFloor(int floorID ) [ 0:06] 2578 { [ 0:06] 2579 [ 0:06] 2580 { [ 0:06] 2581 if (floorID == 0) { [ 0:06] 2582 calls_0 = 0; [ 0:06] 2583 } else { [ 0:06] 2584 if (floorID == 1) { [ 0:06] 2585 calls_1 = 0; [ 0:06] 2586 } else { [ 0:06] 2587 if (floorID == 2) { [ 0:06] 2588 calls_2 = 0; [ 0:06] 2589 } else { [ 0:06] 2590 if (floorID == 3) { [ 0:06] 2591 calls_3 = 0; [ 0:06] 2592 } else { [ 0:06] 2593 if (floorID == 4) { [ 0:06] 2594 calls_4 = 0; [ 0:06] 2595 } else { [ 0:06] 2596 [ 0:06] 2597 } [ 0:06] 2598 } [ 0:06] 2599 } [ 0:06] 2600 } [ 0:06] 2601 } [ 0:06] 2602 return; [ 0:06] 2603 } [ 0:06] 2604 } [ 0:06] 2605 void callOnFloor(int floorID ) [ 0:06] 2606 { [ 0:06] 2607 [ 0:06] 2608 { [ 0:06] 2609 if (floorID == 0) { [ 0:06] 2610 calls_0 = 1; [ 0:06] 2611 } else { [ 0:06] 2612 if (floorID == 1) { [ 0:06] 2613 calls_1 = 1; [ 0:06] 2614 } else { [ 0:06] 2615 if (floorID == 2) { [ 0:06] 2616 calls_2 = 1; [ 0:06] 2617 } else { [ 0:06] 2618 if (floorID == 3) { [ 0:06] 2619 calls_3 = 1; [ 0:06] 2620 } else { [ 0:06] 2621 if (floorID == 4) { [ 0:06] 2622 calls_4 = 1; [ 0:06] 2623 } else { [ 0:06] 2624 [ 0:06] 2625 } [ 0:06] 2626 } [ 0:06] 2627 } [ 0:06] 2628 } [ 0:06] 2629 } [ 0:06] 2630 return; [ 0:06] 2631 } [ 0:06] 2632 } [ 0:06] 2633 int isPersonOnFloor(int person , int floor ) [ 0:06] 2634 { int retValue_acc ; [ 0:06] 2635 [ 0:06] 2636 { [ 0:06] 2637 if (floor == 0) { [ 0:06] 2638 if (person == 0) { [ 0:06] 2639 retValue_acc = personOnFloor_0_0; [ 0:06] 2640 return (retValue_acc); [ 0:06] 2641 } else { [ 0:06] 2642 if (person == 1) { [ 0:06] 2643 retValue_acc = personOnFloor_1_0; [ 0:06] 2644 return (retValue_acc); [ 0:06] 2645 } else { [ 0:06] 2646 if (person == 2) { [ 0:06] 2647 retValue_acc = personOnFloor_2_0; [ 0:06] 2648 return (retValue_acc); [ 0:06] 2649 } else { [ 0:06] 2650 if (person == 3) { [ 0:06] 2651 retValue_acc = personOnFloor_3_0; [ 0:06] 2652 return (retValue_acc); [ 0:06] 2653 } else { [ 0:06] 2654 if (person == 4) { [ 0:06] 2655 retValue_acc = personOnFloor_4_0; [ 0:06] 2656 return (retValue_acc); [ 0:06] 2657 } else { [ 0:06] 2658 if (person == 5) { [ 0:06] 2659 retValue_acc = personOnFloor_5_0; [ 0:06] 2660 return (retValue_acc); [ 0:06] 2661 } else { [ 0:06] 2662 [ 0:06] 2663 } [ 0:06] 2664 } [ 0:06] 2665 } [ 0:06] 2666 } [ 0:06] 2667 } [ 0:06] 2668 } [ 0:06] 2669 } else { [ 0:06] 2670 if (floor == 1) { [ 0:06] 2671 if (person == 0) { [ 0:06] 2672 retValue_acc = personOnFloor_0_1; [ 0:06] 2673 return (retValue_acc); [ 0:06] 2674 } else { [ 0:06] 2675 if (person == 1) { [ 0:06] 2676 retValue_acc = personOnFloor_1_1; [ 0:06] 2677 return (retValue_acc); [ 0:06] 2678 } else { [ 0:06] 2679 if (person == 2) { [ 0:06] 2680 retValue_acc = personOnFloor_2_1; [ 0:06] 2681 return (retValue_acc); [ 0:06] 2682 } else { [ 0:06] 2683 if (person == 3) { [ 0:06] 2684 retValue_acc = personOnFloor_3_1; [ 0:06] 2685 return (retValue_acc); [ 0:06] 2686 } else { [ 0:06] 2687 if (person == 4) { [ 0:06] 2688 retValue_acc = personOnFloor_4_1; [ 0:06] 2689 return (retValue_acc); [ 0:06] 2690 } else { [ 0:06] 2691 if (person == 5) { [ 0:06] 2692 retValue_acc = personOnFloor_5_1; [ 0:06] 2693 return (retValue_acc); [ 0:06] 2694 } else { [ 0:06] 2695 [ 0:06] 2696 } [ 0:06] 2697 } [ 0:06] 2698 } [ 0:06] 2699 } [ 0:06] 2700 } [ 0:06] 2701 } [ 0:06] 2702 } else { [ 0:06] 2703 if (floor == 2) { [ 0:06] 2704 if (person == 0) { [ 0:06] 2705 retValue_acc = personOnFloor_0_2; [ 0:06] 2706 return (retValue_acc); [ 0:06] 2707 } else { [ 0:06] 2708 if (person == 1) { [ 0:06] 2709 retValue_acc = personOnFloor_1_2; [ 0:06] 2710 return (retValue_acc); [ 0:06] 2711 } else { [ 0:06] 2712 if (person == 2) { [ 0:06] 2713 retValue_acc = personOnFloor_2_2; [ 0:06] 2714 return (retValue_acc); [ 0:06] 2715 } else { [ 0:06] 2716 if (person == 3) { [ 0:06] 2717 retValue_acc = personOnFloor_3_2; [ 0:06] 2718 return (retValue_acc); [ 0:06] 2719 } else { [ 0:06] 2720 if (person == 4) { [ 0:06] 2721 retValue_acc = personOnFloor_4_2; [ 0:06] 2722 return (retValue_acc); [ 0:06] 2723 } else { [ 0:06] 2724 if (person == 5) { [ 0:06] 2725 retValue_acc = personOnFloor_5_2; [ 0:06] 2726 return (retValue_acc); [ 0:06] 2727 } else { [ 0:06] 2728 [ 0:06] 2729 } [ 0:06] 2730 } [ 0:06] 2731 } [ 0:06] 2732 } [ 0:06] 2733 } [ 0:06] 2734 } [ 0:06] 2735 } else { [ 0:06] 2736 if (floor == 3) { [ 0:06] 2737 if (person == 0) { [ 0:06] 2738 retValue_acc = personOnFloor_0_3; [ 0:06] 2739 return (retValue_acc); [ 0:06] 2740 } else { [ 0:06] 2741 if (person == 1) { [ 0:06] 2742 retValue_acc = personOnFloor_1_3; [ 0:06] 2743 return (retValue_acc); [ 0:06] 2744 } else { [ 0:06] 2745 if (person == 2) { [ 0:06] 2746 retValue_acc = personOnFloor_2_3; [ 0:06] 2747 return (retValue_acc); [ 0:06] 2748 } else { [ 0:06] 2749 if (person == 3) { [ 0:06] 2750 retValue_acc = personOnFloor_3_3; [ 0:06] 2751 return (retValue_acc); [ 0:06] 2752 } else { [ 0:06] 2753 if (person == 4) { [ 0:06] 2754 retValue_acc = personOnFloor_4_3; [ 0:06] 2755 return (retValue_acc); [ 0:06] 2756 } else { [ 0:06] 2757 if (person == 5) { [ 0:06] 2758 retValue_acc = personOnFloor_5_3; [ 0:06] 2759 return (retValue_acc); [ 0:06] 2760 } else { [ 0:06] 2761 [ 0:06] 2762 } [ 0:06] 2763 } [ 0:06] 2764 } [ 0:06] 2765 } [ 0:06] 2766 } [ 0:06] 2767 } [ 0:06] 2768 } else { [ 0:06] 2769 if (floor == 4) { [ 0:06] 2770 if (person == 0) { [ 0:06] 2771 retValue_acc = personOnFloor_0_4; [ 0:06] 2772 return (retValue_acc); [ 0:06] 2773 } else { [ 0:06] 2774 if (person == 1) { [ 0:06] 2775 retValue_acc = personOnFloor_1_4; [ 0:06] 2776 return (retValue_acc); [ 0:06] 2777 } else { [ 0:06] 2778 if (person == 2) { [ 0:06] 2779 retValue_acc = personOnFloor_2_4; [ 0:06] 2780 return (retValue_acc); [ 0:06] 2781 } else { [ 0:06] 2782 if (person == 3) { [ 0:06] 2783 retValue_acc = personOnFloor_3_4; [ 0:06] 2784 return (retValue_acc); [ 0:06] 2785 } else { [ 0:06] 2786 if (person == 4) { [ 0:06] 2787 retValue_acc = personOnFloor_4_4; [ 0:06] 2788 return (retValue_acc); [ 0:06] 2789 } else { [ 0:06] 2790 if (person == 5) { [ 0:06] 2791 retValue_acc = personOnFloor_5_4; [ 0:06] 2792 return (retValue_acc); [ 0:06] 2793 } else { [ 0:06] 2794 [ 0:06] 2795 } [ 0:06] 2796 } [ 0:06] 2797 } [ 0:06] 2798 } [ 0:06] 2799 } [ 0:06] 2800 } [ 0:06] 2801 } else { [ 0:06] 2802 [ 0:06] 2803 } [ 0:06] 2804 } [ 0:06] 2805 } [ 0:06] 2806 } [ 0:06] 2807 } [ 0:06] 2808 retValue_acc = 0; [ 0:06] 2809 return (retValue_acc); [ 0:06] 2810 return (retValue_acc); [ 0:06] 2811 } [ 0:06] 2812 } [ 0:06] 2813 void initPersonOnFloor(int person , int floor ) [ 0:06] 2814 { [ 0:06] 2815 [ 0:06] 2816 { [ 0:06] 2817 if (floor == 0) { [ 0:06] 2818 if (person == 0) { [ 0:06] 2819 personOnFloor_0_0 = 1; [ 0:06] 2820 } else { [ 0:06] 2821 if (person == 1) { [ 0:06] 2822 personOnFloor_1_0 = 1; [ 0:06] 2823 } else { [ 0:06] 2824 if (person == 2) { [ 0:06] 2825 personOnFloor_2_0 = 1; [ 0:06] 2826 } else { [ 0:06] 2827 if (person == 3) { [ 0:06] 2828 personOnFloor_3_0 = 1; [ 0:06] 2829 } else { [ 0:06] 2830 if (person == 4) { [ 0:06] 2831 personOnFloor_4_0 = 1; [ 0:06] 2832 } else { [ 0:06] 2833 if (person == 5) { [ 0:06] 2834 personOnFloor_5_0 = 1; [ 0:06] 2835 } else { [ 0:06] 2836 [ 0:06] 2837 } [ 0:06] 2838 } [ 0:06] 2839 } [ 0:06] 2840 } [ 0:06] 2841 } [ 0:06] 2842 } [ 0:06] 2843 } else { [ 0:06] 2844 if (floor == 1) { [ 0:06] 2845 if (person == 0) { [ 0:06] 2846 personOnFloor_0_1 = 1; [ 0:06] 2847 } else { [ 0:06] 2848 if (person == 1) { [ 0:06] 2849 personOnFloor_1_1 = 1; [ 0:06] 2850 } else { [ 0:06] 2851 if (person == 2) { [ 0:06] 2852 personOnFloor_2_1 = 1; [ 0:06] 2853 } else { [ 0:06] 2854 if (person == 3) { [ 0:06] 2855 personOnFloor_3_1 = 1; [ 0:06] 2856 } else { [ 0:06] 2857 if (person == 4) { [ 0:06] 2858 personOnFloor_4_1 = 1; [ 0:06] 2859 } else { [ 0:06] 2860 if (person == 5) { [ 0:06] 2861 personOnFloor_5_1 = 1; [ 0:06] 2862 } else { [ 0:06] 2863 [ 0:06] 2864 } [ 0:06] 2865 } [ 0:06] 2866 } [ 0:06] 2867 } [ 0:06] 2868 } [ 0:06] 2869 } [ 0:06] 2870 } else { [ 0:06] 2871 if (floor == 2) { [ 0:06] 2872 if (person == 0) { [ 0:06] 2873 personOnFloor_0_2 = 1; [ 0:06] 2874 } else { [ 0:06] 2875 if (person == 1) { [ 0:06] 2876 personOnFloor_1_2 = 1; [ 0:06] 2877 } else { [ 0:06] 2878 if (person == 2) { [ 0:06] 2879 personOnFloor_2_2 = 1; [ 0:06] 2880 } else { [ 0:06] 2881 if (person == 3) { [ 0:06] 2882 personOnFloor_3_2 = 1; [ 0:06] 2883 } else { [ 0:06] 2884 if (person == 4) { [ 0:06] 2885 personOnFloor_4_2 = 1; [ 0:06] 2886 } else { [ 0:06] 2887 if (person == 5) { [ 0:06] 2888 personOnFloor_5_2 = 1; [ 0:06] 2889 } else { [ 0:06] 2890 [ 0:06] 2891 } [ 0:06] 2892 } [ 0:06] 2893 } [ 0:06] 2894 } [ 0:06] 2895 } [ 0:06] 2896 } [ 0:06] 2897 } else { [ 0:06] 2898 if (floor == 3) { [ 0:06] 2899 if (person == 0) { [ 0:06] 2900 personOnFloor_0_3 = 1; [ 0:06] 2901 } else { [ 0:06] 2902 if (person == 1) { [ 0:06] 2903 personOnFloor_1_3 = 1; [ 0:06] 2904 } else { [ 0:06] 2905 if (person == 2) { [ 0:06] 2906 personOnFloor_2_3 = 1; [ 0:06] 2907 } else { [ 0:06] 2908 if (person == 3) { [ 0:06] 2909 personOnFloor_3_3 = 1; [ 0:06] 2910 } else { [ 0:06] 2911 if (person == 4) { [ 0:06] 2912 personOnFloor_4_3 = 1; [ 0:06] 2913 } else { [ 0:06] 2914 if (person == 5) { [ 0:06] 2915 personOnFloor_5_3 = 1; [ 0:06] 2916 } else { [ 0:06] 2917 [ 0:06] 2918 } [ 0:06] 2919 } [ 0:06] 2920 } [ 0:06] 2921 } [ 0:06] 2922 } [ 0:06] 2923 } [ 0:06] 2924 } else { [ 0:06] 2925 if (floor == 4) { [ 0:06] 2926 if (person == 0) { [ 0:06] 2927 personOnFloor_0_4 = 1; [ 0:06] 2928 } else { [ 0:06] 2929 if (person == 1) { [ 0:06] 2930 personOnFloor_1_4 = 1; [ 0:06] 2931 } else { [ 0:06] 2932 if (person == 2) { [ 0:06] 2933 personOnFloor_2_4 = 1; [ 0:06] 2934 } else { [ 0:06] 2935 if (person == 3) { [ 0:06] 2936 personOnFloor_3_4 = 1; [ 0:06] 2937 } else { [ 0:06] 2938 if (person == 4) { [ 0:06] 2939 personOnFloor_4_4 = 1; [ 0:06] 2940 } else { [ 0:06] 2941 if (person == 5) { [ 0:06] 2942 personOnFloor_5_4 = 1; [ 0:06] 2943 } else { [ 0:06] 2944 [ 0:06] 2945 } [ 0:06] 2946 } [ 0:06] 2947 } [ 0:06] 2948 } [ 0:06] 2949 } [ 0:06] 2950 } [ 0:06] 2951 } else { [ 0:06] 2952 [ 0:06] 2953 } [ 0:06] 2954 } [ 0:06] 2955 } [ 0:06] 2956 } [ 0:06] 2957 } [ 0:06] 2958 { [ 0:06] 2959 callOnFloor(floor); [ 0:06] 2960 } [ 0:06] 2961 return; [ 0:06] 2962 } [ 0:06] 2963 } [ 0:06] 2964 void removePersonFromFloor(int person , int floor ) [ 0:06] 2965 { [ 0:06] 2966 [ 0:06] 2967 { [ 0:06] 2968 if (floor == 0) { [ 0:06] 2969 if (person == 0) { [ 0:06] 2970 personOnFloor_0_0 = 0; [ 0:06] 2971 } else { [ 0:06] 2972 if (person == 1) { [ 0:06] 2973 personOnFloor_1_0 = 0; [ 0:06] 2974 } else { [ 0:06] 2975 if (person == 2) { [ 0:06] 2976 personOnFloor_2_0 = 0; [ 0:06] 2977 } else { [ 0:06] 2978 if (person == 3) { [ 0:06] 2979 personOnFloor_3_0 = 0; [ 0:06] 2980 } else { [ 0:06] 2981 if (person == 4) { [ 0:06] 2982 personOnFloor_4_0 = 0; [ 0:06] 2983 } else { [ 0:06] 2984 if (person == 5) { [ 0:06] 2985 personOnFloor_5_0 = 0; [ 0:06] 2986 } else { [ 0:06] 2987 [ 0:06] 2988 } [ 0:06] 2989 } [ 0:06] 2990 } [ 0:06] 2991 } [ 0:06] 2992 } [ 0:06] 2993 } [ 0:06] 2994 } else { [ 0:06] 2995 if (floor == 1) { [ 0:06] 2996 if (person == 0) { [ 0:06] 2997 personOnFloor_0_1 = 0; [ 0:06] 2998 } else { [ 0:06] 2999 if (person == 1) { [ 0:06] 3000 personOnFloor_1_1 = 0; [ 0:06] 3001 } else { [ 0:06] 3002 if (person == 2) { [ 0:06] 3003 personOnFloor_2_1 = 0; [ 0:06] 3004 } else { [ 0:06] 3005 if (person == 3) { [ 0:06] 3006 personOnFloor_3_1 = 0; [ 0:06] 3007 } else { [ 0:06] 3008 if (person == 4) { [ 0:06] 3009 personOnFloor_4_1 = 0; [ 0:06] 3010 } else { [ 0:06] 3011 if (person == 5) { [ 0:06] 3012 personOnFloor_5_1 = 0; [ 0:06] 3013 } else { [ 0:06] 3014 [ 0:06] 3015 } [ 0:06] 3016 } [ 0:06] 3017 } [ 0:06] 3018 } [ 0:06] 3019 } [ 0:06] 3020 } [ 0:06] 3021 } else { [ 0:06] 3022 if (floor == 2) { [ 0:06] 3023 if (person == 0) { [ 0:06] 3024 personOnFloor_0_2 = 0; [ 0:06] 3025 } else { [ 0:06] 3026 if (person == 1) { [ 0:06] 3027 personOnFloor_1_2 = 0; [ 0:06] 3028 } else { [ 0:06] 3029 if (person == 2) { [ 0:06] 3030 personOnFloor_2_2 = 0; [ 0:06] 3031 } else { [ 0:06] 3032 if (person == 3) { [ 0:06] 3033 personOnFloor_3_2 = 0; [ 0:06] 3034 } else { [ 0:06] 3035 if (person == 4) { [ 0:06] 3036 personOnFloor_4_2 = 0; [ 0:06] 3037 } else { [ 0:06] 3038 if (person == 5) { [ 0:06] 3039 personOnFloor_5_2 = 0; [ 0:06] 3040 } else { [ 0:06] 3041 [ 0:06] 3042 } [ 0:06] 3043 } [ 0:06] 3044 } [ 0:06] 3045 } [ 0:06] 3046 } [ 0:06] 3047 } [ 0:06] 3048 } else { [ 0:06] 3049 if (floor == 3) { [ 0:06] 3050 if (person == 0) { [ 0:06] 3051 personOnFloor_0_3 = 0; [ 0:06] 3052 } else { [ 0:06] 3053 if (person == 1) { [ 0:06] 3054 personOnFloor_1_3 = 0; [ 0:06] 3055 } else { [ 0:06] 3056 if (person == 2) { [ 0:06] 3057 personOnFloor_2_3 = 0; [ 0:06] 3058 } else { [ 0:06] 3059 if (person == 3) { [ 0:06] 3060 personOnFloor_3_3 = 0; [ 0:06] 3061 } else { [ 0:06] 3062 if (person == 4) { [ 0:06] 3063 personOnFloor_4_3 = 0; [ 0:06] 3064 } else { [ 0:06] 3065 if (person == 5) { [ 0:06] 3066 personOnFloor_5_3 = 0; [ 0:06] 3067 } else { [ 0:06] 3068 [ 0:06] 3069 } [ 0:06] 3070 } [ 0:06] 3071 } [ 0:06] 3072 } [ 0:06] 3073 } [ 0:06] 3074 } [ 0:06] 3075 } else { [ 0:06] 3076 if (floor == 4) { [ 0:06] 3077 if (person == 0) { [ 0:06] 3078 personOnFloor_0_4 = 0; [ 0:06] 3079 } else { [ 0:06] 3080 if (person == 1) { [ 0:06] 3081 personOnFloor_1_4 = 0; [ 0:06] 3082 } else { [ 0:06] 3083 if (person == 2) { [ 0:06] 3084 personOnFloor_2_4 = 0; [ 0:06] 3085 } else { [ 0:06] 3086 if (person == 3) { [ 0:06] 3087 personOnFloor_3_4 = 0; [ 0:06] 3088 } else { [ 0:06] 3089 if (person == 4) { [ 0:06] 3090 personOnFloor_4_4 = 0; [ 0:06] 3091 } else { [ 0:06] 3092 if (person == 5) { [ 0:06] 3093 personOnFloor_5_4 = 0; [ 0:06] 3094 } else { [ 0:06] 3095 [ 0:06] 3096 } [ 0:06] 3097 } [ 0:06] 3098 } [ 0:06] 3099 } [ 0:06] 3100 } [ 0:06] 3101 } [ 0:06] 3102 } else { [ 0:06] 3103 [ 0:06] 3104 } [ 0:06] 3105 } [ 0:06] 3106 } [ 0:06] 3107 } [ 0:06] 3108 } [ 0:06] 3109 { [ 0:06] 3110 resetCallOnFloor(floor); [ 0:06] 3111 } [ 0:06] 3112 return; [ 0:06] 3113 } [ 0:06] 3114 } [ 0:06] 3115 int isTopFloor(int floorID ) [ 0:06] 3116 { int retValue_acc ; [ 0:06] 3117 [ 0:06] 3118 { [ 0:06] 3119 retValue_acc = floorID == 4; [ 0:06] 3120 return (retValue_acc); [ 0:06] 3121 return (retValue_acc); [ 0:06] 3122 } [ 0:06] 3123 } [ 0:06] 3124 #pragma merger(0,"Specification2_spec.i","") [ 0:06] 3125 void __automaton_fail(void) ; [ 0:06] 3126 int floorButtons_spc2_0 ; [ 0:06] 3127 int floorButtons_spc2_1 ; [ 0:06] 3128 int floorButtons_spc2_2 ; [ 0:06] 3129 int floorButtons_spc2_3 ; [ 0:06] 3130 int floorButtons_spc2_4 ; [ 0:06] 3131 void __utac_acc__Specification2_spec__1(void) [ 0:06] 3132 { [ 0:06] 3133 [ 0:06] 3134 { [ 0:06] 3135 floorButtons_spc2_0 = 0; [ 0:06] 3136 floorButtons_spc2_1 = 0; [ 0:06] 3137 floorButtons_spc2_2 = 0; [ 0:06] 3138 floorButtons_spc2_3 = 0; [ 0:06] 3139 floorButtons_spc2_4 = 0; [ 0:06] 3140 return; [ 0:06] 3141 } [ 0:06] 3142 } [ 0:06] 3143 void __utac_acc__Specification2_spec__2(int floor ) [ 0:06] 3144 { [ 0:06] 3145 [ 0:06] 3146 { [ 0:06] 3147 if (floor == 0) { [ 0:06] 3148 floorButtons_spc2_0 = 1; [ 0:06] 3149 } else { [ 0:06] 3150 if (floor == 1) { [ 0:06] 3151 floorButtons_spc2_1 = 1; [ 0:06] 3152 } else { [ 0:06] 3153 if (floor == 2) { [ 0:06] 3154 floorButtons_spc2_2 = 1; [ 0:06] 3155 } else { [ 0:06] 3156 if (floor == 3) { [ 0:06] 3157 floorButtons_spc2_3 = 1; [ 0:06] 3158 } else { [ 0:06] 3159 if (floor == 4) { [ 0:06] 3160 floorButtons_spc2_4 = 1; [ 0:06] 3161 } else { [ 0:06] 3162 [ 0:06] 3163 } [ 0:06] 3164 } [ 0:06] 3165 } [ 0:06] 3166 } [ 0:06] 3167 } [ 0:06] 3168 return; [ 0:06] 3169 } [ 0:06] 3170 } [ 0:06] 3171 void __utac_acc__Specification2_spec__3(void) [ 0:06] 3172 { int floor ; [ 0:06] 3173 int tmp ; [ 0:06] 3174 int tmp___0 ; [ 0:06] 3175 int tmp___1 ; [ 0:06] 3176 int tmp___2 ; [ 0:06] 3177 int tmp___3 ; [ 0:06] 3178 int tmp___4 ; [ 0:06] 3179 [ 0:06] 3180 { [ 0:06] 3181 { [ 0:06] 3182 tmp = getCurrentFloorID(); [ 0:06] 3183 floor = tmp; [ 0:06] 3184 } [ 0:06] 3185 if (floor == 0) { [ 0:06] 3186 if (floorButtons_spc2_0) { [ 0:06] 3187 { [ 0:06] 3188 tmp___4 = areDoorsOpen(); [ 0:06] 3189 } [ 0:06] 3190 if (tmp___4) { [ 0:06] 3191 floorButtons_spc2_0 = 0; [ 0:06] 3192 } else { [ 0:06] 3193 goto _L___6; [ 0:06] 3194 } [ 0:06] 3195 } else { [ 0:06] 3196 goto _L___6; [ 0:06] 3197 } [ 0:06] 3198 } else { [ 0:06] 3199 _L___6: /* CIL Label */ [ 0:06] 3200 if (floor == 1) { [ 0:06] 3201 if (floorButtons_spc2_1) { [ 0:06] 3202 { [ 0:06] 3203 tmp___3 = areDoorsOpen(); [ 0:06] 3204 } [ 0:06] 3205 if (tmp___3) { [ 0:06] 3206 floorButtons_spc2_1 = 0; [ 0:06] 3207 } else { [ 0:06] 3208 goto _L___4; [ 0:06] 3209 } [ 0:06] 3210 } else { [ 0:06] 3211 goto _L___4; [ 0:06] 3212 } [ 0:06] 3213 } else { [ 0:06] 3214 _L___4: /* CIL Label */ [ 0:06] 3215 if (floor == 2) { [ 0:06] 3216 if (floorButtons_spc2_2) { [ 0:06] 3217 { [ 0:06] 3218 tmp___2 = areDoorsOpen(); [ 0:06] 3219 } [ 0:06] 3220 if (tmp___2) { [ 0:06] 3221 floorButtons_spc2_2 = 0; [ 0:06] 3222 } else { [ 0:06] 3223 goto _L___2; [ 0:06] 3224 } [ 0:06] 3225 } else { [ 0:06] 3226 goto _L___2; [ 0:06] 3227 } [ 0:06] 3228 } else { [ 0:06] 3229 _L___2: /* CIL Label */ [ 0:06] 3230 if (floor == 3) { [ 0:06] 3231 if (floorButtons_spc2_3) { [ 0:06] 3232 { [ 0:06] 3233 tmp___1 = areDoorsOpen(); [ 0:06] 3234 } [ 0:06] 3235 if (tmp___1) { [ 0:06] 3236 floorButtons_spc2_3 = 0; [ 0:06] 3237 } else { [ 0:06] 3238 goto _L___0; [ 0:06] 3239 } [ 0:06] 3240 } else { [ 0:06] 3241 goto _L___0; [ 0:06] 3242 } [ 0:06] 3243 } else { [ 0:06] 3244 _L___0: /* CIL Label */ [ 0:06] 3245 if (floor == 4) { [ 0:06] 3246 if (floorButtons_spc2_4) { [ 0:06] 3247 { [ 0:06] 3248 tmp___0 = areDoorsOpen(); [ 0:06] 3249 } [ 0:06] 3250 if (tmp___0) { [ 0:06] 3251 floorButtons_spc2_4 = 0; [ 0:06] 3252 } else { [ 0:06] 3253 [ 0:06] 3254 } [ 0:06] 3255 } else { [ 0:06] 3256 [ 0:06] 3257 } [ 0:06] 3258 } else { [ 0:06] 3259 [ 0:06] 3260 } [ 0:06] 3261 } [ 0:06] 3262 } [ 0:06] 3263 } [ 0:06] 3264 } [ 0:06] 3265 return; [ 0:06] 3266 } [ 0:06] 3267 } [ 0:06] 3268 void __utac_acc__Specification2_spec__4(void) [ 0:06] 3269 { [ 0:06] 3270 [ 0:06] 3271 { [ 0:06] 3272 if (floorButtons_spc2_0) { [ 0:06] 3273 { [ 0:06] 3274 __automaton_fail(); [ 0:06] 3275 } [ 0:06] 3276 } else { [ 0:06] 3277 if (floorButtons_spc2_1) { [ 0:06] 3278 { [ 0:06] 3279 __automaton_fail(); [ 0:06] 3280 } [ 0:06] 3281 } else { [ 0:06] 3282 if (floorButtons_spc2_2) { [ 0:06] 3283 { [ 0:06] 3284 __automaton_fail(); [ 0:06] 3285 } [ 0:06] 3286 } else { [ 0:06] 3287 if (floorButtons_spc2_3) { [ 0:06] 3288 { [ 0:06] 3289 __automaton_fail(); [ 0:06] 3290 } [ 0:06] 3291 } else { [ 0:06] 3292 if (floorButtons_spc2_4) { [ 0:06] 3293 { [ 0:06] 3294 __automaton_fail(); [ 0:06] 3295 } [ 0:06] 3296 } else { [ 0:06] 3297 [ 0:06] 3298 } [ 0:06] 3299 } [ 0:06] 3300 } [ 0:06] 3301 } [ 0:06] 3302 } [ 0:06] 3303 return; [ 0:06] 3304 } [ 0:06] 3305 } [ 0:06] 3306 #pragma merger(0,"wsllib_check.i","") [ 0:06] 3307 void __automaton_fail(void) [ 0:06] 3308 { [ 0:06] 3309 [ 0:06] 3310 { [ 0:06] 3311 ERROR: __VERIFIER_error(); /* ERROR */ [ 0:06] 3312 return; [ 0:06] 3313 } [ 0:06] 3314 } [ 0:06] 3315 #pragma merger(0,"UnitTests.i","") [ 0:06] 3316 void spec1(void) [ 0:06] 3317 { int tmp ; [ 0:06] 3318 int tmp___0 ; [ 0:06] 3319 int i ; [ 0:06] 3320 int tmp___1 ; [ 0:06] 3321 [ 0:06] 3322 { [ 0:06] 3323 { [ 0:06] 3324 initBottomUp(); [ 0:06] 3325 tmp = getOrigin(5); [ 0:06] 3326 initPersonOnFloor(5, tmp); [ 0:06] 3327 printState(); [ 0:06] 3328 tmp___0 = getOrigin(2); [ 0:06] 3329 initPersonOnFloor(2, tmp___0); [ 0:06] 3330 printState(); [ 0:06] 3331 i = 0; [ 0:06] 3332 } [ 0:06] 3333 { [ 0:06] 3334 while (1) { [ 0:06] 3335 while_8_continue: /* CIL Label */ ; [ 0:06] 3336 if (i < cleanupTimeShifts) { [ 0:06] 3337 { [ 0:06] 3338 tmp___1 = isBlocked(); [ 0:06] 3339 } [ 0:06] 3340 if (tmp___1 != 1) { [ 0:06] 3341 [ 0:06] 3342 } else { [ 0:06] 3343 goto while_8_break; [ 0:06] 3344 } [ 0:06] 3345 } else { [ 0:06] 3346 goto while_8_break; [ 0:06] 3347 } [ 0:06] 3348 { [ 0:06] 3349 timeShift(); [ 0:06] 3350 printState(); [ 0:06] 3351 i = i + 1; [ 0:06] 3352 } [ 0:06] 3353 } [ 0:06] 3354 while_8_break: /* CIL Label */ ; [ 0:06] 3355 } [ 0:06] 3356 return; [ 0:06] 3357 } [ 0:06] 3358 } [ 0:06] 3359 void spec14(void) [ 0:06] 3360 { int tmp ; [ 0:06] 3361 int tmp___0 ; [ 0:06] 3362 int i ; [ 0:06] 3363 int tmp___1 ; [ 0:06] 3364 [ 0:06] 3365 { [ 0:06] 3366 { [ 0:06] 3367 initTopDown(); [ 0:06] 3368 tmp = getOrigin(5); [ 0:06] 3369 initPersonOnFloor(5, tmp); [ 0:06] 3370 printState(); [ 0:06] 3371 timeShift(); [ 0:06] 3372 timeShift(); [ 0:06] 3373 timeShift(); [ 0:06] 3374 timeShift(); [ 0:06] 3375 tmp___0 = getOrigin(0); [ 0:06] 3376 initPersonOnFloor(0, tmp___0); [ 0:06] 3377 printState(); [ 0:06] 3378 i = 0; [ 0:06] 3379 } [ 0:06] 3380 { [ 0:06] 3381 while (1) { [ 0:06] 3382 while_9_continue: /* CIL Label */ ; [ 0:06] 3383 if (i < cleanupTimeShifts) { [ 0:06] 3384 { [ 0:06] 3385 tmp___1 = isBlocked(); [ 0:06] 3386 } [ 0:06] 3387 if (tmp___1 != 1) { [ 0:06] 3388 [ 0:06] 3389 } else { [ 0:06] 3390 goto while_9_break; [ 0:06] 3391 } [ 0:06] 3392 } else { [ 0:06] 3393 goto while_9_break; [ 0:06] 3394 } [ 0:06] 3395 { [ 0:06] 3396 timeShift(); [ 0:06] 3397 printState(); [ 0:06] 3398 i = i + 1; [ 0:06] 3399 } [ 0:06] 3400 } [ 0:06] 3401 while_9_break: /* CIL Label */ ; [ 0:06] 3402 } [ 0:06] 3403 return; [ 0:06] 3404 } [ 0:06] 3405 } [ 0:06] # expected error to be found at /home/xrockai/src/divine/nightly/test/svcomp/product-lines/elevator_spec2_product26_false.cil.c:3311, but it was not