Showing error 2029

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: product-lines/minepump_spec3_product59_unsafe.cil.c
Line in file: 988
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

 958    if (tmp___0 == 2) {
 959      {
 960#line 19
 961      tmp___1 = isPumpRunning();
 962      }
 963#line 19
 964      if (tmp___1) {
 965
 966      } else {
 967        {
 968#line 16
 969        __automaton_fail();
 970        }
 971      }
 972    } else {
 973
 974    }
 975  }
 976#line 16
 977  return;
 978}
 979}
 980#line 1 "wsllib_check.o"
 981#pragma merger(0,"wsllib_check.i","")
 982#line 3 "wsllib_check.c"
 983void __automaton_fail(void) 
 984{ 
 985
 986  {
 987  goto ERROR;
 988  ERROR: ;
 989#line 53 "wsllib_check.c"
 990  return;
 991}
 992}
 993#line 1 "scenario.o"
 994#pragma merger(0,"scenario.i","")
 995#line 12 "scenario.c"
 996void stopSystem(void) ;
 997#line 1 "scenario.c"
 998void test(void)
Show full sources
↑