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