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