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