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