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