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