1extern int __VERIFIER_nondet_int(void);
2
3
4
5#line 2 "libacc.c"
6struct JoinPoint {
7 void **(*fp)(struct JoinPoint * ) ;
8 void **args ;
9 int argsCount ;
10 char const **argsType ;
11 void *(*arg)(int , struct JoinPoint * ) ;
12 char const *(*argType)(int , struct JoinPoint * ) ;
13 void **retValue ;
14 char const *retType ;
15 char const *funcName ;
16 char const *targetName ;
17 char const *fileName ;
18 char const *kind ;
19 void *excep_return ;
20};
21#line 18 "libacc.c"
22struct __UTAC__CFLOW_FUNC {
23 int (*func)(int , int ) ;
24 int val ;
25 struct __UTAC__CFLOW_FUNC *next ;
26};
27#line 18 "libacc.c"
28struct __UTAC__EXCEPTION {
29 void *jumpbuf ;
30 unsigned long long prtValue ;
31 int pops ;
32 struct __UTAC__CFLOW_FUNC *cflowfuncs ;
33};
34#line 211 "/usr/lib/gcc/x86_64-linux-gnu/4.4.5/include/stddef.h"
35typedef unsigned long size_t;
36#line 76 "libacc.c"
37struct __ACC__ERR {
38 void *v ;
39 struct __ACC__ERR *next ;
40};
41#line 1 "scenario.o"
42#pragma merger(0,"scenario.i","")
43#line 2 "scenario.c"
44void bigMacCall(void) ;
45#line 3
46void cleanup(void) ;
47#line 1 "scenario.c"
48void test(void)
49{
50
51 {
52 {
53#line 2
54 bigMacCall();
55#line 3
56 cleanup();
57 }
58#line 53 "scenario.c"
59 return;
60}
61}
62#line 1 "Floor.o"
63#pragma merger(0,"Floor.i","")
64#line 12 "Floor.h"
65int isFloorCalling(int floorID ) ;
66#line 14
67void resetCallOnFloor(int floorID ) ;
68#line 16
69void callOnFloor(int floorID ) ;
70#line 18
71int isPersonOnFloor(int person , int floor ) ;
72#line 20
73void initPersonOnFloor(int person , int floor ) ;
74#line 22
75void removePersonFromFloor(int person , int floor ) ;
76#line 24
77int isTopFloor(int floorID ) ;
78#line 28
79void initFloors(void) ;
80#line 9 "Floor.c"
81int calls_0 ;
82#line 11 "Floor.c"
83int calls_1 ;
84#line 13 "Floor.c"
85int calls_2 ;
86#line 15 "Floor.c"
87int calls_3 ;
88#line 17 "Floor.c"
89int calls_4 ;
90#line 20 "Floor.c"
91int personOnFloor_0_0 ;
92#line 22 "Floor.c"
93int personOnFloor_0_1 ;
94#line 24 "Floor.c"
95int personOnFloor_0_2 ;
96#line 26 "Floor.c"
97int personOnFloor_0_3 ;
98#line 28 "Floor.c"
99int personOnFloor_0_4 ;
100#line 30 "Floor.c"
101int personOnFloor_1_0 ;
102#line 32 "Floor.c"
103int personOnFloor_1_1 ;
104#line 34 "Floor.c"
105int personOnFloor_1_2 ;
106#line 36 "Floor.c"
107int personOnFloor_1_3 ;
108#line 38 "Floor.c"
109int personOnFloor_1_4 ;
110#line 40 "Floor.c"
111int personOnFloor_2_0 ;
112#line 42 "Floor.c"
113int personOnFloor_2_1 ;
114#line 44 "Floor.c"
115int personOnFloor_2_2 ;
116#line 46 "Floor.c"
117int personOnFloor_2_3 ;
118#line 48 "Floor.c"
119int personOnFloor_2_4 ;
120#line 50 "Floor.c"
121int personOnFloor_3_0 ;
122#line 52 "Floor.c"
123int personOnFloor_3_1 ;
124#line 54 "Floor.c"
125int personOnFloor_3_2 ;
126#line 56 "Floor.c"
127int personOnFloor_3_3 ;
128#line 58 "Floor.c"
129int personOnFloor_3_4 ;
130#line 60 "Floor.c"
131int personOnFloor_4_0 ;
132#line 62 "Floor.c"
133int personOnFloor_4_1 ;
134#line 64 "Floor.c"
135int personOnFloor_4_2 ;
136#line 66 "Floor.c"
137int personOnFloor_4_3 ;
138#line 68 "Floor.c"
139int personOnFloor_4_4 ;
140#line 70 "Floor.c"
141int personOnFloor_5_0 ;
142#line 72 "Floor.c"
143int personOnFloor_5_1 ;
144#line 74 "Floor.c"
145int personOnFloor_5_2 ;
146#line 76 "Floor.c"
147int personOnFloor_5_3 ;
148#line 78 "Floor.c"
149int personOnFloor_5_4 ;
150#line 81 "Floor.c"
151void initFloors(void)
152{
153
154 {
155#line 82
156 calls_0 = 0;
157#line 83
158 calls_1 = 0;
159#line 84
160 calls_2 = 0;
161#line 85
162 calls_3 = 0;
163#line 86
164 calls_4 = 0;
165#line 87
166 personOnFloor_0_0 = 0;
167#line 88
168 personOnFloor_0_1 = 0;
169#line 89
170 personOnFloor_0_2 = 0;
171#line 90
172 personOnFloor_0_3 = 0;
173#line 91
174 personOnFloor_0_4 = 0;
175#line 92
176 personOnFloor_1_0 = 0;
177#line 93
178 personOnFloor_1_1 = 0;
179#line 94
180 personOnFloor_1_2 = 0;
181#line 95
182 personOnFloor_1_3 = 0;
183#line 96
184 personOnFloor_1_4 = 0;
185#line 97
186 personOnFloor_2_0 = 0;
187#line 98
188 personOnFloor_2_1 = 0;
189#line 99
190 personOnFloor_2_2 = 0;
191#line 100
192 personOnFloor_2_3 = 0;
193#line 101
194 personOnFloor_2_4 = 0;
195#line 102
196 personOnFloor_3_0 = 0;
197#line 103
198 personOnFloor_3_1 = 0;
199#line 104
200 personOnFloor_3_2 = 0;
201#line 105
202 personOnFloor_3_3 = 0;
203#line 106
204 personOnFloor_3_4 = 0;
205#line 107
206 personOnFloor_4_0 = 0;
207#line 108
208 personOnFloor_4_1 = 0;
209#line 109
210 personOnFloor_4_2 = 0;
211#line 110
212 personOnFloor_4_3 = 0;
213#line 111
214 personOnFloor_4_4 = 0;
215#line 112
216 personOnFloor_5_0 = 0;
217#line 113
218 personOnFloor_5_1 = 0;
219#line 114
220 personOnFloor_5_2 = 0;
221#line 115
222 personOnFloor_5_3 = 0;
223#line 116
224 personOnFloor_5_4 = 0;
225#line 1120 "Floor.c"
226 return;
227}
228}
229#line 120 "Floor.c"
230int isFloorCalling(int floorID )
231{ int retValue_acc ;
232
233 {
234#line 126 "Floor.c"
235 if (floorID == 0) {
236#line 1139
237 retValue_acc = calls_0;
238#line 1141
239 return (retValue_acc);
240 } else {
241#line 1143
242 if (floorID == 1) {
243#line 1146
244 retValue_acc = calls_1;
245#line 1148
246 return (retValue_acc);
247 } else {
248#line 1150
249 if (floorID == 2) {
250#line 1153
251 retValue_acc = calls_2;
252#line 1155
253 return (retValue_acc);
254 } else {
255#line 1157
256 if (floorID == 3) {
257#line 1160
258 retValue_acc = calls_3;
259#line 1162
260 return (retValue_acc);
261 } else {
262#line 1164
263 if (floorID == 4) {
264#line 1167 "Floor.c"
265 retValue_acc = calls_4;
266#line 1169
267 return (retValue_acc);
268 } else {
269
270 }
271 }
272 }
273 }
274 }
275#line 1174 "Floor.c"
276 retValue_acc = 0;
277#line 1176
278 return (retValue_acc);
279#line 1183
280 return (retValue_acc);
281}
282}
283#line 130 "Floor.c"
284void resetCallOnFloor(int floorID )
285{
286
287 {
288#line 136
289 if (floorID == 0) {
290#line 137
291 calls_0 = 0;
292 } else {
293#line 138
294 if (floorID == 1) {
295#line 139
296 calls_1 = 0;
297 } else {
298#line 140
299 if (floorID == 2) {
300#line 141
301 calls_2 = 0;
302 } else {
303#line 142
304 if (floorID == 3) {
305#line 143
306 calls_3 = 0;
307 } else {
308#line 144
309 if (floorID == 4) {
310#line 145
311 calls_4 = 0;
312 } else {
313
314 }
315 }
316 }
317 }
318 }
319#line 1216 "Floor.c"
320 return;
321}
322}
323#line 139 "Floor.c"
324void callOnFloor(int floorID )
325{
326
327 {
328#line 145
329 if (floorID == 0) {
330#line 146
331 calls_0 = 1;
332 } else {
333#line 147
334 if (floorID == 1) {
335#line 148
336 calls_1 = 1;
337 } else {
338#line 149
339 if (floorID == 2) {
340#line 150
341 calls_2 = 1;
342 } else {
343#line 151
344 if (floorID == 3) {
345#line 152
346 calls_3 = 1;
347 } else {
348#line 153
349 if (floorID == 4) {
350#line 154
351 calls_4 = 1;
352 } else {
353
354 }
355 }
356 }
357 }
358 }
359#line 1245 "Floor.c"
360 return;
361}
362}
363#line 148 "Floor.c"
364int isPersonOnFloor(int person , int floor )
365{ int retValue_acc ;
366
367 {
368#line 185
369 if (floor == 0) {
370#line 156 "Floor.c"
371 if (person == 0) {
372#line 1267
373 retValue_acc = personOnFloor_0_0;
374#line 1269
375 return (retValue_acc);
376 } else {
377#line 1271
378 if (person == 1) {
379#line 1274
380 retValue_acc = personOnFloor_1_0;
381#line 1276
382 return (retValue_acc);
383 } else {
384#line 1278
385 if (person == 2) {
386#line 1281
387 retValue_acc = personOnFloor_2_0;
388#line 1283
389 return (retValue_acc);
390 } else {
391#line 1285
392 if (person == 3) {
393#line 1288
394 retValue_acc = personOnFloor_3_0;
395#line 1290
396 return (retValue_acc);
397 } else {
398#line 1292
399 if (person == 4) {
400#line 1295
401 retValue_acc = personOnFloor_4_0;
402#line 1297
403 return (retValue_acc);
404 } else {
405#line 1299
406 if (person == 5) {
407#line 1302
408 retValue_acc = personOnFloor_5_0;
409#line 1304
410 return (retValue_acc);
411 } else {
412
413 }
414 }
415 }
416 }
417 }
418 }
419 } else {
420#line 1306 "Floor.c"
421 if (floor == 1) {
422#line 163 "Floor.c"
423 if (person == 0) {
424#line 1312
425 retValue_acc = personOnFloor_0_1;
426#line 1314
427 return (retValue_acc);
428 } else {
429#line 1316
430 if (person == 1) {
431#line 1319
432 retValue_acc = personOnFloor_1_1;
433#line 1321
434 return (retValue_acc);
435 } else {
436#line 1323
437 if (person == 2) {
438#line 1326
439 retValue_acc = personOnFloor_2_1;
440#line 1328
441 return (retValue_acc);
442 } else {
443#line 1330
444 if (person == 3) {
445#line 1333
446 retValue_acc = personOnFloor_3_1;
447#line 1335
448 return (retValue_acc);
449 } else {
450#line 1337
451 if (person == 4) {
452#line 1340
453 retValue_acc = personOnFloor_4_1;
454#line 1342
455 return (retValue_acc);
456 } else {
457#line 1344
458 if (person == 5) {
459#line 1347
460 retValue_acc = personOnFloor_5_1;
461#line 1349
462 return (retValue_acc);
463 } else {
464
465 }
466 }
467 }
468 }
469 }
470 }
471 } else {
472#line 1351 "Floor.c"
473 if (floor == 2) {
474#line 170 "Floor.c"
475 if (person == 0) {
476#line 1357
477 retValue_acc = personOnFloor_0_2;
478#line 1359
479 return (retValue_acc);
480 } else {
481#line 1361
482 if (person == 1) {
483#line 1364
484 retValue_acc = personOnFloor_1_2;
485#line 1366
486 return (retValue_acc);
487 } else {
488#line 1368
489 if (person == 2) {
490#line 1371
491 retValue_acc = personOnFloor_2_2;
492#line 1373
493 return (retValue_acc);
494 } else {
495#line 1375
496 if (person == 3) {
497#line 1378
498 retValue_acc = personOnFloor_3_2;
499#line 1380
500 return (retValue_acc);
501 } else {
502#line 1382
503 if (person == 4) {
504#line 1385
505 retValue_acc = personOnFloor_4_2;
506#line 1387
507 return (retValue_acc);
508 } else {
509#line 1389
510 if (person == 5) {
511#line 1392
512 retValue_acc = personOnFloor_5_2;
513#line 1394
514 return (retValue_acc);
515 } else {
516
517 }
518 }
519 }
520 }
521 }
522 }
523 } else {
524#line 1396 "Floor.c"
525 if (floor == 3) {
526#line 177 "Floor.c"
527 if (person == 0) {
528#line 1402
529 retValue_acc = personOnFloor_0_3;
530#line 1404
531 return (retValue_acc);
532 } else {
533#line 1406
534 if (person == 1) {
535#line 1409
536 retValue_acc = personOnFloor_1_3;
537#line 1411
538 return (retValue_acc);
539 } else {
540#line 1413
541 if (person == 2) {
542#line 1416
543 retValue_acc = personOnFloor_2_3;
544#line 1418
545 return (retValue_acc);
546 } else {
547#line 1420
548 if (person == 3) {
549#line 1423
550 retValue_acc = personOnFloor_3_3;
551#line 1425
552 return (retValue_acc);
553 } else {
554#line 1427
555 if (person == 4) {
556#line 1430
557 retValue_acc = personOnFloor_4_3;
558#line 1432
559 return (retValue_acc);
560 } else {
561#line 1434
562 if (person == 5) {
563#line 1437
564 retValue_acc = personOnFloor_5_3;
565#line 1439
566 return (retValue_acc);
567 } else {
568
569 }
570 }
571 }
572 }
573 }
574 }
575 } else {
576#line 1441 "Floor.c"
577 if (floor == 4) {
578#line 184 "Floor.c"
579 if (person == 0) {
580#line 1447
581 retValue_acc = personOnFloor_0_4;
582#line 1449
583 return (retValue_acc);
584 } else {
585#line 1451
586 if (person == 1) {
587#line 1454
588 retValue_acc = personOnFloor_1_4;
589#line 1456
590 return (retValue_acc);
591 } else {
592#line 1458
593 if (person == 2) {
594#line 1461
595 retValue_acc = personOnFloor_2_4;
596#line 1463
597 return (retValue_acc);
598 } else {
599#line 1465
600 if (person == 3) {
601#line 1468
602 retValue_acc = personOnFloor_3_4;
603#line 1470
604 return (retValue_acc);
605 } else {
606#line 1472
607 if (person == 4) {
608#line 1475
609 retValue_acc = personOnFloor_4_4;
610#line 1477
611 return (retValue_acc);
612 } else {
613#line 1479
614 if (person == 5) {
615#line 1482 "Floor.c"
616 retValue_acc = personOnFloor_5_4;
617#line 1484
618 return (retValue_acc);
619 } else {
620
621 }
622 }
623 }
624 }
625 }
626 }
627 } else {
628
629 }
630 }
631 }
632 }
633 }
634#line 1489 "Floor.c"
635 retValue_acc = 0;
636#line 1491
637 return (retValue_acc);
638#line 1498
639 return (retValue_acc);
640}
641}
642#line 188 "Floor.c"
643void initPersonOnFloor(int person , int floor )
644{
645
646 {
647#line 225
648 if (floor == 0) {
649#line 196
650 if (person == 0) {
651#line 197
652 personOnFloor_0_0 = 1;
653 } else {
654#line 198
655 if (person == 1) {
656#line 199
657 personOnFloor_1_0 = 1;
658 } else {
659#line 200
660 if (person == 2) {
661#line 201
662 personOnFloor_2_0 = 1;
663 } else {
664#line 202
665 if (person == 3) {
666#line 203
667 personOnFloor_3_0 = 1;
668 } else {
669#line 204
670 if (person == 4) {
671#line 205
672 personOnFloor_4_0 = 1;
673 } else {
674#line 206
675 if (person == 5) {
676#line 207
677 personOnFloor_5_0 = 1;
678 } else {
679
680 }
681 }
682 }
683 }
684 }
685 }
686 } else {
687#line 208
688 if (floor == 1) {
689#line 203
690 if (person == 0) {
691#line 204
692 personOnFloor_0_1 = 1;
693 } else {
694#line 205
695 if (person == 1) {
696#line 206
697 personOnFloor_1_1 = 1;
698 } else {
699#line 207
700 if (person == 2) {
701#line 208
702 personOnFloor_2_1 = 1;
703 } else {
704#line 209
705 if (person == 3) {
706#line 210
707 personOnFloor_3_1 = 1;
708 } else {
709#line 211
710 if (person == 4) {
711#line 212
712 personOnFloor_4_1 = 1;
713 } else {
714#line 213
715 if (person == 5) {
716#line 214
717 personOnFloor_5_1 = 1;
718 } else {
719
720 }
721 }
722 }
723 }
724 }
725 }
726 } else {
727#line 215
728 if (floor == 2) {
729#line 210
730 if (person == 0) {
731#line 211
732 personOnFloor_0_2 = 1;
733 } else {
734#line 212
735 if (person == 1) {
736#line 213
737 personOnFloor_1_2 = 1;
738 } else {
739#line 214
740 if (person == 2) {
741#line 215
742 personOnFloor_2_2 = 1;
743 } else {
744#line 216
745 if (person == 3) {
746#line 217
747 personOnFloor_3_2 = 1;
748 } else {
749#line 218
750 if (person == 4) {
751#line 219
752 personOnFloor_4_2 = 1;
753 } else {
754#line 220
755 if (person == 5) {
756#line 221
757 personOnFloor_5_2 = 1;
758 } else {
759
760 }
761 }
762 }
763 }
764 }
765 }
766 } else {
767#line 222
768 if (floor == 3) {
769#line 217
770 if (person == 0) {
771#line 218
772 personOnFloor_0_3 = 1;
773 } else {
774#line 219
775 if (person == 1) {
776#line 220
777 personOnFloor_1_3 = 1;
778 } else {
779#line 221
780 if (person == 2) {
781#line 222
782 personOnFloor_2_3 = 1;
783 } else {
784#line 223
785 if (person == 3) {
786#line 224
787 personOnFloor_3_3 = 1;
788 } else {
789#line 225
790 if (person == 4) {
791#line 226
792 personOnFloor_4_3 = 1;
793 } else {
794#line 227
795 if (person == 5) {
796#line 228
797 personOnFloor_5_3 = 1;
798 } else {
799
800 }
801 }
802 }
803 }
804 }
805 }
806 } else {
807#line 229
808 if (floor == 4) {
809#line 224
810 if (person == 0) {
811#line 225
812 personOnFloor_0_4 = 1;
813 } else {
814#line 226
815 if (person == 1) {
816#line 227
817 personOnFloor_1_4 = 1;
818 } else {
819#line 228
820 if (person == 2) {
821#line 229
822 personOnFloor_2_4 = 1;
823 } else {
824#line 230
825 if (person == 3) {
826#line 231
827 personOnFloor_3_4 = 1;
828 } else {
829#line 232
830 if (person == 4) {
831#line 233
832 personOnFloor_4_4 = 1;
833 } else {
834#line 234
835 if (person == 5) {
836#line 235
837 personOnFloor_5_4 = 1;
838 } else {
839
840 }
841 }
842 }
843 }
844 }
845 }
846 } else {
847
848 }
849 }
850 }
851 }
852 }
853 {
854#line 225
855 callOnFloor(floor);
856 }
857#line 1598 "Floor.c"
858 return;
859}
860}
861#line 228 "Floor.c"
862void removePersonFromFloor(int person , int floor )
863{
864
865 {
866#line 265
867 if (floor == 0) {
868#line 236
869 if (person == 0) {
870#line 237
871 personOnFloor_0_0 = 0;
872 } else {
873#line 238
874 if (person == 1) {
875#line 239
876 personOnFloor_1_0 = 0;
877 } else {
878#line 240
879 if (person == 2) {
880#line 241
881 personOnFloor_2_0 = 0;
882 } else {
883#line 242
884 if (person == 3) {
885#line 243
886 personOnFloor_3_0 = 0;
887 } else {
888#line 244
889 if (person == 4) {
890#line 245
891 personOnFloor_4_0 = 0;
892 } else {
893#line 246
894 if (person == 5) {
895#line 247
896 personOnFloor_5_0 = 0;
897 } else {
898
899 }
900 }
901 }
902 }
903 }
904 }
905 } else {
906#line 248
907 if (floor == 1) {
908#line 243
909 if (person == 0) {
910#line 244
911 personOnFloor_0_1 = 0;
912 } else {
913#line 245
914 if (person == 1) {
915#line 246
916 personOnFloor_1_1 = 0;
917 } else {
918#line 247
919 if (person == 2) {
920#line 248
921 personOnFloor_2_1 = 0;
922 } else {
923#line 249
924 if (person == 3) {
925#line 250
926 personOnFloor_3_1 = 0;
927 } else {
928#line 251
929 if (person == 4) {
930#line 252
931 personOnFloor_4_1 = 0;
932 } else {
933#line 253
934 if (person == 5) {
935#line 254
936 personOnFloor_5_1 = 0;
937 } else {
938
939 }
940 }
941 }
942 }
943 }
944 }
945 } else {
946#line 255
947 if (floor == 2) {
948#line 250
949 if (person == 0) {
950#line 251
951 personOnFloor_0_2 = 0;
952 } else {
953#line 252
954 if (person == 1) {
955#line 253
956 personOnFloor_1_2 = 0;
957 } else {
958#line 254
959 if (person == 2) {
960#line 255
961 personOnFloor_2_2 = 0;
962 } else {
963#line 256
964 if (person == 3) {
965#line 257
966 personOnFloor_3_2 = 0;
967 } else {
968#line 258
969 if (person == 4) {
970#line 259
971 personOnFloor_4_2 = 0;
972 } else {
973#line 260
974 if (person == 5) {
975#line 261
976 personOnFloor_5_2 = 0;
977 } else {
978
979 }
980 }
981 }
982 }
983 }
984 }
985 } else {
986#line 262
987 if (floor == 3) {
988#line 257
989 if (person == 0) {
990#line 258
991 personOnFloor_0_3 = 0;
992 } else {
993#line 259
994 if (person == 1) {
995#line 260
996 personOnFloor_1_3 = 0;
997 } else {
998#line 261
999 if (person == 2) {
1000#line 262
1001 personOnFloor_2_3 = 0;
1002 } else {
1003#line 263
1004 if (person == 3) {
1005#line 264
1006 personOnFloor_3_3 = 0;
1007 } else {
1008#line 265
1009 if (person == 4) {
1010#line 266
1011 personOnFloor_4_3 = 0;
1012 } else {
1013#line 267
1014 if (person == 5) {
1015#line 268
1016 personOnFloor_5_3 = 0;
1017 } else {
1018
1019 }
1020 }
1021 }
1022 }
1023 }
1024 }
1025 } else {
1026#line 269
1027 if (floor == 4) {
1028#line 264
1029 if (person == 0) {
1030#line 265
1031 personOnFloor_0_4 = 0;
1032 } else {
1033#line 266
1034 if (person == 1) {
1035#line 267
1036 personOnFloor_1_4 = 0;
1037 } else {
1038#line 268
1039 if (person == 2) {
1040#line 269
1041 personOnFloor_2_4 = 0;
1042 } else {
1043#line 270
1044 if (person == 3) {
1045#line 271
1046 personOnFloor_3_4 = 0;
1047 } else {
1048#line 272
1049 if (person == 4) {
1050#line 273
1051 personOnFloor_4_4 = 0;
1052 } else {
1053#line 274
1054 if (person == 5) {
1055#line 275
1056 personOnFloor_5_4 = 0;
1057 } else {
1058
1059 }
1060 }
1061 }
1062 }
1063 }
1064 }
1065 } else {
1066
1067 }
1068 }
1069 }
1070 }
1071 }
1072 {
1073#line 265
1074 resetCallOnFloor(floor);
1075 }
1076#line 1694 "Floor.c"
1077 return;
1078}
1079}
1080#line 268 "Floor.c"
1081int isTopFloor(int floorID )
1082{ int retValue_acc ;
1083
1084 {
1085#line 1712 "Floor.c"
1086 retValue_acc = floorID == 4;
1087#line 1714
1088 return (retValue_acc);
1089#line 1721
1090 return (retValue_acc);
1091}
1092}
1093#line 1 "Test.o"
1094#pragma merger(0,"Test.i","")
1095#line 544 "/usr/include/stdlib.h"
1096extern __attribute__((__nothrow__, __noreturn__)) void exit(int __status ) ;
1097#line 13 "Test.c"
1098int cleanupTimeShifts = 12;
1099#line 17 "Test.c"
1100#line 23 "Test.c"
1101int get_nondetMinMax07(void)
1102{ int retValue_acc ;
1103 int nd ;
1104 nd = __VERIFIER_nondet_int();
1105
1106 {
1107#line 26 "Test.c"
1108 if (nd == 0) {
1109#line 1108
1110 retValue_acc = 0;
1111#line 1110
1112 return (retValue_acc);
1113 } else {
1114#line 1112
1115 if (nd == 1) {
1116#line 1117
1117 retValue_acc = 1;
1118#line 1119
1119 return (retValue_acc);
1120 } else {
1121#line 1121
1122 if (nd == 2) {
1123#line 1126
1124 retValue_acc = 2;
1125#line 1128
1126 return (retValue_acc);
1127 } else {
1128#line 1130
1129 if (nd == 3) {
1130#line 1135
1131 retValue_acc = 3;
1132#line 1137
1133 return (retValue_acc);
1134 } else {
1135#line 1139
1136 if (nd == 4) {
1137#line 1144
1138 retValue_acc = 4;
1139#line 1146
1140 return (retValue_acc);
1141 } else {
1142#line 1148
1143 if (nd == 5) {
1144#line 1153
1145 retValue_acc = 5;
1146#line 1155
1147 return (retValue_acc);
1148 } else {
1149#line 1157
1150 if (nd == 6) {
1151#line 1162
1152 retValue_acc = 6;
1153#line 1164
1154 return (retValue_acc);
1155 } else {
1156#line 1166
1157 if (nd == 7) {
1158#line 1171 "Test.c"
1159 retValue_acc = 7;
1160#line 1173
1161 return (retValue_acc);
1162 } else {
1163 {
1164#line 43
1165 exit(0);
1166 }
1167 }
1168 }
1169 }
1170 }
1171 }
1172 }
1173 }
1174 }
1175#line 1183 "Test.c"
1176 return (retValue_acc);
1177}
1178}
1179#line 48 "Test.c"
1180int getOrigin(int person ) ;
1181#line 48 "Test.c"
1182void bobCall(void)
1183{ int tmp ;
1184
1185 {
1186 {
1187#line 48
1188 tmp = getOrigin(0);
1189#line 48
1190 initPersonOnFloor(0, tmp);
1191 }
1192#line 1207 "Test.c"
1193 return;
1194}
1195}
1196#line 50 "Test.c"
1197void aliceCall(void)
1198{ int tmp ;
1199
1200 {
1201 {
1202#line 50
1203 tmp = getOrigin(1);
1204#line 50
1205 initPersonOnFloor(1, tmp);
1206 }
1207#line 1227 "Test.c"
1208 return;
1209}
1210}
1211#line 52 "Test.c"
1212void angelinaCall(void)
1213{ int tmp ;
1214
1215 {
1216 {
1217#line 52
1218 tmp = getOrigin(2);
1219#line 52
1220 initPersonOnFloor(2, tmp);
1221 }
1222#line 1247 "Test.c"
1223 return;
1224}
1225}
1226#line 54 "Test.c"
1227void chuckCall(void)
1228{ int tmp ;
1229
1230 {
1231 {
1232#line 54
1233 tmp = getOrigin(3);
1234#line 54
1235 initPersonOnFloor(3, tmp);
1236 }
1237#line 1267 "Test.c"
1238 return;
1239}
1240}
1241#line 56 "Test.c"
1242void monicaCall(void)
1243{ int tmp ;
1244
1245 {
1246 {
1247#line 56
1248 tmp = getOrigin(4);
1249#line 56
1250 initPersonOnFloor(4, tmp);
1251 }
1252#line 1287 "Test.c"
1253 return;
1254}
1255}
1256#line 58 "Test.c"
1257void bigMacCall(void)
1258{ int tmp ;
1259
1260 {
1261 {
1262#line 58
1263 tmp = getOrigin(5);
1264#line 58
1265 initPersonOnFloor(5, tmp);
1266 }
1267#line 1307 "Test.c"
1268 return;
1269}
1270}
1271#line 60 "Test.c"
1272void timeShift(void) ;
1273#line 60 "Test.c"
1274void threeTS(void)
1275{
1276
1277 {
1278 {
1279#line 60
1280 timeShift();
1281#line 60
1282 timeShift();
1283#line 60
1284 timeShift();
1285 }
1286#line 1331 "Test.c"
1287 return;
1288}
1289}
1290#line 71 "Test.c"
1291int isIdle(void) ;
1292#line 67
1293int isBlocked(void) ;
1294#line 62 "Test.c"
1295void cleanup(void)
1296{ int i ;
1297 int tmp ;
1298 int tmp___0 ;
1299 int __cil_tmp4 ;
1300
1301 {
1302 {
1303#line 65
1304 timeShift();
1305#line 67
1306 i = 0;
1307 }
1308 {
1309#line 67
1310 while (1) {
1311 while_0_continue: ;
1312 {
1313#line 67
1314 __cil_tmp4 = cleanupTimeShifts - 1;
1315#line 67
1316 if (i < __cil_tmp4) {
1317 {
1318#line 67
1319 tmp___0 = isBlocked();
1320 }
1321#line 67
1322 if (tmp___0 != 1) {
1323
1324 } else {
1325 goto while_0_break;
1326 }
1327 } else {
1328 goto while_0_break;
1329 }
1330 }
1331 {
1332#line 71
1333 tmp = isIdle();
1334 }
1335#line 71
1336 if (tmp) {
1337#line 72
1338 return;
1339 } else {
1340 {
1341#line 74
1342 timeShift();
1343 }
1344 }
1345#line 67
1346 i = i + 1;
1347 }
1348 while_0_break: ;
1349 }
1350#line 1362 "Test.c"
1351 return;
1352}
1353}
1354#line 81 "Test.c"
1355void initTopDown(void) ;
1356#line 85
1357void initBottomUp(void) ;
1358#line 77 "Test.c"
1359void randomSequenceOfActions(void)
1360{ int maxLength ;
1361 int tmp ;
1362 int counter ;
1363 int action ;
1364 int tmp___0 ;
1365 int origin ;
1366 int tmp___1 ;
1367 int tmp___2 ;
1368
1369 {
1370 {
1371#line 78
1372 maxLength = 4;
1373#line 79
1374 tmp = __VERIFIER_nondet_int();
1375 }
1376#line 79
1377 if (tmp) {
1378 {
1379#line 81
1380 initTopDown();
1381 }
1382 } else {
1383 {
1384#line 85
1385 initBottomUp();
1386 }
1387 }
1388#line 90
1389 counter = 0;
1390 {
1391#line 91
1392 while (1) {
1393 while_1_continue: ;
1394#line 91
1395 if (counter < maxLength) {
1396
1397 } else {
1398 goto while_1_break;
1399 }
1400 {
1401#line 92
1402 counter = counter + 1;
1403#line 93
1404 tmp___0 = get_nondetMinMax07();
1405#line 93
1406 action = tmp___0;
1407 }
1408#line 99
1409 if (action < 6) {
1410 {
1411#line 100
1412 tmp___1 = getOrigin(action);
1413#line 100
1414 origin = tmp___1;
1415#line 101
1416 initPersonOnFloor(action, origin);
1417 }
1418 } else {
1419#line 102
1420 if (action == 6) {
1421 {
1422#line 103
1423 timeShift();
1424 }
1425 } else {
1426#line 104
1427 if (action == 7) {
1428 {
1429#line 106
1430 timeShift();
1431#line 107
1432 timeShift();
1433#line 108
1434 timeShift();
1435 }
1436 } else {
1437
1438 }
1439 }
1440 }
1441 {
1442#line 113
1443 tmp___2 = isBlocked();
1444 }
1445#line 113
1446 if (tmp___2) {
1447#line 114
1448 return;
1449 } else {
1450
1451 }
1452 }
1453 while_1_break: ;
1454 }
1455 {
1456#line 117
1457 cleanup();
1458 }
1459#line 1433 "Test.c"
1460 return;
1461}
1462}
1463#line 122 "Test.c"
1464void runTest_Simple(void)
1465{
1466
1467 {
1468 {
1469#line 123
1470 bigMacCall();
1471#line 124
1472 angelinaCall();
1473#line 125
1474 cleanup();
1475 }
1476#line 1457 "Test.c"
1477 return;
1478}
1479}
1480#line 130 "Test.c"
1481void Specification1(void)
1482{
1483
1484 {
1485 {
1486#line 131
1487 bigMacCall();
1488#line 132
1489 angelinaCall();
1490#line 133
1491 cleanup();
1492 }
1493#line 1481 "Test.c"
1494 return;
1495}
1496}
1497#line 137 "Test.c"
1498void Specification2(void)
1499{
1500
1501 {
1502 {
1503#line 138
1504 bigMacCall();
1505#line 139
1506 cleanup();
1507 }
1508#line 1503 "Test.c"
1509 return;
1510}
1511}
1512#line 142 "Test.c"
1513void Specification3(void)
1514{
1515
1516 {
1517 {
1518#line 143
1519 bobCall();
1520#line 144
1521 timeShift();
1522#line 145
1523 timeShift();
1524#line 146
1525 timeShift();
1526#line 147
1527 timeShift();
1528#line 149
1529 timeShift();
1530#line 154
1531 bobCall();
1532#line 155
1533 cleanup();
1534 }
1535#line 1537 "Test.c"
1536 return;
1537}
1538}
1539#line 160 "Test.c"
1540void setup(void)
1541{
1542
1543 {
1544#line 1555 "Test.c"
1545 return;
1546}
1547}
1548#line 1557
1549void __utac_acc__Specification9_spec__1(void) ;
1550#line 1560
1551void __utac_acc__Specification9_spec__4(void) ;
1552#line 165 "Test.c"
1553void runTest(void)
1554{
1555
1556 {
1557 {
1558#line 1571 "Test.c"
1559 __utac_acc__Specification9_spec__1();
1560#line 168 "Test.c"
1561 test();
1562#line 1585 "Test.c"
1563 __utac_acc__Specification9_spec__4();
1564 }
1565#line 1591
1566 return;
1567}
1568}
1569#line 174 "Test.c"
1570void select_helpers(void) ;
1571#line 175
1572void select_features(void) ;
1573#line 176
1574int valid_product(void) ;
1575#line 173 "Test.c"
1576int main(void)
1577{ int retValue_acc ;
1578 int tmp ;
1579
1580 {
1581 {
1582#line 174
1583 select_helpers();
1584#line 175
1585 select_features();
1586#line 176
1587 tmp = valid_product();
1588 }
1589#line 176
1590 if (tmp) {
1591 {
1592#line 177
1593 setup();
1594#line 178
1595 runTest();
1596 }
1597 } else {
1598
1599 }
1600#line 1620 "Test.c"
1601 retValue_acc = 0;
1602#line 1622
1603 return (retValue_acc);
1604#line 1629
1605 return (retValue_acc);
1606}
1607}
1608#line 1 "Elevator.o"
1609#pragma merger(0,"Elevator.i","")
1610#line 359 "/usr/include/stdio.h"
1611extern int printf(char const * __restrict __format , ...) ;
1612#line 14 "Person.h"
1613int getDestination(int person ) ;
1614#line 16
1615void enterElevator(int p ) ;
1616#line 18 "Elevator.h"
1617void printState(void) ;
1618#line 20
1619int isEmpty(void) ;
1620#line 22
1621int isAnyLiftButtonPressed(void) ;
1622#line 24
1623int buttonForFloorIsPressed(int floorID ) ;
1624#line 32
1625int areDoorsOpen(void) ;
1626#line 34
1627int getCurrentFloorID(void) ;
1628#line 16 "Elevator.c"
1629int currentHeading = 1;
1630#line 18 "Elevator.c"
1631int currentFloorID = 0;
1632#line 20 "Elevator.c"
1633int persons_0 ;
1634#line 22 "Elevator.c"
1635int persons_1 ;
1636#line 24 "Elevator.c"
1637int persons_2 ;
1638#line 26 "Elevator.c"
1639int persons_3 ;
1640#line 28 "Elevator.c"
1641int persons_4 ;
1642#line 30 "Elevator.c"
1643int persons_5 ;
1644#line 33 "Elevator.c"
1645int doorState = 1;
1646#line 35 "Elevator.c"
1647int floorButtons_0 ;
1648#line 37 "Elevator.c"
1649int floorButtons_1 ;
1650#line 39 "Elevator.c"
1651int floorButtons_2 ;
1652#line 41 "Elevator.c"
1653int floorButtons_3 ;
1654#line 43 "Elevator.c"
1655int floorButtons_4 ;
1656#line 51 "Elevator.c"
1657void initTopDown(void)
1658{
1659
1660 {
1661 {
1662#line 52
1663 currentFloorID = 4;
1664#line 53
1665 currentHeading = 0;
1666#line 54
1667 floorButtons_0 = 0;
1668#line 55
1669 floorButtons_1 = 0;
1670#line 56
1671 floorButtons_2 = 0;
1672#line 57
1673 floorButtons_3 = 0;
1674#line 58
1675 floorButtons_4 = 0;
1676#line 59
1677 persons_0 = 0;
1678#line 60
1679 persons_1 = 0;
1680#line 61
1681 persons_2 = 0;
1682#line 62
1683 persons_3 = 0;
1684#line 63
1685 persons_4 = 0;
1686#line 64
1687 persons_5 = 0;
1688#line 65
1689 initFloors();
1690 }
1691#line 1071 "Elevator.c"
1692 return;
1693}
1694}
1695#line 68 "Elevator.c"
1696void initBottomUp(void)
1697{
1698
1699 {
1700 {
1701#line 69
1702 currentFloorID = 0;
1703#line 70
1704 currentHeading = 1;
1705#line 71
1706 floorButtons_0 = 0;
1707#line 72
1708 floorButtons_1 = 0;
1709#line 73
1710 floorButtons_2 = 0;
1711#line 74
1712 floorButtons_3 = 0;
1713#line 75
1714 floorButtons_4 = 0;
1715#line 76
1716 persons_0 = 0;
1717#line 77
1718 persons_1 = 0;
1719#line 78
1720 persons_2 = 0;
1721#line 79
1722 persons_3 = 0;
1723#line 80
1724 persons_4 = 0;
1725#line 81
1726 persons_5 = 0;
1727#line 82
1728 initFloors();
1729 }
1730#line 1117 "Elevator.c"
1731 return;
1732}
1733}
1734#line 86 "Elevator.c"
1735int isBlocked(void)
1736{ int retValue_acc ;
1737
1738 {
1739#line 1135 "Elevator.c"
1740 retValue_acc = 0;
1741#line 1137
1742 return (retValue_acc);
1743#line 1144
1744 return (retValue_acc);
1745}
1746}
1747#line 91 "Elevator.c"
1748void enterElevator(int p )
1749{
1750
1751 {
1752#line 100
1753 if (p == 0) {
1754#line 101
1755 persons_0 = 1;
1756 } else {
1757#line 102
1758 if (p == 1) {
1759#line 103
1760 persons_1 = 1;
1761 } else {
1762#line 104
1763 if (p == 2) {
1764#line 105
1765 persons_2 = 1;
1766 } else {
1767#line 106
1768 if (p == 3) {
1769#line 107
1770 persons_3 = 1;
1771 } else {
1772#line 108
1773 if (p == 4) {
1774#line 109
1775 persons_4 = 1;
1776 } else {
1777#line 110
1778 if (p == 5) {
1779#line 111
1780 persons_5 = 1;
1781 } else {
1782
1783 }
1784 }
1785 }
1786 }
1787 }
1788 }
1789#line 1179 "Elevator.c"
1790 return;
1791}
1792}
1793#line 102 "Elevator.c"
1794void leaveElevator__wrappee__base(int p )
1795{
1796
1797 {
1798#line 110
1799 if (p == 0) {
1800#line 111
1801 persons_0 = 0;
1802 } else {
1803#line 112
1804 if (p == 1) {
1805#line 113
1806 persons_1 = 0;
1807 } else {
1808#line 114
1809 if (p == 2) {
1810#line 115
1811 persons_2 = 0;
1812 } else {
1813#line 116
1814 if (p == 3) {
1815#line 117
1816 persons_3 = 0;
1817 } else {
1818#line 118
1819 if (p == 4) {
1820#line 119
1821 persons_4 = 0;
1822 } else {
1823#line 120
1824 if (p == 5) {
1825#line 121
1826 persons_5 = 0;
1827 } else {
1828
1829 }
1830 }
1831 }
1832 }
1833 }
1834 }
1835#line 1210 "Elevator.c"
1836 return;
1837}
1838}
1839#line 113 "Elevator.c"
1840void leaveElevator(int p )
1841{ int tmp ;
1842
1843 {
1844 {
1845#line 114
1846 leaveElevator__wrappee__base(p);
1847#line 116
1848 tmp = isEmpty();
1849 }
1850#line 116
1851 if (tmp) {
1852#line 117
1853 floorButtons_0 = 0;
1854#line 118
1855 floorButtons_1 = 0;
1856#line 119
1857 floorButtons_2 = 0;
1858#line 120
1859 floorButtons_3 = 0;
1860#line 121
1861 floorButtons_4 = 0;
1862 } else {
1863
1864 }
1865#line 1243 "Elevator.c"
1866 return;
1867}
1868}
1869#line 1245
1870void __utac_acc__Specification9_spec__2(int floor ) ;
1871#line 125 "Elevator.c"
1872void pressInLiftFloorButton(int floorID )
1873{ int __utac__ad__arg1 ;
1874
1875 {
1876 {
1877#line 1256 "Elevator.c"
1878 __utac__ad__arg1 = floorID;
1879#line 1257
1880 __utac_acc__Specification9_spec__2(__utac__ad__arg1);
1881 }
1882#line 131
1883 if (floorID == 0) {
1884#line 132
1885 floorButtons_0 = 1;
1886 } else {
1887#line 133
1888 if (floorID == 1) {
1889#line 134
1890 floorButtons_1 = 1;
1891 } else {
1892#line 135
1893 if (floorID == 2) {
1894#line 136
1895 floorButtons_2 = 1;
1896 } else {
1897#line 137
1898 if (floorID == 3) {
1899#line 138
1900 floorButtons_3 = 1;
1901 } else {
1902#line 139
1903 if (floorID == 4) {
1904#line 140 "Elevator.c"
1905 floorButtons_4 = 1;
1906 } else {
1907
1908 }
1909 }
1910 }
1911 }
1912 }
1913#line 1281 "Elevator.c"
1914 return;
1915}
1916}
1917#line 133 "Elevator.c"
1918void resetFloorButton(int floorID )
1919{
1920
1921 {
1922#line 139
1923 if (floorID == 0) {
1924#line 140
1925 floorButtons_0 = 0;
1926 } else {
1927#line 141
1928 if (floorID == 1) {
1929#line 142
1930 floorButtons_1 = 0;
1931 } else {
1932#line 143
1933 if (floorID == 2) {
1934#line 144
1935 floorButtons_2 = 0;
1936 } else {
1937#line 145
1938 if (floorID == 3) {
1939#line 146
1940 floorButtons_3 = 0;
1941 } else {
1942#line 147
1943 if (floorID == 4) {
1944#line 148
1945 floorButtons_4 = 0;
1946 } else {
1947
1948 }
1949 }
1950 }
1951 }
1952 }
1953#line 1310 "Elevator.c"
1954 return;
1955}
1956}
1957#line 141 "Elevator.c"
1958int getCurrentFloorID(void)
1959{ int retValue_acc ;
1960
1961 {
1962#line 1328 "Elevator.c"
1963 retValue_acc = currentFloorID;
1964#line 1330
1965 return (retValue_acc);
1966#line 1337
1967 return (retValue_acc);
1968}
1969}
1970#line 145 "Elevator.c"
1971int areDoorsOpen(void)
1972{ int retValue_acc ;
1973
1974 {
1975#line 1359 "Elevator.c"
1976 retValue_acc = doorState;
1977#line 1361
1978 return (retValue_acc);
1979#line 1368
1980 return (retValue_acc);
1981}
1982}
1983#line 149 "Elevator.c"
1984int buttonForFloorIsPressed(int floorID )
1985{ int retValue_acc ;
1986
1987 {
1988#line 155 "Elevator.c"
1989 if (floorID == 0) {
1990#line 1391
1991 retValue_acc = floorButtons_0;
1992#line 1393
1993 return (retValue_acc);
1994 } else {
1995#line 1395
1996 if (floorID == 1) {
1997#line 1398
1998 retValue_acc = floorButtons_1;
1999#line 1400
2000 return (retValue_acc);
2001 } else {
2002#line 1402
2003 if (floorID == 2) {
2004#line 1405
2005 retValue_acc = floorButtons_2;
2006#line 1407
2007 return (retValue_acc);
2008 } else {
2009#line 1409
2010 if (floorID == 3) {
2011#line 1412
2012 retValue_acc = floorButtons_3;
2013#line 1414
2014 return (retValue_acc);
2015 } else {
2016#line 1416
2017 if (floorID == 4) {
2018#line 1419
2019 retValue_acc = floorButtons_4;
2020#line 1421
2021 return (retValue_acc);
2022 } else {
2023#line 1425 "Elevator.c"
2024 retValue_acc = 0;
2025#line 1427
2026 return (retValue_acc);
2027 }
2028 }
2029 }
2030 }
2031 }
2032#line 1434 "Elevator.c"
2033 return (retValue_acc);
2034}
2035}
2036#line 158 "Elevator.c"
2037int getCurrentHeading(void)
2038{ int retValue_acc ;
2039
2040 {
2041#line 1456 "Elevator.c"
2042 retValue_acc = currentHeading;
2043#line 1458
2044 return (retValue_acc);
2045#line 1465
2046 return (retValue_acc);
2047}
2048}
2049#line 162 "Elevator.c"
2050int isEmpty(void)
2051{ int retValue_acc ;
2052
2053 {
2054#line 169 "Elevator.c"
2055 if (persons_0 == 1) {
2056#line 1488
2057 retValue_acc = 0;
2058#line 1490
2059 return (retValue_acc);
2060 } else {
2061#line 1492
2062 if (persons_1 == 1) {
2063#line 1495
2064 retValue_acc = 0;
2065#line 1497
2066 return (retValue_acc);
2067 } else {
2068#line 1499
2069 if (persons_2 == 1) {
2070#line 1502
2071 retValue_acc = 0;
2072#line 1504
2073 return (retValue_acc);
2074 } else {
2075#line 1506
2076 if (persons_3 == 1) {
2077#line 1509
2078 retValue_acc = 0;
2079#line 1511
2080 return (retValue_acc);
2081 } else {
2082#line 1513
2083 if (persons_4 == 1) {
2084#line 1516
2085 retValue_acc = 0;
2086#line 1518
2087 return (retValue_acc);
2088 } else {
2089#line 1520
2090 if (persons_5 == 1) {
2091#line 1523 "Elevator.c"
2092 retValue_acc = 0;
2093#line 1525
2094 return (retValue_acc);
2095 } else {
2096
2097 }
2098 }
2099 }
2100 }
2101 }
2102 }
2103#line 1530 "Elevator.c"
2104 retValue_acc = 1;
2105#line 1532
2106 return (retValue_acc);
2107#line 1539
2108 return (retValue_acc);
2109}
2110}
2111#line 173 "Elevator.c"
2112int anyStopRequested(void)
2113{ int retValue_acc ;
2114 int tmp ;
2115 int tmp___0 ;
2116 int tmp___1 ;
2117 int tmp___2 ;
2118 int tmp___3 ;
2119
2120 {
2121 {
2122#line 184
2123 tmp___3 = isFloorCalling(0);
2124 }
2125#line 184 "Elevator.c"
2126 if (tmp___3) {
2127#line 1562
2128 retValue_acc = 1;
2129#line 1564
2130 return (retValue_acc);
2131 } else {
2132#line 1566
2133 if (floorButtons_0) {
2134#line 1569
2135 retValue_acc = 1;
2136#line 1571
2137 return (retValue_acc);
2138 } else {
2139 {
2140#line 1573 "Elevator.c"
2141 tmp___2 = isFloorCalling(1);
2142 }
2143#line 1573
2144 if (tmp___2) {
2145#line 1576
2146 retValue_acc = 1;
2147#line 1578
2148 return (retValue_acc);
2149 } else {
2150#line 1580
2151 if (floorButtons_1) {
2152#line 1583
2153 retValue_acc = 1;
2154#line 1585
2155 return (retValue_acc);
2156 } else {
2157 {
2158#line 1587
2159 tmp___1 = isFloorCalling(2);
2160 }
2161#line 1587
2162 if (tmp___1) {
2163#line 1590
2164 retValue_acc = 1;
2165#line 1592
2166 return (retValue_acc);
2167 } else {
2168#line 1594
2169 if (floorButtons_2) {
2170#line 1597
2171 retValue_acc = 1;
2172#line 1599
2173 return (retValue_acc);
2174 } else {
2175 {
2176#line 1601
2177 tmp___0 = isFloorCalling(3);
2178 }
2179#line 1601
2180 if (tmp___0) {
2181#line 1604
2182 retValue_acc = 1;
2183#line 1606
2184 return (retValue_acc);
2185 } else {
2186#line 1608
2187 if (floorButtons_3) {
2188#line 1611
2189 retValue_acc = 1;
2190#line 1613
2191 return (retValue_acc);
2192 } else {
2193 {
2194#line 1615
2195 tmp = isFloorCalling(4);
2196 }
2197#line 1615
2198 if (tmp) {
2199#line 1618
2200 retValue_acc = 1;
2201#line 1620
2202 return (retValue_acc);
2203 } else {
2204#line 1622
2205 if (floorButtons_4) {
2206#line 1625
2207 retValue_acc = 1;
2208#line 1627
2209 return (retValue_acc);
2210 } else {
2211
2212 }
2213 }
2214 }
2215 }
2216 }
2217 }
2218 }
2219 }
2220 }
2221 }
2222#line 1632 "Elevator.c"
2223 retValue_acc = 0;
2224#line 1634
2225 return (retValue_acc);
2226#line 1641
2227 return (retValue_acc);
2228}
2229}
2230#line 187 "Elevator.c"
2231int isIdle(void)
2232{ int retValue_acc ;
2233 int tmp ;
2234
2235 {
2236 {
2237#line 1663 "Elevator.c"
2238 tmp = anyStopRequested();
2239#line 1663
2240 retValue_acc = tmp == 0;
2241 }
2242#line 1665
2243 return (retValue_acc);
2244#line 1672
2245 return (retValue_acc);
2246}
2247}
2248#line 191 "Elevator.c"
2249int stopRequestedInDirection(int dir , int respectFloorCalls , int respectInLiftCalls )
2250{ int retValue_acc ;
2251 int tmp ;
2252 int tmp___0 ;
2253 int tmp___1 ;
2254 int tmp___2 ;
2255 int tmp___3 ;
2256 int tmp___4 ;
2257 int tmp___5 ;
2258 int tmp___6 ;
2259 int tmp___7 ;
2260 int tmp___8 ;
2261 int tmp___9 ;
2262
2263 {
2264#line 242
2265 if (dir == 1) {
2266 {
2267#line 202
2268 tmp = isTopFloor(currentFloorID);
2269 }
2270#line 202 "Elevator.c"
2271 if (tmp) {
2272#line 1698 "Elevator.c"
2273 retValue_acc = 0;
2274#line 1700
2275 return (retValue_acc);
2276 } else {
2277
2278 }
2279#line 202
2280 if (currentFloorID < 0) {
2281#line 202
2282 if (respectFloorCalls) {
2283 {
2284#line 202 "Elevator.c"
2285 tmp___4 = isFloorCalling(0);
2286 }
2287#line 202 "Elevator.c"
2288 if (tmp___4) {
2289#line 1706 "Elevator.c"
2290 retValue_acc = 1;
2291#line 1708
2292 return (retValue_acc);
2293 } else {
2294 goto _L___16;
2295 }
2296 } else {
2297 goto _L___16;
2298 }
2299 } else {
2300 _L___16:
2301#line 1710
2302 if (currentFloorID < 0) {
2303#line 1710
2304 if (respectInLiftCalls) {
2305#line 1710
2306 if (floorButtons_0) {
2307#line 1713
2308 retValue_acc = 1;
2309#line 1715
2310 return (retValue_acc);
2311 } else {
2312 goto _L___14;
2313 }
2314 } else {
2315 goto _L___14;
2316 }
2317 } else {
2318 _L___14:
2319#line 1717
2320 if (currentFloorID < 1) {
2321#line 1717
2322 if (respectFloorCalls) {
2323 {
2324#line 1717
2325 tmp___3 = isFloorCalling(1);
2326 }
2327#line 1717
2328 if (tmp___3) {
2329#line 1720
2330 retValue_acc = 1;
2331#line 1722
2332 return (retValue_acc);
2333 } else {
2334 goto _L___12;
2335 }
2336 } else {
2337 goto _L___12;
2338 }
2339 } else {
2340 _L___12:
2341#line 1724
2342 if (currentFloorID < 1) {
2343#line 1724
2344 if (respectInLiftCalls) {
2345#line 1724
2346 if (floorButtons_1) {
2347#line 1727
2348 retValue_acc = 1;
2349#line 1729
2350 return (retValue_acc);
2351 } else {
2352 goto _L___10;
2353 }
2354 } else {
2355 goto _L___10;
2356 }
2357 } else {
2358 _L___10:
2359#line 1731
2360 if (currentFloorID < 2) {
2361#line 1731
2362 if (respectFloorCalls) {
2363 {
2364#line 1731
2365 tmp___2 = isFloorCalling(2);
2366 }
2367#line 1731
2368 if (tmp___2) {
2369#line 1734
2370 retValue_acc = 1;
2371#line 1736
2372 return (retValue_acc);
2373 } else {
2374 goto _L___8;
2375 }
2376 } else {
2377 goto _L___8;
2378 }
2379 } else {
2380 _L___8:
2381#line 1738
2382 if (currentFloorID < 2) {
2383#line 1738
2384 if (respectInLiftCalls) {
2385#line 1738
2386 if (floorButtons_2) {
2387#line 1741
2388 retValue_acc = 1;
2389#line 1743
2390 return (retValue_acc);
2391 } else {
2392 goto _L___6;
2393 }
2394 } else {
2395 goto _L___6;
2396 }
2397 } else {
2398 _L___6:
2399#line 1745
2400 if (currentFloorID < 3) {
2401#line 1745
2402 if (respectFloorCalls) {
2403 {
2404#line 1745
2405 tmp___1 = isFloorCalling(3);
2406 }
2407#line 1745
2408 if (tmp___1) {
2409#line 1748
2410 retValue_acc = 1;
2411#line 1750
2412 return (retValue_acc);
2413 } else {
2414 goto _L___4;
2415 }
2416 } else {
2417 goto _L___4;
2418 }
2419 } else {
2420 _L___4:
2421#line 1752
2422 if (currentFloorID < 3) {
2423#line 1752
2424 if (respectInLiftCalls) {
2425#line 1752
2426 if (floorButtons_3) {
2427#line 1755
2428 retValue_acc = 1;
2429#line 1757
2430 return (retValue_acc);
2431 } else {
2432 goto _L___2;
2433 }
2434 } else {
2435 goto _L___2;
2436 }
2437 } else {
2438 _L___2:
2439#line 1759
2440 if (currentFloorID < 4) {
2441#line 1759
2442 if (respectFloorCalls) {
2443 {
2444#line 1759
2445 tmp___0 = isFloorCalling(4);
2446 }
2447#line 1759
2448 if (tmp___0) {
2449#line 1762
2450 retValue_acc = 1;
2451#line 1764
2452 return (retValue_acc);
2453 } else {
2454 goto _L___0;
2455 }
2456 } else {
2457 goto _L___0;
2458 }
2459 } else {
2460 _L___0:
2461#line 1766
2462 if (currentFloorID < 4) {
2463#line 1766
2464 if (respectInLiftCalls) {
2465#line 1766
2466 if (floorButtons_4) {
2467#line 1769
2468 retValue_acc = 1;
2469#line 1771
2470 return (retValue_acc);
2471 } else {
2472#line 1775
2473 retValue_acc = 0;
2474#line 1777
2475 return (retValue_acc);
2476 }
2477 } else {
2478#line 1775
2479 retValue_acc = 0;
2480#line 1777
2481 return (retValue_acc);
2482 }
2483 } else {
2484#line 1775 "Elevator.c"
2485 retValue_acc = 0;
2486#line 1777
2487 return (retValue_acc);
2488 }
2489 }
2490 }
2491 }
2492 }
2493 }
2494 }
2495 }
2496 }
2497 }
2498 } else {
2499#line 227 "Elevator.c"
2500 if (currentFloorID == 0) {
2501#line 1785 "Elevator.c"
2502 retValue_acc = 0;
2503#line 1787
2504 return (retValue_acc);
2505 } else {
2506
2507 }
2508#line 227
2509 if (currentFloorID > 0) {
2510#line 227
2511 if (respectFloorCalls) {
2512 {
2513#line 227 "Elevator.c"
2514 tmp___9 = isFloorCalling(0);
2515 }
2516#line 227 "Elevator.c"
2517 if (tmp___9) {
2518#line 1793 "Elevator.c"
2519 retValue_acc = 1;
2520#line 1795
2521 return (retValue_acc);
2522 } else {
2523 goto _L___34;
2524 }
2525 } else {
2526 goto _L___34;
2527 }
2528 } else {
2529 _L___34:
2530#line 1797
2531 if (currentFloorID > 0) {
2532#line 1797
2533 if (respectInLiftCalls) {
2534#line 1797
2535 if (floorButtons_0) {
2536#line 1800
2537 retValue_acc = 1;
2538#line 1802
2539 return (retValue_acc);
2540 } else {
2541 goto _L___32;
2542 }
2543 } else {
2544 goto _L___32;
2545 }
2546 } else {
2547 _L___32:
2548#line 1804
2549 if (currentFloorID > 1) {
2550#line 1804
2551 if (respectFloorCalls) {
2552 {
2553#line 1804
2554 tmp___8 = isFloorCalling(1);
2555 }
2556#line 1804
2557 if (tmp___8) {
2558#line 1807
2559 retValue_acc = 1;
2560#line 1809
2561 return (retValue_acc);
2562 } else {
2563 goto _L___30;
2564 }
2565 } else {
2566 goto _L___30;
2567 }
2568 } else {
2569 _L___30:
2570#line 1811
2571 if (currentFloorID > 1) {
2572#line 1811
2573 if (respectInLiftCalls) {
2574#line 1811
2575 if (floorButtons_1) {
2576#line 1814
2577 retValue_acc = 1;
2578#line 1816
2579 return (retValue_acc);
2580 } else {
2581 goto _L___28;
2582 }
2583 } else {
2584 goto _L___28;
2585 }
2586 } else {
2587 _L___28:
2588#line 1818
2589 if (currentFloorID > 2) {
2590#line 1818
2591 if (respectFloorCalls) {
2592 {
2593#line 1818
2594 tmp___7 = isFloorCalling(2);
2595 }
2596#line 1818
2597 if (tmp___7) {
2598#line 1821
2599 retValue_acc = 1;
2600#line 1823
2601 return (retValue_acc);
2602 } else {
2603 goto _L___26;
2604 }
2605 } else {
2606 goto _L___26;
2607 }
2608 } else {
2609 _L___26:
2610#line 1825
2611 if (currentFloorID > 2) {
2612#line 1825
2613 if (respectInLiftCalls) {
2614#line 1825
2615 if (floorButtons_2) {
2616#line 1828
2617 retValue_acc = 1;
2618#line 1830
2619 return (retValue_acc);
2620 } else {
2621 goto _L___24;
2622 }
2623 } else {
2624 goto _L___24;
2625 }
2626 } else {
2627 _L___24:
2628#line 1832
2629 if (currentFloorID > 3) {
2630#line 1832
2631 if (respectFloorCalls) {
2632 {
2633#line 1832
2634 tmp___6 = isFloorCalling(3);
2635 }
2636#line 1832
2637 if (tmp___6) {
2638#line 1835
2639 retValue_acc = 1;
2640#line 1837
2641 return (retValue_acc);
2642 } else {
2643 goto _L___22;
2644 }
2645 } else {
2646 goto _L___22;
2647 }
2648 } else {
2649 _L___22:
2650#line 1839
2651 if (currentFloorID > 3) {
2652#line 1839
2653 if (respectInLiftCalls) {
2654#line 1839
2655 if (floorButtons_3) {
2656#line 1842
2657 retValue_acc = 1;
2658#line 1844
2659 return (retValue_acc);
2660 } else {
2661 goto _L___20;
2662 }
2663 } else {
2664 goto _L___20;
2665 }
2666 } else {
2667 _L___20:
2668#line 1846
2669 if (currentFloorID > 4) {
2670#line 1846
2671 if (respectFloorCalls) {
2672 {
2673#line 1846
2674 tmp___5 = isFloorCalling(4);
2675 }
2676#line 1846
2677 if (tmp___5) {
2678#line 1849
2679 retValue_acc = 1;
2680#line 1851
2681 return (retValue_acc);
2682 } else {
2683 goto _L___18;
2684 }
2685 } else {
2686 goto _L___18;
2687 }
2688 } else {
2689 _L___18:
2690#line 1853
2691 if (currentFloorID > 4) {
2692#line 1853
2693 if (respectInLiftCalls) {
2694#line 1853
2695 if (floorButtons_4) {
2696#line 1856
2697 retValue_acc = 1;
2698#line 1858
2699 return (retValue_acc);
2700 } else {
2701#line 1862
2702 retValue_acc = 0;
2703#line 1864
2704 return (retValue_acc);
2705 }
2706 } else {
2707#line 1862
2708 retValue_acc = 0;
2709#line 1864
2710 return (retValue_acc);
2711 }
2712 } else {
2713#line 1862 "Elevator.c"
2714 retValue_acc = 0;
2715#line 1864
2716 return (retValue_acc);
2717 }
2718 }
2719 }
2720 }
2721 }
2722 }
2723 }
2724 }
2725 }
2726 }
2727 }
2728#line 1871 "Elevator.c"
2729 return (retValue_acc);
2730}
2731}
2732#line 245 "Elevator.c"
2733int isAnyLiftButtonPressed(void)
2734{ int retValue_acc ;
2735
2736 {
2737#line 251 "Elevator.c"
2738 if (floorButtons_0) {
2739#line 1894
2740 retValue_acc = 1;
2741#line 1896
2742 return (retValue_acc);
2743 } else {
2744#line 1898
2745 if (floorButtons_1) {
2746#line 1901
2747 retValue_acc = 1;
2748#line 1903
2749 return (retValue_acc);
2750 } else {
2751#line 1905
2752 if (floorButtons_2) {
2753#line 1908
2754 retValue_acc = 1;
2755#line 1910
2756 return (retValue_acc);
2757 } else {
2758#line 1912
2759 if (floorButtons_3) {
2760#line 1915
2761 retValue_acc = 1;
2762#line 1917
2763 return (retValue_acc);
2764 } else {
2765#line 1919
2766 if (floorButtons_4) {
2767#line 1922
2768 retValue_acc = 1;
2769#line 1924
2770 return (retValue_acc);
2771 } else {
2772#line 1928 "Elevator.c"
2773 retValue_acc = 0;
2774#line 1930
2775 return (retValue_acc);
2776 }
2777 }
2778 }
2779 }
2780 }
2781#line 1937 "Elevator.c"
2782 return (retValue_acc);
2783}
2784}
2785#line 254 "Elevator.c"
2786void continueInDirection(int dir )
2787{ int tmp ;
2788
2789 {
2790#line 255
2791 currentHeading = dir;
2792#line 256
2793 if (currentHeading == 1) {
2794 {
2795#line 261
2796 tmp = isTopFloor(currentFloorID);
2797 }
2798#line 261
2799 if (tmp) {
2800#line 259
2801 currentHeading = 0;
2802 } else {
2803
2804 }
2805 } else {
2806#line 266
2807 if (currentFloorID == 0) {
2808#line 264
2809 currentHeading = 1;
2810 } else {
2811
2812 }
2813 }
2814#line 267
2815 if (currentHeading == 1) {
2816#line 268
2817 currentFloorID = currentFloorID + 1;
2818 } else {
2819#line 270
2820 currentFloorID = currentFloorID - 1;
2821 }
2822#line 1983 "Elevator.c"
2823 return;
2824}
2825}
2826#line 274 "Elevator.c"
2827int stopRequestedAtCurrentFloor(void)
2828{ int retValue_acc ;
2829 int tmp ;
2830 int tmp___0 ;
2831
2832 {
2833 {
2834#line 281
2835 tmp___0 = isFloorCalling(currentFloorID);
2836 }
2837#line 281 "Elevator.c"
2838 if (tmp___0) {
2839#line 2004
2840 retValue_acc = 1;
2841#line 2006
2842 return (retValue_acc);
2843 } else {
2844 {
2845#line 2008 "Elevator.c"
2846 tmp = buttonForFloorIsPressed(currentFloorID);
2847 }
2848#line 2008
2849 if (tmp) {
2850#line 2013
2851 retValue_acc = 1;
2852#line 2015
2853 return (retValue_acc);
2854 } else {
2855#line 2021
2856 retValue_acc = 0;
2857#line 2023
2858 return (retValue_acc);
2859 }
2860 }
2861#line 2030 "Elevator.c"
2862 return (retValue_acc);
2863}
2864}
2865#line 284 "Elevator.c"
2866int getReverseHeading(int ofHeading )
2867{ int retValue_acc ;
2868
2869 {
2870#line 287 "Elevator.c"
2871 if (ofHeading == 0) {
2872#line 2055
2873 retValue_acc = 1;
2874#line 2057
2875 return (retValue_acc);
2876 } else {
2877#line 2061 "Elevator.c"
2878 retValue_acc = 0;
2879#line 2063
2880 return (retValue_acc);
2881 }
2882#line 2070 "Elevator.c"
2883 return (retValue_acc);
2884}
2885}
2886#line 291 "Elevator.c"
2887void processWaitingOnFloor(int floorID )
2888{ int tmp ;
2889 int tmp___0 ;
2890 int tmp___1 ;
2891 int tmp___2 ;
2892 int tmp___3 ;
2893 int tmp___4 ;
2894 int tmp___5 ;
2895 int tmp___6 ;
2896 int tmp___7 ;
2897 int tmp___8 ;
2898 int tmp___9 ;
2899 int tmp___10 ;
2900
2901 {
2902 {
2903#line 297
2904 tmp___0 = isPersonOnFloor(0, floorID);
2905 }
2906#line 297
2907 if (tmp___0) {
2908 {
2909#line 293
2910 removePersonFromFloor(0, floorID);
2911#line 294
2912 tmp = getDestination(0);
2913#line 294
2914 pressInLiftFloorButton(tmp);
2915#line 295
2916 enterElevator(0);
2917 }
2918 } else {
2919
2920 }
2921 {
2922#line 297
2923 tmp___2 = isPersonOnFloor(1, floorID);
2924 }
2925#line 297
2926 if (tmp___2) {
2927 {
2928#line 298
2929 removePersonFromFloor(1, floorID);
2930#line 299
2931 tmp___1 = getDestination(1);
2932#line 299
2933 pressInLiftFloorButton(tmp___1);
2934#line 300
2935 enterElevator(1);
2936 }
2937 } else {
2938
2939 }
2940 {
2941#line 302
2942 tmp___4 = isPersonOnFloor(2, floorID);
2943 }
2944#line 302
2945 if (tmp___4) {
2946 {
2947#line 303
2948 removePersonFromFloor(2, floorID);
2949#line 304
2950 tmp___3 = getDestination(2);
2951#line 304
2952 pressInLiftFloorButton(tmp___3);
2953#line 305
2954 enterElevator(2);
2955 }
2956 } else {
2957
2958 }
2959 {
2960#line 307
2961 tmp___6 = isPersonOnFloor(3, floorID);
2962 }
2963#line 307
2964 if (tmp___6) {
2965 {
2966#line 308
2967 removePersonFromFloor(3, floorID);
2968#line 309
2969 tmp___5 = getDestination(3);
2970#line 309
2971 pressInLiftFloorButton(tmp___5);
2972#line 310
2973 enterElevator(3);
2974 }
2975 } else {
2976
2977 }
2978 {
2979#line 312
2980 tmp___8 = isPersonOnFloor(4, floorID);
2981 }
2982#line 312
2983 if (tmp___8) {
2984 {
2985#line 313
2986 removePersonFromFloor(4, floorID);
2987#line 314
2988 tmp___7 = getDestination(4);
2989#line 314
2990 pressInLiftFloorButton(tmp___7);
2991#line 315
2992 enterElevator(4);
2993 }
2994 } else {
2995
2996 }
2997 {
2998#line 317
2999 tmp___10 = isPersonOnFloor(5, floorID);
3000 }
3001#line 317
3002 if (tmp___10) {
3003 {
3004#line 318
3005 removePersonFromFloor(5, floorID);
3006#line 319
3007 tmp___9 = getDestination(5);
3008#line 319
3009 pressInLiftFloorButton(tmp___9);
3010#line 320
3011 enterElevator(5);
3012 }
3013 } else {
3014
3015 }
3016 {
3017#line 322
3018 resetCallOnFloor(floorID);
3019 }
3020#line 2148 "Elevator.c"
3021 return;
3022}
3023}
3024#line 2150
3025void __utac_acc__Specification9_spec__3(void) ;
3026#line 326 "Elevator.c"
3027void timeShift(void)
3028{ int tmp ;
3029 int tmp___0 ;
3030 int tmp___1 ;
3031 int tmp___2 ;
3032 int tmp___3 ;
3033 int tmp___4 ;
3034 int tmp___5 ;
3035 int tmp___6 ;
3036 int tmp___7 ;
3037 int tmp___8 ;
3038 int tmp___9 ;
3039
3040 {
3041 {
3042#line 359
3043 tmp___9 = stopRequestedAtCurrentFloor();
3044 }
3045#line 359
3046 if (tmp___9) {
3047#line 331
3048 doorState = 1;
3049#line 333
3050 if (persons_0) {
3051 {
3052#line 333
3053 tmp = getDestination(0);
3054 }
3055#line 333
3056 if (tmp == currentFloorID) {
3057 {
3058#line 334
3059 leaveElevator(0);
3060 }
3061 } else {
3062
3063 }
3064 } else {
3065
3066 }
3067#line 334
3068 if (persons_1) {
3069 {
3070#line 334
3071 tmp___0 = getDestination(1);
3072 }
3073#line 334
3074 if (tmp___0 == currentFloorID) {
3075 {
3076#line 335
3077 leaveElevator(1);
3078 }
3079 } else {
3080
3081 }
3082 } else {
3083
3084 }
3085#line 335
3086 if (persons_2) {
3087 {
3088#line 335
3089 tmp___1 = getDestination(2);
3090 }
3091#line 335
3092 if (tmp___1 == currentFloorID) {
3093 {
3094#line 336
3095 leaveElevator(2);
3096 }
3097 } else {
3098
3099 }
3100 } else {
3101
3102 }
3103#line 336
3104 if (persons_3) {
3105 {
3106#line 336
3107 tmp___2 = getDestination(3);
3108 }
3109#line 336
3110 if (tmp___2 == currentFloorID) {
3111 {
3112#line 337
3113 leaveElevator(3);
3114 }
3115 } else {
3116
3117 }
3118 } else {
3119
3120 }
3121#line 337
3122 if (persons_4) {
3123 {
3124#line 337
3125 tmp___3 = getDestination(4);
3126 }
3127#line 337
3128 if (tmp___3 == currentFloorID) {
3129 {
3130#line 338
3131 leaveElevator(4);
3132 }
3133 } else {
3134
3135 }
3136 } else {
3137
3138 }
3139#line 338
3140 if (persons_5) {
3141 {
3142#line 338
3143 tmp___4 = getDestination(5);
3144 }
3145#line 338
3146 if (tmp___4 == currentFloorID) {
3147 {
3148#line 339
3149 leaveElevator(5);
3150 }
3151 } else {
3152
3153 }
3154 } else {
3155
3156 }
3157 {
3158#line 339
3159 processWaitingOnFloor(currentFloorID);
3160#line 340
3161 resetFloorButton(currentFloorID);
3162 }
3163 } else {
3164#line 346
3165 if (doorState == 1) {
3166#line 343
3167 doorState = 0;
3168 } else {
3169
3170 }
3171 {
3172#line 346
3173 tmp___8 = stopRequestedInDirection(currentHeading, 1, 1);
3174 }
3175#line 346
3176 if (tmp___8) {
3177 {
3178#line 349
3179 continueInDirection(currentHeading);
3180 }
3181 } else {
3182 {
3183#line 350
3184 tmp___6 = getReverseHeading(currentHeading);
3185#line 350
3186 tmp___7 = stopRequestedInDirection(tmp___6, 1, 1);
3187 }
3188#line 350
3189 if (tmp___7) {
3190 {
3191#line 353
3192 tmp___5 = getReverseHeading(currentHeading);
3193#line 353
3194 continueInDirection(tmp___5);
3195 }
3196 } else {
3197 {
3198#line 357
3199 continueInDirection(currentHeading);
3200 }
3201 }
3202 }
3203 }
3204 {
3205#line 2213 "Elevator.c"
3206 __utac_acc__Specification9_spec__3();
3207 }
3208#line 2219
3209 return;
3210}
3211}
3212#line 362 "Elevator.c"
3213void printState(void)
3214{ int tmp ;
3215 int tmp___0 ;
3216 int tmp___1 ;
3217 int tmp___2 ;
3218 int tmp___3 ;
3219 char const * __restrict __cil_tmp6 ;
3220 char const * __restrict __cil_tmp7 ;
3221 char const * __restrict __cil_tmp8 ;
3222 char const * __restrict __cil_tmp9 ;
3223 char const * __restrict __cil_tmp10 ;
3224 char const * __restrict __cil_tmp11 ;
3225 char const * __restrict __cil_tmp12 ;
3226 char const * __restrict __cil_tmp13 ;
3227 char const * __restrict __cil_tmp14 ;
3228 char const * __restrict __cil_tmp15 ;
3229 char const * __restrict __cil_tmp16 ;
3230 char const * __restrict __cil_tmp17 ;
3231 char const * __restrict __cil_tmp18 ;
3232 char const * __restrict __cil_tmp19 ;
3233 char const * __restrict __cil_tmp20 ;
3234 char const * __restrict __cil_tmp21 ;
3235 char const * __restrict __cil_tmp22 ;
3236 char const * __restrict __cil_tmp23 ;
3237 char const * __restrict __cil_tmp24 ;
3238 char const * __restrict __cil_tmp25 ;
3239 char const * __restrict __cil_tmp26 ;
3240
3241 {
3242 {
3243#line 363
3244 __cil_tmp6 = (char const * __restrict )"Elevator ";
3245#line 363
3246 printf(__cil_tmp6);
3247 }
3248#line 364
3249 if (doorState) {
3250 {
3251#line 365
3252 __cil_tmp7 = (char const * __restrict )"[_]";
3253#line 365
3254 printf(__cil_tmp7);
3255 }
3256 } else {
3257 {
3258#line 366
3259 __cil_tmp8 = (char const * __restrict )"[] ";
3260#line 366
3261 printf(__cil_tmp8);
3262 }
3263 }
3264 {
3265#line 366
3266 __cil_tmp9 = (char const * __restrict )" at ";
3267#line 366
3268 printf(__cil_tmp9);
3269#line 367
3270 __cil_tmp10 = (char const * __restrict )"%i";
3271#line 367
3272 printf(__cil_tmp10, currentFloorID);
3273#line 368
3274 __cil_tmp11 = (char const * __restrict )" heading ";
3275#line 368
3276 printf(__cil_tmp11);
3277 }
3278#line 369
3279 if (currentHeading) {
3280 {
3281#line 370
3282 __cil_tmp12 = (char const * __restrict )"up";
3283#line 370
3284 printf(__cil_tmp12);
3285 }
3286 } else {
3287 {
3288#line 371
3289 __cil_tmp13 = (char const * __restrict )"down";
3290#line 371
3291 printf(__cil_tmp13);
3292 }
3293 }
3294 {
3295#line 371
3296 __cil_tmp14 = (char const * __restrict )" IL_p:";
3297#line 371
3298 printf(__cil_tmp14);
3299 }
3300#line 372
3301 if (floorButtons_0) {
3302 {
3303#line 373
3304 __cil_tmp15 = (char const * __restrict )" %i";
3305#line 373
3306 printf(__cil_tmp15, 0);
3307 }
3308 } else {
3309
3310 }
3311#line 373
3312 if (floorButtons_1) {
3313 {
3314#line 374
3315 __cil_tmp16 = (char const * __restrict )" %i";
3316#line 374
3317 printf(__cil_tmp16, 1);
3318 }
3319 } else {
3320
3321 }
3322#line 374
3323 if (floorButtons_2) {
3324 {
3325#line 375
3326 __cil_tmp17 = (char const * __restrict )" %i";
3327#line 375
3328 printf(__cil_tmp17, 2);
3329 }
3330 } else {
3331
3332 }
3333#line 375
3334 if (floorButtons_3) {
3335 {
3336#line 376
3337 __cil_tmp18 = (char const * __restrict )" %i";
3338#line 376
3339 printf(__cil_tmp18, 3);
3340 }
3341 } else {
3342
3343 }
3344#line 376
3345 if (floorButtons_4) {
3346 {
3347#line 377
3348 __cil_tmp19 = (char const * __restrict )" %i";
3349#line 377
3350 printf(__cil_tmp19, 4);
3351 }
3352 } else {
3353
3354 }
3355 {
3356#line 377
3357 __cil_tmp20 = (char const * __restrict )" F_p:";
3358#line 377
3359 printf(__cil_tmp20);
3360#line 378
3361 tmp = isFloorCalling(0);
3362 }
3363#line 378
3364 if (tmp) {
3365 {
3366#line 379
3367 __cil_tmp21 = (char const * __restrict )" %i";
3368#line 379
3369 printf(__cil_tmp21, 0);
3370 }
3371 } else {
3372
3373 }
3374 {
3375#line 379
3376 tmp___0 = isFloorCalling(1);
3377 }
3378#line 379
3379 if (tmp___0) {
3380 {
3381#line 380
3382 __cil_tmp22 = (char const * __restrict )" %i";
3383#line 380
3384 printf(__cil_tmp22, 1);
3385 }
3386 } else {
3387
3388 }
3389 {
3390#line 380
3391 tmp___1 = isFloorCalling(2);
3392 }
3393#line 380
3394 if (tmp___1) {
3395 {
3396#line 381
3397 __cil_tmp23 = (char const * __restrict )" %i";
3398#line 381
3399 printf(__cil_tmp23, 2);
3400 }
3401 } else {
3402
3403 }
3404 {
3405#line 381
3406 tmp___2 = isFloorCalling(3);
3407 }
3408#line 381
3409 if (tmp___2) {
3410 {
3411#line 382
3412 __cil_tmp24 = (char const * __restrict )" %i";
3413#line 382
3414 printf(__cil_tmp24, 3);
3415 }
3416 } else {
3417
3418 }
3419 {
3420#line 382
3421 tmp___3 = isFloorCalling(4);
3422 }
3423#line 382
3424 if (tmp___3) {
3425 {
3426#line 383
3427 __cil_tmp25 = (char const * __restrict )" %i";
3428#line 383
3429 printf(__cil_tmp25, 4);
3430 }
3431 } else {
3432
3433 }
3434 {
3435#line 383
3436 __cil_tmp26 = (char const * __restrict )"\n";
3437#line 383
3438 printf(__cil_tmp26);
3439 }
3440#line 2289 "Elevator.c"
3441 return;
3442}
3443}
3444#line 387 "Elevator.c"
3445int existInLiftCallsInDirection(int d )
3446{ int retValue_acc ;
3447 int i ;
3448 int i___0 ;
3449
3450 {
3451#line 408
3452 if (d == 1) {
3453#line 389 "Elevator.c"
3454 i = 0;
3455#line 390
3456 i = currentFloorID + 1;
3457 {
3458#line 390
3459 while (1) {
3460 while_2_continue: ;
3461#line 390
3462 if (i < 5) {
3463
3464 } else {
3465 goto while_2_break;
3466 }
3467#line 396
3468 if (i == 0) {
3469#line 396 "Elevator.c"
3470 if (floorButtons_0) {
3471#line 2317
3472 retValue_acc = 1;
3473#line 2319
3474 return (retValue_acc);
3475 } else {
3476 goto _L___2;
3477 }
3478 } else {
3479 _L___2:
3480#line 2321
3481 if (i == 1) {
3482#line 2321
3483 if (floorButtons_1) {
3484#line 2324
3485 retValue_acc = 1;
3486#line 2326
3487 return (retValue_acc);
3488 } else {
3489 goto _L___1;
3490 }
3491 } else {
3492 _L___1:
3493#line 2328
3494 if (i == 2) {
3495#line 2328
3496 if (floorButtons_2) {
3497#line 2331
3498 retValue_acc = 1;
3499#line 2333
3500 return (retValue_acc);
3501 } else {
3502 goto _L___0;
3503 }
3504 } else {
3505 _L___0:
3506#line 2335
3507 if (i == 3) {
3508#line 2335
3509 if (floorButtons_3) {
3510#line 2338
3511 retValue_acc = 1;
3512#line 2340
3513 return (retValue_acc);
3514 } else {
3515 goto _L;
3516 }
3517 } else {
3518 _L:
3519#line 2342
3520 if (i == 4) {
3521#line 2342
3522 if (floorButtons_4) {
3523#line 2345 "Elevator.c"
3524 retValue_acc = 1;
3525#line 2347
3526 return (retValue_acc);
3527 } else {
3528
3529 }
3530 } else {
3531
3532 }
3533 }
3534 }
3535 }
3536 }
3537#line 390
3538 i = i + 1;
3539 }
3540 while_2_break: ;
3541 }
3542 } else {
3543#line 2349 "Elevator.c"
3544 if (d == 0) {
3545#line 398
3546 i___0 = 0;
3547#line 399
3548 i___0 = currentFloorID - 1;
3549 {
3550#line 399
3551 while (1) {
3552 while_3_continue: ;
3553#line 399
3554 if (i___0 >= 0) {
3555
3556 } else {
3557 goto while_3_break;
3558 }
3559#line 399
3560 i___0 = currentFloorID + 1;
3561 {
3562#line 399
3563 while (1) {
3564 while_4_continue: ;
3565#line 399
3566 if (i___0 < 5) {
3567
3568 } else {
3569 goto while_4_break;
3570 }
3571#line 406
3572 if (i___0 == 0) {
3573#line 406 "Elevator.c"
3574 if (floorButtons_0) {
3575#line 2361
3576 retValue_acc = 1;
3577#line 2363
3578 return (retValue_acc);
3579 } else {
3580 goto _L___6;
3581 }
3582 } else {
3583 _L___6:
3584#line 2365
3585 if (i___0 == 1) {
3586#line 2365
3587 if (floorButtons_1) {
3588#line 2368
3589 retValue_acc = 1;
3590#line 2370
3591 return (retValue_acc);
3592 } else {
3593 goto _L___5;
3594 }
3595 } else {
3596 _L___5:
3597#line 2372
3598 if (i___0 == 2) {
3599#line 2372
3600 if (floorButtons_2) {
3601#line 2375
3602 retValue_acc = 1;
3603#line 2377
3604 return (retValue_acc);
3605 } else {
3606 goto _L___4;
3607 }
3608 } else {
3609 _L___4:
3610#line 2379
3611 if (i___0 == 3) {
3612#line 2379
3613 if (floorButtons_3) {
3614#line 2382
3615 retValue_acc = 1;
3616#line 2384
3617 return (retValue_acc);
3618 } else {
3619 goto _L___3;
3620 }
3621 } else {
3622 _L___3:
3623#line 2386
3624 if (i___0 == 4) {
3625#line 2386
3626 if (floorButtons_4) {
3627#line 2389 "Elevator.c"
3628 retValue_acc = 1;
3629#line 2391
3630 return (retValue_acc);
3631 } else {
3632
3633 }
3634 } else {
3635
3636 }
3637 }
3638 }
3639 }
3640 }
3641#line 399
3642 i___0 = i___0 + 1;
3643 }
3644 while_4_break: ;
3645 }
3646#line 399
3647 i___0 = i___0 - 1;
3648 }
3649 while_3_break: ;
3650 }
3651 } else {
3652
3653 }
3654 }
3655#line 2396 "Elevator.c"
3656 retValue_acc = 0;
3657#line 2398
3658 return (retValue_acc);
3659#line 2405
3660 return (retValue_acc);
3661}
3662}
3663#line 1 "libacc.o"
3664#pragma merger(0,"libacc.i","")
3665#line 73 "/usr/include/assert.h"
3666extern __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const *__assertion ,
3667 char const *__file ,
3668 unsigned int __line ,
3669 char const *__function ) ;
3670#line 471 "/usr/include/stdlib.h"
3671extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
3672#line 488
3673extern __attribute__((__nothrow__)) void free(void *__ptr ) ;
3674#line 32 "libacc.c"
3675void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int ,
3676 int ) ,
3677 int val )
3678{ struct __UTAC__EXCEPTION *excep ;
3679 struct __UTAC__CFLOW_FUNC *cf ;
3680 void *tmp ;
3681 unsigned long __cil_tmp7 ;
3682 unsigned long __cil_tmp8 ;
3683 unsigned long __cil_tmp9 ;
3684 unsigned long __cil_tmp10 ;
3685 unsigned long __cil_tmp11 ;
3686 unsigned long __cil_tmp12 ;
3687 unsigned long __cil_tmp13 ;
3688 unsigned long __cil_tmp14 ;
3689 int (**mem_15)(int , int ) ;
3690 int *mem_16 ;
3691 struct __UTAC__CFLOW_FUNC **mem_17 ;
3692 struct __UTAC__CFLOW_FUNC **mem_18 ;
3693 struct __UTAC__CFLOW_FUNC **mem_19 ;
3694
3695 {
3696 {
3697#line 33
3698 excep = (struct __UTAC__EXCEPTION *)exception;
3699#line 34
3700 tmp = malloc(24UL);
3701#line 34
3702 cf = (struct __UTAC__CFLOW_FUNC *)tmp;
3703#line 36
3704 mem_15 = (int (**)(int , int ))cf;
3705#line 36
3706 *mem_15 = cflow_func;
3707#line 37
3708 __cil_tmp7 = (unsigned long )cf;
3709#line 37
3710 __cil_tmp8 = __cil_tmp7 + 8;
3711#line 37
3712 mem_16 = (int *)__cil_tmp8;
3713#line 37
3714 *mem_16 = val;
3715#line 38
3716 __cil_tmp9 = (unsigned long )cf;
3717#line 38
3718 __cil_tmp10 = __cil_tmp9 + 16;
3719#line 38
3720 __cil_tmp11 = (unsigned long )excep;
3721#line 38
3722 __cil_tmp12 = __cil_tmp11 + 24;
3723#line 38
3724 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
3725#line 38
3726 mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
3727#line 38
3728 *mem_17 = *mem_18;
3729#line 39
3730 __cil_tmp13 = (unsigned long )excep;
3731#line 39
3732 __cil_tmp14 = __cil_tmp13 + 24;
3733#line 39
3734 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
3735#line 39
3736 *mem_19 = cf;
3737 }
3738#line 654 "libacc.c"
3739 return;
3740}
3741}
3742#line 44 "libacc.c"
3743void __utac__exception__cf_handler_free(void *exception )
3744{ struct __UTAC__EXCEPTION *excep ;
3745 struct __UTAC__CFLOW_FUNC *cf ;
3746 struct __UTAC__CFLOW_FUNC *tmp ;
3747 unsigned long __cil_tmp5 ;
3748 unsigned long __cil_tmp6 ;
3749 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
3750 unsigned long __cil_tmp8 ;
3751 unsigned long __cil_tmp9 ;
3752 unsigned long __cil_tmp10 ;
3753 unsigned long __cil_tmp11 ;
3754 void *__cil_tmp12 ;
3755 unsigned long __cil_tmp13 ;
3756 unsigned long __cil_tmp14 ;
3757 struct __UTAC__CFLOW_FUNC **mem_15 ;
3758 struct __UTAC__CFLOW_FUNC **mem_16 ;
3759 struct __UTAC__CFLOW_FUNC **mem_17 ;
3760
3761 {
3762#line 45
3763 excep = (struct __UTAC__EXCEPTION *)exception;
3764#line 46
3765 __cil_tmp5 = (unsigned long )excep;
3766#line 46
3767 __cil_tmp6 = __cil_tmp5 + 24;
3768#line 46
3769 mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
3770#line 46
3771 cf = *mem_15;
3772 {
3773#line 49
3774 while (1) {
3775 while_5_continue: ;
3776 {
3777#line 49
3778 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
3779#line 49
3780 __cil_tmp8 = (unsigned long )__cil_tmp7;
3781#line 49
3782 __cil_tmp9 = (unsigned long )cf;
3783#line 49
3784 if (__cil_tmp9 != __cil_tmp8) {
3785
3786 } else {
3787 goto while_5_break;
3788 }
3789 }
3790 {
3791#line 50
3792 tmp = cf;
3793#line 51
3794 __cil_tmp10 = (unsigned long )cf;
3795#line 51
3796 __cil_tmp11 = __cil_tmp10 + 16;
3797#line 51
3798 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
3799#line 51
3800 cf = *mem_16;
3801#line 52
3802 __cil_tmp12 = (void *)tmp;
3803#line 52
3804 free(__cil_tmp12);
3805 }
3806 }
3807 while_5_break: ;
3808 }
3809#line 55
3810 __cil_tmp13 = (unsigned long )excep;
3811#line 55
3812 __cil_tmp14 = __cil_tmp13 + 24;
3813#line 55
3814 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
3815#line 55
3816 *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
3817#line 694 "libacc.c"
3818 return;
3819}
3820}
3821#line 59 "libacc.c"
3822void __utac__exception__cf_handler_reset(void *exception )
3823{ struct __UTAC__EXCEPTION *excep ;
3824 struct __UTAC__CFLOW_FUNC *cf ;
3825 unsigned long __cil_tmp5 ;
3826 unsigned long __cil_tmp6 ;
3827 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
3828 unsigned long __cil_tmp8 ;
3829 unsigned long __cil_tmp9 ;
3830 int (*__cil_tmp10)(int , int ) ;
3831 unsigned long __cil_tmp11 ;
3832 unsigned long __cil_tmp12 ;
3833 int __cil_tmp13 ;
3834 unsigned long __cil_tmp14 ;
3835 unsigned long __cil_tmp15 ;
3836 struct __UTAC__CFLOW_FUNC **mem_16 ;
3837 int (**mem_17)(int , int ) ;
3838 int *mem_18 ;
3839 struct __UTAC__CFLOW_FUNC **mem_19 ;
3840
3841 {
3842#line 60
3843 excep = (struct __UTAC__EXCEPTION *)exception;
3844#line 61
3845 __cil_tmp5 = (unsigned long )excep;
3846#line 61
3847 __cil_tmp6 = __cil_tmp5 + 24;
3848#line 61
3849 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
3850#line 61
3851 cf = *mem_16;
3852 {
3853#line 64
3854 while (1) {
3855 while_6_continue: ;
3856 {
3857#line 64
3858 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
3859#line 64
3860 __cil_tmp8 = (unsigned long )__cil_tmp7;
3861#line 64
3862 __cil_tmp9 = (unsigned long )cf;
3863#line 64
3864 if (__cil_tmp9 != __cil_tmp8) {
3865
3866 } else {
3867 goto while_6_break;
3868 }
3869 }
3870 {
3871#line 65
3872 mem_17 = (int (**)(int , int ))cf;
3873#line 65
3874 __cil_tmp10 = *mem_17;
3875#line 65
3876 __cil_tmp11 = (unsigned long )cf;
3877#line 65
3878 __cil_tmp12 = __cil_tmp11 + 8;
3879#line 65
3880 mem_18 = (int *)__cil_tmp12;
3881#line 65
3882 __cil_tmp13 = *mem_18;
3883#line 65
3884 (*__cil_tmp10)(4, __cil_tmp13);
3885#line 66
3886 __cil_tmp14 = (unsigned long )cf;
3887#line 66
3888 __cil_tmp15 = __cil_tmp14 + 16;
3889#line 66
3890 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
3891#line 66
3892 cf = *mem_19;
3893 }
3894 }
3895 while_6_break: ;
3896 }
3897 {
3898#line 69
3899 __utac__exception__cf_handler_free(exception);
3900 }
3901#line 732 "libacc.c"
3902 return;
3903}
3904}
3905#line 80 "libacc.c"
3906void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
3907#line 80 "libacc.c"
3908static struct __ACC__ERR *head = (struct __ACC__ERR *)0;
3909#line 79 "libacc.c"
3910void *__utac__error_stack_mgt(void *env , int mode , int count )
3911{ void *retValue_acc ;
3912 struct __ACC__ERR *new ;
3913 void *tmp ;
3914 struct __ACC__ERR *temp ;
3915 struct __ACC__ERR *next ;
3916 void *excep ;
3917 unsigned long __cil_tmp10 ;
3918 unsigned long __cil_tmp11 ;
3919 unsigned long __cil_tmp12 ;
3920 unsigned long __cil_tmp13 ;
3921 void *__cil_tmp14 ;
3922 unsigned long __cil_tmp15 ;
3923 unsigned long __cil_tmp16 ;
3924 void *__cil_tmp17 ;
3925 void **mem_18 ;
3926 struct __ACC__ERR **mem_19 ;
3927 struct __ACC__ERR **mem_20 ;
3928 void **mem_21 ;
3929 struct __ACC__ERR **mem_22 ;
3930 void **mem_23 ;
3931 void **mem_24 ;
3932
3933 {
3934#line 82 "libacc.c"
3935 if (count == 0) {
3936#line 758 "libacc.c"
3937 return (retValue_acc);
3938 } else {
3939
3940 }
3941#line 86 "libacc.c"
3942 if (mode == 0) {
3943 {
3944#line 87
3945 tmp = malloc(16UL);
3946#line 87
3947 new = (struct __ACC__ERR *)tmp;
3948#line 88
3949 mem_18 = (void **)new;
3950#line 88
3951 *mem_18 = env;
3952#line 89
3953 __cil_tmp10 = (unsigned long )new;
3954#line 89
3955 __cil_tmp11 = __cil_tmp10 + 8;
3956#line 89
3957 mem_19 = (struct __ACC__ERR **)__cil_tmp11;
3958#line 89
3959 *mem_19 = head;
3960#line 90
3961 head = new;
3962#line 776 "libacc.c"
3963 retValue_acc = (void *)new;
3964 }
3965#line 778
3966 return (retValue_acc);
3967 } else {
3968
3969 }
3970#line 94 "libacc.c"
3971 if (mode == 1) {
3972#line 95
3973 temp = head;
3974 {
3975#line 98
3976 while (1) {
3977 while_7_continue: ;
3978#line 98
3979 if (count > 1) {
3980
3981 } else {
3982 goto while_7_break;
3983 }
3984 {
3985#line 99
3986 __cil_tmp12 = (unsigned long )temp;
3987#line 99
3988 __cil_tmp13 = __cil_tmp12 + 8;
3989#line 99
3990 mem_20 = (struct __ACC__ERR **)__cil_tmp13;
3991#line 99
3992 next = *mem_20;
3993#line 100
3994 mem_21 = (void **)temp;
3995#line 100
3996 excep = *mem_21;
3997#line 101
3998 __cil_tmp14 = (void *)temp;
3999#line 101
4000 free(__cil_tmp14);
4001#line 102
4002 __utac__exception__cf_handler_reset(excep);
4003#line 103
4004 temp = next;
4005#line 104
4006 count = count - 1;
4007 }
4008 }
4009 while_7_break: ;
4010 }
4011 {
4012#line 107
4013 __cil_tmp15 = (unsigned long )temp;
4014#line 107
4015 __cil_tmp16 = __cil_tmp15 + 8;
4016#line 107
4017 mem_22 = (struct __ACC__ERR **)__cil_tmp16;
4018#line 107
4019 head = *mem_22;
4020#line 108
4021 mem_23 = (void **)temp;
4022#line 108
4023 excep = *mem_23;
4024#line 109
4025 __cil_tmp17 = (void *)temp;
4026#line 109
4027 free(__cil_tmp17);
4028#line 110
4029 __utac__exception__cf_handler_reset(excep);
4030#line 820 "libacc.c"
4031 retValue_acc = excep;
4032 }
4033#line 822
4034 return (retValue_acc);
4035 } else {
4036
4037 }
4038#line 114
4039 if (mode == 2) {
4040#line 118 "libacc.c"
4041 if (head) {
4042#line 831
4043 mem_24 = (void **)head;
4044#line 831
4045 retValue_acc = *mem_24;
4046#line 833
4047 return (retValue_acc);
4048 } else {
4049#line 837 "libacc.c"
4050 retValue_acc = (void *)0;
4051#line 839
4052 return (retValue_acc);
4053 }
4054 } else {
4055
4056 }
4057#line 846 "libacc.c"
4058 return (retValue_acc);
4059}
4060}
4061#line 122 "libacc.c"
4062void *__utac__get_this_arg(int i , struct JoinPoint *this )
4063{ void *retValue_acc ;
4064 unsigned long __cil_tmp4 ;
4065 unsigned long __cil_tmp5 ;
4066 int __cil_tmp6 ;
4067 int __cil_tmp7 ;
4068 unsigned long __cil_tmp8 ;
4069 unsigned long __cil_tmp9 ;
4070 void **__cil_tmp10 ;
4071 void **__cil_tmp11 ;
4072 int *mem_12 ;
4073 void ***mem_13 ;
4074
4075 {
4076#line 123
4077 if (i > 0) {
4078 {
4079#line 123
4080 __cil_tmp4 = (unsigned long )this;
4081#line 123
4082 __cil_tmp5 = __cil_tmp4 + 16;
4083#line 123
4084 mem_12 = (int *)__cil_tmp5;
4085#line 123
4086 __cil_tmp6 = *mem_12;
4087#line 123
4088 if (i <= __cil_tmp6) {
4089
4090 } else {
4091 {
4092#line 123
4093 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
4094 123U, "__utac__get_this_arg");
4095 }
4096 }
4097 }
4098 } else {
4099 {
4100#line 123
4101 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
4102 123U, "__utac__get_this_arg");
4103 }
4104 }
4105#line 870 "libacc.c"
4106 __cil_tmp7 = i - 1;
4107#line 870
4108 __cil_tmp8 = (unsigned long )this;
4109#line 870
4110 __cil_tmp9 = __cil_tmp8 + 8;
4111#line 870
4112 mem_13 = (void ***)__cil_tmp9;
4113#line 870
4114 __cil_tmp10 = *mem_13;
4115#line 870
4116 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
4117#line 870
4118 retValue_acc = *__cil_tmp11;
4119#line 872
4120 return (retValue_acc);
4121#line 879
4122 return (retValue_acc);
4123}
4124}
4125#line 129 "libacc.c"
4126char const *__utac__get_this_argtype(int i , struct JoinPoint *this )
4127{ char const *retValue_acc ;
4128 unsigned long __cil_tmp4 ;
4129 unsigned long __cil_tmp5 ;
4130 int __cil_tmp6 ;
4131 int __cil_tmp7 ;
4132 unsigned long __cil_tmp8 ;
4133 unsigned long __cil_tmp9 ;
4134 char const **__cil_tmp10 ;
4135 char const **__cil_tmp11 ;
4136 int *mem_12 ;
4137 char const ***mem_13 ;
4138
4139 {
4140#line 131
4141 if (i > 0) {
4142 {
4143#line 131
4144 __cil_tmp4 = (unsigned long )this;
4145#line 131
4146 __cil_tmp5 = __cil_tmp4 + 16;
4147#line 131
4148 mem_12 = (int *)__cil_tmp5;
4149#line 131
4150 __cil_tmp6 = *mem_12;
4151#line 131
4152 if (i <= __cil_tmp6) {
4153
4154 } else {
4155 {
4156#line 131
4157 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
4158 131U, "__utac__get_this_argtype");
4159 }
4160 }
4161 }
4162 } else {
4163 {
4164#line 131
4165 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
4166 131U, "__utac__get_this_argtype");
4167 }
4168 }
4169#line 903 "libacc.c"
4170 __cil_tmp7 = i - 1;
4171#line 903
4172 __cil_tmp8 = (unsigned long )this;
4173#line 903
4174 __cil_tmp9 = __cil_tmp8 + 24;
4175#line 903
4176 mem_13 = (char const ***)__cil_tmp9;
4177#line 903
4178 __cil_tmp10 = *mem_13;
4179#line 903
4180 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
4181#line 903
4182 retValue_acc = *__cil_tmp11;
4183#line 905
4184 return (retValue_acc);
4185#line 912
4186 return (retValue_acc);
4187}
4188}
4189#line 1 "Specification9_spec.o"
4190#pragma merger(0,"Specification9_spec.i","")
4191#line 4 "wsllib.h"
4192void __automaton_fail(void) ;
4193#line 7 "Specification9_spec.c"
4194int floorButtons_spc9_0 ;
4195#line 8 "Specification9_spec.c"
4196int floorButtons_spc9_1 ;
4197#line 9 "Specification9_spec.c"
4198int floorButtons_spc9_2 ;
4199#line 10 "Specification9_spec.c"
4200int floorButtons_spc9_3 ;
4201#line 11 "Specification9_spec.c"
4202int floorButtons_spc9_4 ;
4203#line 15 "Specification9_spec.c"
4204void __utac_acc__Specification9_spec__1(void)
4205{
4206
4207 {
4208#line 17
4209 floorButtons_spc9_0 = 0;
4210#line 18
4211 floorButtons_spc9_1 = 0;
4212#line 19
4213 floorButtons_spc9_2 = 0;
4214#line 20
4215 floorButtons_spc9_3 = 0;
4216#line 21
4217 floorButtons_spc9_4 = 0;
4218#line 21
4219 return;
4220}
4221}
4222#line 25 "Specification9_spec.c"
4223void __utac_acc__Specification9_spec__2(int floor )
4224{
4225
4226 {
4227#line 33
4228 if (floor == 0) {
4229#line 34
4230 floorButtons_spc9_0 = 1;
4231 } else {
4232#line 35
4233 if (floor == 1) {
4234#line 36
4235 floorButtons_spc9_1 = 1;
4236 } else {
4237#line 37
4238 if (floor == 2) {
4239#line 38
4240 floorButtons_spc9_2 = 1;
4241 } else {
4242#line 39
4243 if (floor == 3) {
4244#line 40
4245 floorButtons_spc9_3 = 1;
4246 } else {
4247#line 41
4248 if (floor == 4) {
4249#line 42
4250 floorButtons_spc9_4 = 1;
4251 } else {
4252
4253 }
4254 }
4255 }
4256 }
4257 }
4258#line 42
4259 return;
4260}
4261}
4262#line 35 "Specification9_spec.c"
4263void __utac_acc__Specification9_spec__3(void)
4264{ int floor ;
4265 int tmp ;
4266 int tmp___0 ;
4267 int tmp___1 ;
4268
4269 {
4270 {
4271#line 37
4272 tmp = getCurrentFloorID();
4273#line 37
4274 floor = tmp;
4275#line 38
4276 tmp___1 = isEmpty();
4277 }
4278#line 38
4279 if (tmp___1) {
4280#line 39
4281 floorButtons_spc9_0 = 0;
4282#line 40
4283 floorButtons_spc9_1 = 0;
4284#line 41
4285 floorButtons_spc9_2 = 0;
4286#line 42
4287 floorButtons_spc9_3 = 0;
4288#line 43
4289 floorButtons_spc9_4 = 0;
4290 } else {
4291 {
4292#line 44
4293 tmp___0 = areDoorsOpen();
4294 }
4295#line 44
4296 if (tmp___0) {
4297#line 50
4298 if (floor == 0) {
4299#line 50
4300 if (floorButtons_spc9_0) {
4301#line 51
4302 floorButtons_spc9_0 = 0;
4303 } else {
4304 goto _L___2;
4305 }
4306 } else {
4307 _L___2:
4308#line 52
4309 if (floor == 1) {
4310#line 52
4311 if (floorButtons_spc9_1) {
4312#line 53
4313 floorButtons_spc9_1 = 0;
4314 } else {
4315 goto _L___1;
4316 }
4317 } else {
4318 _L___1:
4319#line 54
4320 if (floor == 2) {
4321#line 54
4322 if (floorButtons_spc9_2) {
4323#line 55
4324 floorButtons_spc9_2 = 0;
4325 } else {
4326 goto _L___0;
4327 }
4328 } else {
4329 _L___0:
4330#line 56
4331 if (floor == 3) {
4332#line 56
4333 if (floorButtons_spc9_3) {
4334#line 57
4335 floorButtons_spc9_3 = 0;
4336 } else {
4337 goto _L;
4338 }
4339 } else {
4340 _L:
4341#line 58
4342 if (floor == 4) {
4343#line 58
4344 if (floorButtons_spc9_4) {
4345#line 59
4346 floorButtons_spc9_4 = 0;
4347 } else {
4348
4349 }
4350 } else {
4351
4352 }
4353 }
4354 }
4355 }
4356 }
4357 } else {
4358
4359 }
4360 }
4361#line 59
4362 return;
4363}
4364}
4365#line 54 "Specification9_spec.c"
4366void __utac_acc__Specification9_spec__4(void)
4367{
4368
4369 {
4370#line 62
4371 if (floorButtons_spc9_0) {
4372 {
4373#line 63
4374 __automaton_fail();
4375 }
4376 } else {
4377#line 64
4378 if (floorButtons_spc9_1) {
4379 {
4380#line 65
4381 __automaton_fail();
4382 }
4383 } else {
4384#line 66
4385 if (floorButtons_spc9_2) {
4386 {
4387#line 67
4388 __automaton_fail();
4389 }
4390 } else {
4391#line 68
4392 if (floorButtons_spc9_3) {
4393 {
4394#line 69
4395 __automaton_fail();
4396 }
4397 } else {
4398#line 70
4399 if (floorButtons_spc9_4) {
4400 {
4401#line 71
4402 __automaton_fail();
4403 }
4404 } else {
4405
4406 }
4407 }
4408 }
4409 }
4410 }
4411#line 71
4412 return;
4413}
4414}
4415#line 1 "Person.o"
4416#pragma merger(0,"Person.i","")
4417#line 10 "Person.h"
4418int getWeight(int person ) ;
4419#line 20 "Person.c"
4420int getWeight(int person )
4421{ int retValue_acc ;
4422
4423 {
4424#line 35 "Person.c"
4425 if (person == 0) {
4426#line 974
4427 retValue_acc = 40;
4428#line 976
4429 return (retValue_acc);
4430 } else {
4431#line 978
4432 if (person == 1) {
4433#line 983
4434 retValue_acc = 40;
4435#line 985
4436 return (retValue_acc);
4437 } else {
4438#line 987
4439 if (person == 2) {
4440#line 992
4441 retValue_acc = 40;
4442#line 994
4443 return (retValue_acc);
4444 } else {
4445#line 996
4446 if (person == 3) {
4447#line 1001
4448 retValue_acc = 40;
4449#line 1003
4450 return (retValue_acc);
4451 } else {
4452#line 1005
4453 if (person == 4) {
4454#line 1010
4455 retValue_acc = 30;
4456#line 1012
4457 return (retValue_acc);
4458 } else {
4459#line 1014
4460 if (person == 5) {
4461#line 1019
4462 retValue_acc = 150;
4463#line 1021
4464 return (retValue_acc);
4465 } else {
4466#line 1027 "Person.c"
4467 retValue_acc = 0;
4468#line 1029
4469 return (retValue_acc);
4470 }
4471 }
4472 }
4473 }
4474 }
4475 }
4476#line 1036 "Person.c"
4477 return (retValue_acc);
4478}
4479}
4480#line 39 "Person.c"
4481int getOrigin(int person )
4482{ int retValue_acc ;
4483
4484 {
4485#line 54 "Person.c"
4486 if (person == 0) {
4487#line 1061
4488 retValue_acc = 4;
4489#line 1063
4490 return (retValue_acc);
4491 } else {
4492#line 1065
4493 if (person == 1) {
4494#line 1070
4495 retValue_acc = 3;
4496#line 1072
4497 return (retValue_acc);
4498 } else {
4499#line 1074
4500 if (person == 2) {
4501#line 1079
4502 retValue_acc = 2;
4503#line 1081
4504 return (retValue_acc);
4505 } else {
4506#line 1083
4507 if (person == 3) {
4508#line 1088
4509 retValue_acc = 1;
4510#line 1090
4511 return (retValue_acc);
4512 } else {
4513#line 1092
4514 if (person == 4) {
4515#line 1097
4516 retValue_acc = 0;
4517#line 1099
4518 return (retValue_acc);
4519 } else {
4520#line 1101
4521 if (person == 5) {
4522#line 1106
4523 retValue_acc = 1;
4524#line 1108
4525 return (retValue_acc);
4526 } else {
4527#line 1114 "Person.c"
4528 retValue_acc = 0;
4529#line 1116
4530 return (retValue_acc);
4531 }
4532 }
4533 }
4534 }
4535 }
4536 }
4537#line 1123 "Person.c"
4538 return (retValue_acc);
4539}
4540}
4541#line 57 "Person.c"
4542int getDestination(int person )
4543{ int retValue_acc ;
4544
4545 {
4546#line 72 "Person.c"
4547 if (person == 0) {
4548#line 1148
4549 retValue_acc = 0;
4550#line 1150
4551 return (retValue_acc);
4552 } else {
4553#line 1152
4554 if (person == 1) {
4555#line 1157
4556 retValue_acc = 0;
4557#line 1159
4558 return (retValue_acc);
4559 } else {
4560#line 1161
4561 if (person == 2) {
4562#line 1166
4563 retValue_acc = 1;
4564#line 1168
4565 return (retValue_acc);
4566 } else {
4567#line 1170
4568 if (person == 3) {
4569#line 1175
4570 retValue_acc = 3;
4571#line 1177
4572 return (retValue_acc);
4573 } else {
4574#line 1179
4575 if (person == 4) {
4576#line 1184
4577 retValue_acc = 1;
4578#line 1186
4579 return (retValue_acc);
4580 } else {
4581#line 1188
4582 if (person == 5) {
4583#line 1193
4584 retValue_acc = 3;
4585#line 1195
4586 return (retValue_acc);
4587 } else {
4588#line 1201 "Person.c"
4589 retValue_acc = 0;
4590#line 1203
4591 return (retValue_acc);
4592 }
4593 }
4594 }
4595 }
4596 }
4597 }
4598#line 1210 "Person.c"
4599 return (retValue_acc);
4600}
4601}
4602#line 1 "UnitTests.o"
4603#pragma merger(0,"UnitTests.i","")
4604#line 24 "UnitTests.c"
4605void spec1(void)
4606{ int tmp ;
4607 int tmp___0 ;
4608 int i ;
4609 int tmp___1 ;
4610
4611 {
4612 {
4613#line 25
4614 initBottomUp();
4615#line 26
4616 tmp = getOrigin(5);
4617#line 26
4618 initPersonOnFloor(5, tmp);
4619#line 27
4620 printState();
4621#line 30
4622 tmp___0 = getOrigin(2);
4623#line 30
4624 initPersonOnFloor(2, tmp___0);
4625#line 31
4626 printState();
4627#line 35
4628 i = 0;
4629 }
4630 {
4631#line 35
4632 while (1) {
4633 while_8_continue: ;
4634#line 35
4635 if (i < cleanupTimeShifts) {
4636 {
4637#line 35
4638 tmp___1 = isBlocked();
4639 }
4640#line 35
4641 if (tmp___1 != 1) {
4642
4643 } else {
4644 goto while_8_break;
4645 }
4646 } else {
4647 goto while_8_break;
4648 }
4649 {
4650#line 36
4651 timeShift();
4652#line 37
4653 printState();
4654#line 35
4655 i = i + 1;
4656 }
4657 }
4658 while_8_break: ;
4659 }
4660#line 1067 "UnitTests.c"
4661 return;
4662}
4663}
4664#line 42 "UnitTests.c"
4665void spec14(void)
4666{ int tmp ;
4667 int tmp___0 ;
4668 int i ;
4669 int tmp___1 ;
4670
4671 {
4672 {
4673#line 43
4674 initTopDown();
4675#line 44
4676 tmp = getOrigin(5);
4677#line 44
4678 initPersonOnFloor(5, tmp);
4679#line 45
4680 printState();
4681#line 47
4682 timeShift();
4683#line 48
4684 timeShift();
4685#line 49
4686 timeShift();
4687#line 50
4688 timeShift();
4689#line 52
4690 tmp___0 = getOrigin(0);
4691#line 52
4692 initPersonOnFloor(0, tmp___0);
4693#line 53
4694 printState();
4695#line 57
4696 i = 0;
4697 }
4698 {
4699#line 57
4700 while (1) {
4701 while_9_continue: ;
4702#line 57
4703 if (i < cleanupTimeShifts) {
4704 {
4705#line 57
4706 tmp___1 = isBlocked();
4707 }
4708#line 57
4709 if (tmp___1 != 1) {
4710
4711 } else {
4712 goto while_9_break;
4713 }
4714 } else {
4715 goto while_9_break;
4716 }
4717 {
4718#line 58
4719 timeShift();
4720#line 59
4721 printState();
4722#line 57
4723 i = i + 1;
4724 }
4725 }
4726 while_9_break: ;
4727 }
4728#line 1113 "UnitTests.c"
4729 return;
4730}
4731}
4732#line 1 "featureselect.o"
4733#pragma merger(0,"featureselect.i","")
4734#line 9 "featureselect.h"
4735int select_one(void) ;
4736#line 8 "featureselect.c"
4737int select_one(void)
4738{ int retValue_acc ;
4739 int choice = __VERIFIER_nondet_int();
4740
4741 {
4742#line 63 "featureselect.c"
4743 retValue_acc = choice;
4744#line 65
4745 return (retValue_acc);
4746#line 72
4747 return (retValue_acc);
4748}
4749}
4750#line 14 "featureselect.c"
4751void select_features(void)
4752{
4753
4754 {
4755#line 94 "featureselect.c"
4756 return;
4757}
4758}
4759#line 20 "featureselect.c"
4760void select_helpers(void)
4761{
4762
4763 {
4764#line 112 "featureselect.c"
4765 return;
4766}
4767}
4768#line 25 "featureselect.c"
4769int valid_product(void)
4770{ int retValue_acc ;
4771
4772 {
4773#line 130 "featureselect.c"
4774 retValue_acc = 1;
4775#line 132
4776 return (retValue_acc);
4777#line 139
4778 return (retValue_acc);
4779}
4780}
4781#line 1 "wsllib_check.o"
4782#pragma merger(0,"wsllib_check.i","")
4783#line 3 "wsllib_check.c"
4784void __automaton_fail(void)
4785{
4786
4787 {
4788 goto ERROR;
4789 ERROR: ;
4790#line 53 "wsllib_check.c"
4791 return;
4792}
4793}