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