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