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