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