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