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