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