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