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