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