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