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