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