Showing error 1980

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

Source: 

 200  }
 201  {
 202#line 51
 203  printf(")");
 204  }
 205#line 189 "Environment.c"
 206  return;
 207}
 208}
 209#line 55 "Environment.c"
 210int getWaterLevel(void) 
 211{ int retValue_acc ;
 212
 213  {
 214#line 207 "Environment.c"
 215  retValue_acc = waterLevel;
 216#line 209
 217  return (retValue_acc);
 218#line 216
 219  return (retValue_acc);
 220}
 221}
 222#line 1 "wsllib_check.o"
 223#pragma merger(0,"wsllib_check.i","")
 224#line 3 "wsllib_check.c"
 225void __automaton_fail(void) 
 226{ 
 227
 228  {
 229  goto ERROR;
 230  ERROR: ;
 231#line 53 "wsllib_check.c"
 232  return;
 233}
 234}
 235#line 1 "libacc.o"
 236#pragma merger(0,"libacc.i","")
 237#line 73 "/usr/include/assert.h"
 238extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 239                                                                      char const   *__file ,
 240                                                                      unsigned int __line ,
Show full sources
↑