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