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