Showing error 1903

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

Source: 

 486#line 12
 487        stopSystem();
 488        }
 489      } else {
 490
 491      }
 492    }
 493    {
 494#line 14
 495    timeShift();
 496    }
 497  }
 498  while_0_break: /* CIL Label */ ;
 499  }
 500  {
 501#line 16
 502  cleanup();
 503  }
 504#line 76 "scenario.c"
 505  return;
 506}
 507}
 508#line 1 "wsllib_check.o"
 509#pragma merger(0,"wsllib_check.i","")
 510#line 3 "wsllib_check.c"
 511void __automaton_fail(void) 
 512{ 
 513
 514  {
 515  goto ERROR;
 516  ERROR: ;
 517#line 53 "wsllib_check.c"
 518  return;
 519}
 520}
 521#line 1 "libacc.o"
 522#pragma merger(0,"libacc.i","")
 523#line 73 "/usr/include/assert.h"
 524extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 525                                                                      char const   *__file ,
 526                                                                      unsigned int __line ,
Show full sources
↑