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