Showing error 2054

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_spec4_product19_safe.cil.c
Line in file: 959
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

 929}
 930}
 931#line 70 "MinePump.c"
 932void stopSystem(void) 
 933{ 
 934
 935  {
 936#line 75
 937  if (pumpRunning) {
 938    {
 939#line 72
 940    deactivatePump();
 941    }
 942  } else {
 943
 944  }
 945#line 75
 946  systemActive = 0;
 947#line 343 "MinePump.c"
 948  return;
 949}
 950}
 951#line 1 "wsllib_check.o"
 952#pragma merger(0,"wsllib_check.i","")
 953#line 3 "wsllib_check.c"
 954void __automaton_fail(void) 
 955{ 
 956
 957  {
 958  goto ERROR;
 959  ERROR: ;
 960#line 53 "wsllib_check.c"
 961  return;
 962}
 963}
 964#line 1 "scenario.o"
 965#pragma merger(0,"scenario.i","")
 966#line 7 "scenario.c"
 967#line 16
 968void cleanup(void) ;
 969#line 1 "scenario.c"
Show full sources