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