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