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