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