Showing error 1841

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

Source: 

 620#line 17
 621  if (tmp) {
 622    {
 623#line 17
 624    tmp___0 = isPumpRunning();
 625    }
 626#line 17
 627    if (tmp___0) {
 628      {
 629#line 14
 630      __automaton_fail();
 631      }
 632    } else {
 633
 634    }
 635  } else {
 636
 637  }
 638#line 14
 639  return;
 640}
 641}
 642#line 1 "wsllib_check.o"
 643#pragma merger(0,"wsllib_check.i","")
 644#line 3 "wsllib_check.c"
 645void __automaton_fail(void) 
 646{ 
 647
 648  {
 649  goto ERROR;
 650  ERROR: ;
 651#line 53 "wsllib_check.c"
 652  return;
 653}
 654}
 655#line 1 "libacc.o"
 656#pragma merger(0,"libacc.i","")
 657#line 73 "/usr/include/assert.h"
 658extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 659                                                                      char const   *__file ,
 660                                                                      unsigned int __line ,
Show full sources
↑