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