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