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