Showing error 2102

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

Source: 

 938#line 12
 939      if (tmp___1) {
 940
 941      } else {
 942
 943      }
 944    }
 945    {
 946#line 14
 947    timeShift();
 948    }
 949  }
 950  while_3_break: /* CIL Label */ ;
 951  }
 952  {
 953#line 16
 954  cleanup();
 955  }
 956#line 76 "scenario.c"
 957  return;
 958}
 959}
 960#line 1 "wsllib_check.o"
 961#pragma merger(0,"wsllib_check.i","")
 962#line 3 "wsllib_check.c"
 963void __automaton_fail(void) 
 964{ 
 965
 966  {
 967  goto ERROR;
 968  ERROR: ;
 969#line 53 "wsllib_check.c"
 970  return;
 971}
 972}
 973#line 1 "Specification5_spec.o"
 974#pragma merger(0,"Specification5_spec.i","")
 975#line 7 "Specification5_spec.c"
 976int switchedOnBeforeTS  ;
 977#line 11 "Specification5_spec.c"
 978__inline void __utac_acc__Specification5_spec__1(void)
Show full sources
↑