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