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