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