Showing error 2145

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

Source: 

 168}
 169#line 58 "Environment.c"
 170int isHighWaterSensorDry(void) 
 171{ int retValue_acc ;
 172
 173  {
 174#line 65 "Environment.c"
 175  if (waterLevel < 2) {
 176#line 243
 177    retValue_acc = 1;
 178#line 245
 179    return (retValue_acc);
 180  } else {
 181#line 251 "Environment.c"
 182    retValue_acc = 0;
 183#line 253
 184    return (retValue_acc);
 185  }
 186#line 260 "Environment.c"
 187  return (retValue_acc);
 188}
 189}
 190#line 1 "wsllib_check.o"
 191#pragma merger(0,"wsllib_check.i","")
 192#line 3 "wsllib_check.c"
 193void __automaton_fail(void) 
 194{ 
 195
 196  {
 197  goto ERROR;
 198  ERROR: ;
 199#line 53 "wsllib_check.c"
 200  return;
 201}
 202}
 203#line 1 "libacc.o"
 204#pragma merger(0,"libacc.i","")
 205#line 73 "/usr/include/assert.h"
 206extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 207                                                                      char const   *__file ,
 208                                                                      unsigned int __line ,
Show full sources
↑