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