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