1extern int __VERIFIER_nondet_int(void);
2extern int printf (__const char *__restrict __format, ...);
3
4
5
6#line 2 "libacc.c"
7struct JoinPoint {
8 void **(*fp)(struct JoinPoint * ) ;
9 void **args ;
10 int argsCount ;
11 char const **argsType ;
12 void *(*arg)(int , struct JoinPoint * ) ;
13 char const *(*argType)(int , struct JoinPoint * ) ;
14 void **retValue ;
15 char const *retType ;
16 char const *funcName ;
17 char const *targetName ;
18 char const *fileName ;
19 char const *kind ;
20 void *excep_return ;
21};
22#line 18 "libacc.c"
23struct __UTAC__CFLOW_FUNC {
24 int (*func)(int , int ) ;
25 int val ;
26 struct __UTAC__CFLOW_FUNC *next ;
27};
28#line 18 "libacc.c"
29struct __UTAC__EXCEPTION {
30 void *jumpbuf ;
31 unsigned long long prtValue ;
32 int pops ;
33 struct __UTAC__CFLOW_FUNC *cflowfuncs ;
34};
35#line 211 "/usr/lib/gcc/x86_64-linux-gnu/4.4.5/include/stddef.h"
36typedef unsigned long size_t;
37#line 76 "libacc.c"
38struct __ACC__ERR {
39 void *v ;
40 struct __ACC__ERR *next ;
41};
42#line 1 "featureselect.o"
43#pragma merger(0,"featureselect.i","")
44#line 8 "featureselect.h"
45int select_one(void) ;
46#line 10
47void select_features(void) ;
48#line 12
49void select_helpers(void) ;
50#line 14
51int valid_product(void) ;
52#line 8 "featureselect.c"
53int select_one(void)
54{ int retValue_acc ;
55 int choice = __VERIFIER_nondet_int();
56
57 {
58#line 62 "featureselect.c"
59 retValue_acc = choice;
60#line 64
61 return (retValue_acc);
62#line 71
63 return (retValue_acc);
64}
65}
66#line 14 "featureselect.c"
67void select_features(void)
68{
69
70 {
71#line 93 "featureselect.c"
72 return;
73}
74}
75#line 20 "featureselect.c"
76void select_helpers(void)
77{
78
79 {
80#line 111 "featureselect.c"
81 return;
82}
83}
84#line 25 "featureselect.c"
85int valid_product(void)
86{ int retValue_acc ;
87
88 {
89#line 129 "featureselect.c"
90 retValue_acc = 1;
91#line 131
92 return (retValue_acc);
93#line 138
94 return (retValue_acc);
95}
96}
97#line 1 "wsllib_check.o"
98#pragma merger(0,"wsllib_check.i","")
99#line 3 "wsllib_check.c"
100void __automaton_fail(void)
101{
102
103 {
104 goto ERROR;
105 ERROR: ;
106#line 53 "wsllib_check.c"
107 return;
108}
109}
110#line 1 "Environment.o"
111#pragma merger(0,"Environment.i","")
112#line 4 "Environment.h"
113void lowerWaterLevel(void) ;
114#line 6
115void waterRise(void) ;
116#line 8
117void changeMethaneLevel(void) ;
118#line 10
119int isMethaneLevelCritical(void) ;
120#line 12
121int getWaterLevel(void) ;
122#line 15
123void printEnvironment(void) ;
124#line 16
125int isLowWaterSensorDry(void) ;
126#line 9 "Environment.c"
127int waterLevel = 1;
128#line 12 "Environment.c"
129int methaneLevelCritical = 0;
130#line 15 "Environment.c"
131void lowerWaterLevel(void)
132{
133
134 {
135#line 19
136 if (waterLevel > 0) {
137#line 17
138 waterLevel = waterLevel - 1;
139 } else {
140
141 }
142#line 83 "Environment.c"
143 return;
144}
145}
146#line 22 "Environment.c"
147void waterRise(void)
148{
149
150 {
151#line 26
152 if (waterLevel < 2) {
153#line 24
154 waterLevel = waterLevel + 1;
155 } else {
156
157 }
158#line 106 "Environment.c"
159 return;
160}
161}
162#line 29 "Environment.c"
163void changeMethaneLevel(void)
164{
165
166 {
167#line 34
168 if (methaneLevelCritical) {
169#line 31
170 methaneLevelCritical = 0;
171 } else {
172#line 33
173 methaneLevelCritical = 1;
174 }
175#line 132 "Environment.c"
176 return;
177}
178}
179#line 38 "Environment.c"
180int isMethaneLevelCritical(void)
181{ int retValue_acc ;
182
183 {
184#line 150 "Environment.c"
185 retValue_acc = methaneLevelCritical;
186#line 152
187 return (retValue_acc);
188#line 159
189 return (retValue_acc);
190}
191}
192#line 45 "Environment.c"
193#line 44 "Environment.c"
194void printEnvironment(void)
195{
196
197 {
198 {
199#line 45
200 printf("Env(Water:%i", waterLevel);
201#line 46
202 printf(",Meth:");
203 }
204#line 47
205 if (methaneLevelCritical) {
206 {
207#line 48
208 printf("CRIT");
209 }
210 } else {
211 {
212#line 49
213 printf("OK");
214 }
215 }
216 {
217#line 51
218 printf(")");
219 }
220#line 191 "Environment.c"
221 return;
222}
223}
224#line 55 "Environment.c"
225int getWaterLevel(void)
226{ int retValue_acc ;
227
228 {
229#line 209 "Environment.c"
230 retValue_acc = waterLevel;
231#line 211
232 return (retValue_acc);
233#line 218
234 return (retValue_acc);
235}
236}
237#line 58 "Environment.c"
238int isLowWaterSensorDry(void)
239{ int retValue_acc ;
240
241 {
242#line 240 "Environment.c"
243 retValue_acc = waterLevel == 0;
244#line 242
245 return (retValue_acc);
246#line 249
247 return (retValue_acc);
248}
249}
250#line 1 "Test.o"
251#pragma merger(0,"Test.i","")
252#line 8 "Test.c"
253int cleanupTimeShifts = 4;
254#line 11 "Test.c"
255#line 20 "Test.c"
256void timeShift(void) ;
257#line 17 "Test.c"
258void cleanup(void)
259{ int i ;
260 int __cil_tmp2 ;
261
262 {
263 {
264#line 20
265 timeShift();
266#line 22
267 i = 0;
268 }
269 {
270#line 22
271 while (1) {
272 while_0_continue: ;
273 {
274#line 22
275 __cil_tmp2 = cleanupTimeShifts - 1;
276#line 22
277 if (i < __cil_tmp2) {
278
279 } else {
280 goto while_0_break;
281 }
282 }
283 {
284#line 23
285 timeShift();
286#line 22
287 i = i + 1;
288 }
289 }
290 while_0_break: ;
291 }
292#line 1111 "Test.c"
293 return;
294}
295}
296#line 57 "Test.c"
297void printPump(void) ;
298#line 56 "Test.c"
299void Specification2(void)
300{
301
302 {
303 {
304#line 57
305 timeShift();
306#line 57
307 printPump();
308#line 58
309 timeShift();
310#line 58
311 printPump();
312#line 59
313 timeShift();
314#line 59
315 printPump();
316#line 60
317 waterRise();
318#line 60
319 printPump();
320#line 61
321 timeShift();
322#line 61
323 printPump();
324#line 62
325 changeMethaneLevel();
326#line 62
327 printPump();
328#line 63
329 timeShift();
330#line 63
331 printPump();
332#line 64
333 cleanup();
334 }
335#line 1159 "Test.c"
336 return;
337}
338}
339#line 67 "Test.c"
340void setup(void)
341{
342
343 {
344#line 1177 "Test.c"
345 return;
346}
347}
348#line 1179
349void __utac_acc__Specification5_spec__1(void) ;
350#line 77 "Test.c"
351void test(void) ;
352#line 74 "Test.c"
353void runTest(void)
354{
355
356 {
357 {
358#line 1190 "Test.c"
359 __utac_acc__Specification5_spec__1();
360#line 77 "Test.c"
361 test();
362 }
363#line 1205 "Test.c"
364 return;
365}
366}
367#line 82 "Test.c"
368int main(void)
369{ int retValue_acc ;
370 int tmp ;
371
372 {
373 {
374#line 83
375 select_helpers();
376#line 84
377 select_features();
378#line 85
379 tmp = valid_product();
380 }
381#line 85
382 if (tmp) {
383 {
384#line 86
385 setup();
386#line 87
387 runTest();
388 }
389 } else {
390
391 }
392#line 1234 "Test.c"
393 retValue_acc = 0;
394#line 1236
395 return (retValue_acc);
396#line 1243
397 return (retValue_acc);
398}
399}
400#line 1 "MinePump.o"
401#pragma merger(0,"MinePump.i","")
402#line 6 "MinePump.h"
403void activatePump(void) ;
404#line 8
405void deactivatePump(void) ;
406#line 10
407int isPumpRunning(void) ;
408#line 7 "MinePump.c"
409int pumpRunning = 0;
410#line 9 "MinePump.c"
411int systemActive = 1;
412#line 10
413void __utac_acc__Specification5_spec__2(void) ;
414#line 13
415void __utac_acc__Specification5_spec__3(void) ;
416#line 16
417void processEnvironment(void) ;
418#line 12 "MinePump.c"
419void timeShift(void)
420{
421
422 {
423 {
424#line 87 "MinePump.c"
425 __utac_acc__Specification5_spec__2();
426 }
427#line 15
428 if (pumpRunning) {
429 {
430#line 16 "MinePump.c"
431 lowerWaterLevel();
432 }
433 } else {
434
435 }
436#line 15
437 if (systemActive) {
438 {
439#line 16
440 processEnvironment();
441 }
442 } else {
443
444 }
445 {
446#line 105 "MinePump.c"
447 __utac_acc__Specification5_spec__3();
448 }
449#line 111
450 return;
451}
452}
453#line 19 "MinePump.c"
454void processEnvironment__wrappee__base(void)
455{
456
457 {
458#line 129 "MinePump.c"
459 return;
460}
461}
462#line 28 "MinePump.c"
463int isLowWaterLevel(void) ;
464#line 23 "MinePump.c"
465void processEnvironment__wrappee__methaneQuery(void)
466{ int tmp ;
467
468 {
469#line 28
470 if (pumpRunning) {
471 {
472#line 28
473 tmp = isLowWaterLevel();
474 }
475#line 28
476 if (tmp) {
477 {
478#line 25
479 deactivatePump();
480 }
481 } else {
482 {
483#line 27
484 processEnvironment__wrappee__base();
485 }
486 }
487 } else {
488 {
489#line 27
490 processEnvironment__wrappee__base();
491 }
492 }
493#line 155 "MinePump.c"
494 return;
495}
496}
497#line 35 "MinePump.c"
498int isMethaneAlarm(void) ;
499#line 30 "MinePump.c"
500void processEnvironment(void)
501{ int tmp ;
502
503 {
504#line 35
505 if (pumpRunning) {
506 {
507#line 35
508 tmp = isMethaneAlarm();
509 }
510#line 35
511 if (tmp) {
512 {
513#line 32
514 deactivatePump();
515 }
516 } else {
517 {
518#line 34
519 processEnvironment__wrappee__methaneQuery();
520 }
521 }
522 } else {
523 {
524#line 34
525 processEnvironment__wrappee__methaneQuery();
526 }
527 }
528#line 181 "MinePump.c"
529 return;
530}
531}
532#line 39 "MinePump.c"
533void activatePump__wrappee__lowWaterSensor(void)
534{
535
536 {
537#line 40
538 pumpRunning = 1;
539#line 201 "MinePump.c"
540 return;
541}
542}
543#line 42 "MinePump.c"
544void activatePump(void)
545{ int tmp ;
546
547 {
548 {
549#line 47
550 tmp = isMethaneAlarm();
551 }
552#line 47
553 if (tmp) {
554
555 } else {
556 {
557#line 44
558 activatePump__wrappee__lowWaterSensor();
559 }
560 }
561#line 225 "MinePump.c"
562 return;
563}
564}
565#line 51 "MinePump.c"
566void deactivatePump(void)
567{
568
569 {
570#line 52
571 pumpRunning = 0;
572#line 245 "MinePump.c"
573 return;
574}
575}
576#line 56 "MinePump.c"
577int isMethaneAlarm(void)
578{ int retValue_acc ;
579
580 {
581 {
582#line 263 "MinePump.c"
583 retValue_acc = isMethaneLevelCritical();
584 }
585#line 265
586 return (retValue_acc);
587#line 272
588 return (retValue_acc);
589}
590}
591#line 61 "MinePump.c"
592int isPumpRunning(void)
593{ int retValue_acc ;
594
595 {
596#line 294 "MinePump.c"
597 retValue_acc = pumpRunning;
598#line 296
599 return (retValue_acc);
600#line 303
601 return (retValue_acc);
602}
603}
604#line 66 "MinePump.c"
605void printPump(void)
606{
607
608 {
609 {
610#line 67
611 printf("Pump(System:");
612 }
613#line 68
614 if (systemActive) {
615 {
616#line 69
617 printf("On");
618 }
619 } else {
620 {
621#line 70
622 printf("Off");
623 }
624 }
625 {
626#line 72
627 printf(",Pump:");
628 }
629#line 73
630 if (pumpRunning) {
631 {
632#line 74
633 printf("On");
634 }
635 } else {
636 {
637#line 75
638 printf("Off");
639 }
640 }
641 {
642#line 77
643 printf(") ");
644#line 78
645 printEnvironment();
646#line 79
647 printf("\n");
648 }
649#line 343 "MinePump.c"
650 return;
651}
652}
653#line 81 "MinePump.c"
654int isLowWaterLevel(void)
655{ int retValue_acc ;
656 int tmp ;
657 int tmp___0 ;
658
659 {
660 {
661#line 361 "MinePump.c"
662 tmp = isLowWaterSensorDry();
663 }
664#line 361
665 if (tmp) {
666#line 361
667 tmp___0 = 0;
668 } else {
669#line 361
670 tmp___0 = 1;
671 }
672#line 361
673 retValue_acc = tmp___0;
674#line 363
675 return (retValue_acc);
676#line 370
677 return (retValue_acc);
678}
679}
680#line 1 "scenario.o"
681#pragma merger(0,"scenario.i","")
682#line 1 "scenario.c"
683void test(void)
684{ int splverifierCounter ;
685 int tmp ;
686 int tmp___0 ;
687 int tmp___1 ;
688 int tmp___2 ;
689
690 {
691#line 2
692 splverifierCounter = 0;
693 {
694#line 3
695 while (1) {
696 while_1_continue: ;
697#line 3
698 if (splverifierCounter < 4) {
699
700 } else {
701 goto while_1_break;
702 }
703 {
704#line 7
705 tmp = __VERIFIER_nondet_int();
706 }
707#line 7
708 if (tmp) {
709 {
710#line 5
711 waterRise();
712 }
713 } else {
714
715 }
716 {
717#line 7
718 tmp___0 = __VERIFIER_nondet_int();
719 }
720#line 7
721 if (tmp___0) {
722 {
723#line 8
724 changeMethaneLevel();
725 }
726 } else {
727
728 }
729 {
730#line 10
731 tmp___2 = __VERIFIER_nondet_int();
732 }
733#line 10
734 if (tmp___2) {
735
736 } else {
737 {
738#line 12
739 tmp___1 = __VERIFIER_nondet_int();
740 }
741#line 12
742 if (tmp___1) {
743
744 } else {
745
746 }
747 }
748 {
749#line 13
750 timeShift();
751 }
752 }
753 while_1_break: ;
754 }
755 {
756#line 15
757 cleanup();
758 }
759#line 74 "scenario.c"
760 return;
761}
762}
763#line 1 "libacc.o"
764#pragma merger(0,"libacc.i","")
765#line 73 "/usr/include/assert.h"
766extern __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const *__assertion ,
767 char const *__file ,
768 unsigned int __line ,
769 char const *__function ) ;
770#line 471 "/usr/include/stdlib.h"
771extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
772#line 488
773extern __attribute__((__nothrow__)) void free(void *__ptr ) ;
774#line 32 "libacc.c"
775void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int ,
776 int ) ,
777 int val )
778{ struct __UTAC__EXCEPTION *excep ;
779 struct __UTAC__CFLOW_FUNC *cf ;
780 void *tmp ;
781 unsigned long __cil_tmp7 ;
782 unsigned long __cil_tmp8 ;
783 unsigned long __cil_tmp9 ;
784 unsigned long __cil_tmp10 ;
785 unsigned long __cil_tmp11 ;
786 unsigned long __cil_tmp12 ;
787 unsigned long __cil_tmp13 ;
788 unsigned long __cil_tmp14 ;
789 int (**mem_15)(int , int ) ;
790 int *mem_16 ;
791 struct __UTAC__CFLOW_FUNC **mem_17 ;
792 struct __UTAC__CFLOW_FUNC **mem_18 ;
793 struct __UTAC__CFLOW_FUNC **mem_19 ;
794
795 {
796 {
797#line 33
798 excep = (struct __UTAC__EXCEPTION *)exception;
799#line 34
800 tmp = malloc(24UL);
801#line 34
802 cf = (struct __UTAC__CFLOW_FUNC *)tmp;
803#line 36
804 mem_15 = (int (**)(int , int ))cf;
805#line 36
806 *mem_15 = cflow_func;
807#line 37
808 __cil_tmp7 = (unsigned long )cf;
809#line 37
810 __cil_tmp8 = __cil_tmp7 + 8;
811#line 37
812 mem_16 = (int *)__cil_tmp8;
813#line 37
814 *mem_16 = val;
815#line 38
816 __cil_tmp9 = (unsigned long )cf;
817#line 38
818 __cil_tmp10 = __cil_tmp9 + 16;
819#line 38
820 __cil_tmp11 = (unsigned long )excep;
821#line 38
822 __cil_tmp12 = __cil_tmp11 + 24;
823#line 38
824 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
825#line 38
826 mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
827#line 38
828 *mem_17 = *mem_18;
829#line 39
830 __cil_tmp13 = (unsigned long )excep;
831#line 39
832 __cil_tmp14 = __cil_tmp13 + 24;
833#line 39
834 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
835#line 39
836 *mem_19 = cf;
837 }
838#line 654 "libacc.c"
839 return;
840}
841}
842#line 44 "libacc.c"
843void __utac__exception__cf_handler_free(void *exception )
844{ struct __UTAC__EXCEPTION *excep ;
845 struct __UTAC__CFLOW_FUNC *cf ;
846 struct __UTAC__CFLOW_FUNC *tmp ;
847 unsigned long __cil_tmp5 ;
848 unsigned long __cil_tmp6 ;
849 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
850 unsigned long __cil_tmp8 ;
851 unsigned long __cil_tmp9 ;
852 unsigned long __cil_tmp10 ;
853 unsigned long __cil_tmp11 ;
854 void *__cil_tmp12 ;
855 unsigned long __cil_tmp13 ;
856 unsigned long __cil_tmp14 ;
857 struct __UTAC__CFLOW_FUNC **mem_15 ;
858 struct __UTAC__CFLOW_FUNC **mem_16 ;
859 struct __UTAC__CFLOW_FUNC **mem_17 ;
860
861 {
862#line 45
863 excep = (struct __UTAC__EXCEPTION *)exception;
864#line 46
865 __cil_tmp5 = (unsigned long )excep;
866#line 46
867 __cil_tmp6 = __cil_tmp5 + 24;
868#line 46
869 mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
870#line 46
871 cf = *mem_15;
872 {
873#line 49
874 while (1) {
875 while_2_continue: ;
876 {
877#line 49
878 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
879#line 49
880 __cil_tmp8 = (unsigned long )__cil_tmp7;
881#line 49
882 __cil_tmp9 = (unsigned long )cf;
883#line 49
884 if (__cil_tmp9 != __cil_tmp8) {
885
886 } else {
887 goto while_2_break;
888 }
889 }
890 {
891#line 50
892 tmp = cf;
893#line 51
894 __cil_tmp10 = (unsigned long )cf;
895#line 51
896 __cil_tmp11 = __cil_tmp10 + 16;
897#line 51
898 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
899#line 51
900 cf = *mem_16;
901#line 52
902 __cil_tmp12 = (void *)tmp;
903#line 52
904 free(__cil_tmp12);
905 }
906 }
907 while_2_break: ;
908 }
909#line 55
910 __cil_tmp13 = (unsigned long )excep;
911#line 55
912 __cil_tmp14 = __cil_tmp13 + 24;
913#line 55
914 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
915#line 55
916 *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
917#line 694 "libacc.c"
918 return;
919}
920}
921#line 59 "libacc.c"
922void __utac__exception__cf_handler_reset(void *exception )
923{ struct __UTAC__EXCEPTION *excep ;
924 struct __UTAC__CFLOW_FUNC *cf ;
925 unsigned long __cil_tmp5 ;
926 unsigned long __cil_tmp6 ;
927 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
928 unsigned long __cil_tmp8 ;
929 unsigned long __cil_tmp9 ;
930 int (*__cil_tmp10)(int , int ) ;
931 unsigned long __cil_tmp11 ;
932 unsigned long __cil_tmp12 ;
933 int __cil_tmp13 ;
934 unsigned long __cil_tmp14 ;
935 unsigned long __cil_tmp15 ;
936 struct __UTAC__CFLOW_FUNC **mem_16 ;
937 int (**mem_17)(int , int ) ;
938 int *mem_18 ;
939 struct __UTAC__CFLOW_FUNC **mem_19 ;
940
941 {
942#line 60
943 excep = (struct __UTAC__EXCEPTION *)exception;
944#line 61
945 __cil_tmp5 = (unsigned long )excep;
946#line 61
947 __cil_tmp6 = __cil_tmp5 + 24;
948#line 61
949 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
950#line 61
951 cf = *mem_16;
952 {
953#line 64
954 while (1) {
955 while_3_continue: ;
956 {
957#line 64
958 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
959#line 64
960 __cil_tmp8 = (unsigned long )__cil_tmp7;
961#line 64
962 __cil_tmp9 = (unsigned long )cf;
963#line 64
964 if (__cil_tmp9 != __cil_tmp8) {
965
966 } else {
967 goto while_3_break;
968 }
969 }
970 {
971#line 65
972 mem_17 = (int (**)(int , int ))cf;
973#line 65
974 __cil_tmp10 = *mem_17;
975#line 65
976 __cil_tmp11 = (unsigned long )cf;
977#line 65
978 __cil_tmp12 = __cil_tmp11 + 8;
979#line 65
980 mem_18 = (int *)__cil_tmp12;
981#line 65
982 __cil_tmp13 = *mem_18;
983#line 65
984 (*__cil_tmp10)(4, __cil_tmp13);
985#line 66
986 __cil_tmp14 = (unsigned long )cf;
987#line 66
988 __cil_tmp15 = __cil_tmp14 + 16;
989#line 66
990 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
991#line 66
992 cf = *mem_19;
993 }
994 }
995 while_3_break: ;
996 }
997 {
998#line 69
999 __utac__exception__cf_handler_free(exception);
1000 }
1001#line 732 "libacc.c"
1002 return;
1003}
1004}
1005#line 80 "libacc.c"
1006void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
1007#line 80 "libacc.c"
1008static struct __ACC__ERR *head = (struct __ACC__ERR *)0;
1009#line 79 "libacc.c"
1010void *__utac__error_stack_mgt(void *env , int mode , int count )
1011{ void *retValue_acc ;
1012 struct __ACC__ERR *new ;
1013 void *tmp ;
1014 struct __ACC__ERR *temp ;
1015 struct __ACC__ERR *next ;
1016 void *excep ;
1017 unsigned long __cil_tmp10 ;
1018 unsigned long __cil_tmp11 ;
1019 unsigned long __cil_tmp12 ;
1020 unsigned long __cil_tmp13 ;
1021 void *__cil_tmp14 ;
1022 unsigned long __cil_tmp15 ;
1023 unsigned long __cil_tmp16 ;
1024 void *__cil_tmp17 ;
1025 void **mem_18 ;
1026 struct __ACC__ERR **mem_19 ;
1027 struct __ACC__ERR **mem_20 ;
1028 void **mem_21 ;
1029 struct __ACC__ERR **mem_22 ;
1030 void **mem_23 ;
1031 void **mem_24 ;
1032
1033 {
1034#line 82 "libacc.c"
1035 if (count == 0) {
1036#line 758 "libacc.c"
1037 return (retValue_acc);
1038 } else {
1039
1040 }
1041#line 86 "libacc.c"
1042 if (mode == 0) {
1043 {
1044#line 87
1045 tmp = malloc(16UL);
1046#line 87
1047 new = (struct __ACC__ERR *)tmp;
1048#line 88
1049 mem_18 = (void **)new;
1050#line 88
1051 *mem_18 = env;
1052#line 89
1053 __cil_tmp10 = (unsigned long )new;
1054#line 89
1055 __cil_tmp11 = __cil_tmp10 + 8;
1056#line 89
1057 mem_19 = (struct __ACC__ERR **)__cil_tmp11;
1058#line 89
1059 *mem_19 = head;
1060#line 90
1061 head = new;
1062#line 776 "libacc.c"
1063 retValue_acc = (void *)new;
1064 }
1065#line 778
1066 return (retValue_acc);
1067 } else {
1068
1069 }
1070#line 94 "libacc.c"
1071 if (mode == 1) {
1072#line 95
1073 temp = head;
1074 {
1075#line 98
1076 while (1) {
1077 while_4_continue: ;
1078#line 98
1079 if (count > 1) {
1080
1081 } else {
1082 goto while_4_break;
1083 }
1084 {
1085#line 99
1086 __cil_tmp12 = (unsigned long )temp;
1087#line 99
1088 __cil_tmp13 = __cil_tmp12 + 8;
1089#line 99
1090 mem_20 = (struct __ACC__ERR **)__cil_tmp13;
1091#line 99
1092 next = *mem_20;
1093#line 100
1094 mem_21 = (void **)temp;
1095#line 100
1096 excep = *mem_21;
1097#line 101
1098 __cil_tmp14 = (void *)temp;
1099#line 101
1100 free(__cil_tmp14);
1101#line 102
1102 __utac__exception__cf_handler_reset(excep);
1103#line 103
1104 temp = next;
1105#line 104
1106 count = count - 1;
1107 }
1108 }
1109 while_4_break: ;
1110 }
1111 {
1112#line 107
1113 __cil_tmp15 = (unsigned long )temp;
1114#line 107
1115 __cil_tmp16 = __cil_tmp15 + 8;
1116#line 107
1117 mem_22 = (struct __ACC__ERR **)__cil_tmp16;
1118#line 107
1119 head = *mem_22;
1120#line 108
1121 mem_23 = (void **)temp;
1122#line 108
1123 excep = *mem_23;
1124#line 109
1125 __cil_tmp17 = (void *)temp;
1126#line 109
1127 free(__cil_tmp17);
1128#line 110
1129 __utac__exception__cf_handler_reset(excep);
1130#line 820 "libacc.c"
1131 retValue_acc = excep;
1132 }
1133#line 822
1134 return (retValue_acc);
1135 } else {
1136
1137 }
1138#line 114
1139 if (mode == 2) {
1140#line 118 "libacc.c"
1141 if (head) {
1142#line 831
1143 mem_24 = (void **)head;
1144#line 831
1145 retValue_acc = *mem_24;
1146#line 833
1147 return (retValue_acc);
1148 } else {
1149#line 837 "libacc.c"
1150 retValue_acc = (void *)0;
1151#line 839
1152 return (retValue_acc);
1153 }
1154 } else {
1155
1156 }
1157#line 846 "libacc.c"
1158 return (retValue_acc);
1159}
1160}
1161#line 122 "libacc.c"
1162void *__utac__get_this_arg(int i , struct JoinPoint *this )
1163{ void *retValue_acc ;
1164 unsigned long __cil_tmp4 ;
1165 unsigned long __cil_tmp5 ;
1166 int __cil_tmp6 ;
1167 int __cil_tmp7 ;
1168 unsigned long __cil_tmp8 ;
1169 unsigned long __cil_tmp9 ;
1170 void **__cil_tmp10 ;
1171 void **__cil_tmp11 ;
1172 int *mem_12 ;
1173 void ***mem_13 ;
1174
1175 {
1176#line 123
1177 if (i > 0) {
1178 {
1179#line 123
1180 __cil_tmp4 = (unsigned long )this;
1181#line 123
1182 __cil_tmp5 = __cil_tmp4 + 16;
1183#line 123
1184 mem_12 = (int *)__cil_tmp5;
1185#line 123
1186 __cil_tmp6 = *mem_12;
1187#line 123
1188 if (i <= __cil_tmp6) {
1189
1190 } else {
1191 {
1192#line 123
1193 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
1194 123U, "__utac__get_this_arg");
1195 }
1196 }
1197 }
1198 } else {
1199 {
1200#line 123
1201 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
1202 123U, "__utac__get_this_arg");
1203 }
1204 }
1205#line 870 "libacc.c"
1206 __cil_tmp7 = i - 1;
1207#line 870
1208 __cil_tmp8 = (unsigned long )this;
1209#line 870
1210 __cil_tmp9 = __cil_tmp8 + 8;
1211#line 870
1212 mem_13 = (void ***)__cil_tmp9;
1213#line 870
1214 __cil_tmp10 = *mem_13;
1215#line 870
1216 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
1217#line 870
1218 retValue_acc = *__cil_tmp11;
1219#line 872
1220 return (retValue_acc);
1221#line 879
1222 return (retValue_acc);
1223}
1224}
1225#line 129 "libacc.c"
1226char const *__utac__get_this_argtype(int i , struct JoinPoint *this )
1227{ char const *retValue_acc ;
1228 unsigned long __cil_tmp4 ;
1229 unsigned long __cil_tmp5 ;
1230 int __cil_tmp6 ;
1231 int __cil_tmp7 ;
1232 unsigned long __cil_tmp8 ;
1233 unsigned long __cil_tmp9 ;
1234 char const **__cil_tmp10 ;
1235 char const **__cil_tmp11 ;
1236 int *mem_12 ;
1237 char const ***mem_13 ;
1238
1239 {
1240#line 131
1241 if (i > 0) {
1242 {
1243#line 131
1244 __cil_tmp4 = (unsigned long )this;
1245#line 131
1246 __cil_tmp5 = __cil_tmp4 + 16;
1247#line 131
1248 mem_12 = (int *)__cil_tmp5;
1249#line 131
1250 __cil_tmp6 = *mem_12;
1251#line 131
1252 if (i <= __cil_tmp6) {
1253
1254 } else {
1255 {
1256#line 131
1257 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
1258 131U, "__utac__get_this_argtype");
1259 }
1260 }
1261 }
1262 } else {
1263 {
1264#line 131
1265 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
1266 131U, "__utac__get_this_argtype");
1267 }
1268 }
1269#line 903 "libacc.c"
1270 __cil_tmp7 = i - 1;
1271#line 903
1272 __cil_tmp8 = (unsigned long )this;
1273#line 903
1274 __cil_tmp9 = __cil_tmp8 + 24;
1275#line 903
1276 mem_13 = (char const ***)__cil_tmp9;
1277#line 903
1278 __cil_tmp10 = *mem_13;
1279#line 903
1280 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
1281#line 903
1282 retValue_acc = *__cil_tmp11;
1283#line 905
1284 return (retValue_acc);
1285#line 912
1286 return (retValue_acc);
1287}
1288}
1289#line 1 "Specification5_spec.o"
1290#pragma merger(0,"Specification5_spec.i","")
1291#line 7 "Specification5_spec.c"
1292int switchedOnBeforeTS ;
1293#line 11 "Specification5_spec.c"
1294void __utac_acc__Specification5_spec__1(void)
1295{
1296
1297 {
1298#line 13
1299 switchedOnBeforeTS = 0;
1300#line 13
1301 return;
1302}
1303}
1304#line 17 "Specification5_spec.c"
1305void __utac_acc__Specification5_spec__2(void)
1306{
1307
1308 {
1309 {
1310#line 19
1311 switchedOnBeforeTS = isPumpRunning();
1312 }
1313#line 19
1314 return;
1315}
1316}
1317#line 23 "Specification5_spec.c"
1318void __utac_acc__Specification5_spec__3(void)
1319{ int tmp ;
1320 int tmp___0 ;
1321
1322 {
1323 {
1324#line 31
1325 tmp = getWaterLevel();
1326 }
1327#line 31
1328 if (tmp != 2) {
1329 {
1330#line 31
1331 tmp___0 = isPumpRunning();
1332 }
1333#line 31
1334 if (tmp___0) {
1335#line 31
1336 if (! switchedOnBeforeTS) {
1337 {
1338#line 28
1339 __automaton_fail();
1340 }
1341 } else {
1342
1343 }
1344 } else {
1345
1346 }
1347 } else {
1348
1349 }
1350#line 28
1351 return;
1352}
1353}