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