Showing error 1871

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

Source: 

 777#line 12
 778        stopSystem();
 779        }
 780      } else {
 781
 782      }
 783    }
 784    {
 785#line 14
 786    timeShift();
 787    }
 788  }
 789  while_1_break: /* CIL Label */ ;
 790  }
 791  {
 792#line 16
 793  cleanup();
 794  }
 795#line 76 "scenario.c"
 796  return;
 797}
 798}
 799#line 1 "wsllib_check.o"
 800#pragma merger(0,"wsllib_check.i","")
 801#line 3 "wsllib_check.c"
 802void __automaton_fail(void) 
 803{ 
 804
 805  {
 806  goto ERROR;
 807  ERROR: ;
 808#line 53 "wsllib_check.c"
 809  return;
 810}
 811}
 812#line 1 "libacc.o"
 813#pragma merger(0,"libacc.i","")
 814#line 73 "/usr/include/assert.h"
 815extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 816                                                                      char const   *__file ,
 817                                                                      unsigned int __line ,
Show full sources
↑