Showing error 1910

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

Source: 

 678  }
 679  {
 680#line 51
 681  printf(")");
 682  }
 683#line 189 "Environment.c"
 684  return;
 685}
 686}
 687#line 55 "Environment.c"
 688int getWaterLevel(void) 
 689{ int retValue_acc ;
 690
 691  {
 692#line 207 "Environment.c"
 693  retValue_acc = waterLevel;
 694#line 209
 695  return (retValue_acc);
 696#line 216
 697  return (retValue_acc);
 698}
 699}
 700#line 1 "wsllib_check.o"
 701#pragma merger(0,"wsllib_check.i","")
 702#line 3 "wsllib_check.c"
 703void __automaton_fail(void) 
 704{ 
 705
 706  {
 707  goto ERROR;
 708  ERROR: ;
 709#line 53 "wsllib_check.c"
 710  return;
 711}
 712}
 713#line 1 "libacc.o"
 714#pragma merger(0,"libacc.i","")
 715#line 73 "/usr/include/assert.h"
 716extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 717                                                                      char const   *__file ,
 718                                                                      unsigned int __line ,
Show full sources
↑