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