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