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