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