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