Showing error 2056

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

Source: 

 375#line 12
 376      if (tmp___1) {
 377
 378      } else {
 379
 380      }
 381    }
 382    {
 383#line 13
 384    timeShift();
 385    }
 386  }
 387  while_0_break: /* CIL Label */ ;
 388  }
 389  {
 390#line 15
 391  cleanup();
 392  }
 393#line 74 "scenario.c"
 394  return;
 395}
 396}
 397#line 1 "wsllib_check.o"
 398#pragma merger(0,"wsllib_check.i","")
 399#line 3 "wsllib_check.c"
 400void __automaton_fail(void) 
 401{ 
 402
 403  {
 404  goto ERROR;
 405  ERROR: ;
 406#line 53 "wsllib_check.c"
 407  return;
 408}
 409}
 410#line 1 "libacc.o"
 411#pragma merger(0,"libacc.i","")
 412#line 73 "/usr/include/assert.h"
 413extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 414                                                                      char const   *__file ,
 415                                                                      unsigned int __line ,
Show full sources
↑