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