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