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