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