Showing error 2119

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

Source: 

 371}
 372}
 373#line 70 "MinePump.c"
 374void stopSystem(void) 
 375{ 
 376
 377  {
 378#line 75
 379  if (pumpRunning) {
 380    {
 381#line 72
 382    deactivatePump();
 383    }
 384  } else {
 385
 386  }
 387#line 75
 388  systemActive = 0;
 389#line 351 "MinePump.c"
 390  return;
 391}
 392}
 393#line 1 "wsllib_check.o"
 394#pragma merger(0,"wsllib_check.i","")
 395#line 3 "wsllib_check.c"
 396void __automaton_fail(void) 
 397{ 
 398
 399  {
 400  goto ERROR;
 401  ERROR: ;
 402#line 53 "wsllib_check.c"
 403  return;
 404}
 405}
 406#line 1 "libacc.o"
 407#pragma merger(0,"libacc.i","")
 408#line 73 "/usr/include/assert.h"
 409extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 410                                                                      char const   *__file ,
 411                                                                      unsigned int __line ,
Show full sources
↑