Showing error 2069

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

Source: 

 719}
 720#line 58 "Environment.c"
 721int isHighWaterSensorDry(void) 
 722{ int retValue_acc ;
 723
 724  {
 725#line 65 "Environment.c"
 726  if (waterLevel < 2) {
 727#line 243
 728    retValue_acc = 1;
 729#line 245
 730    return (retValue_acc);
 731  } else {
 732#line 251 "Environment.c"
 733    retValue_acc = 0;
 734#line 253
 735    return (retValue_acc);
 736  }
 737#line 260 "Environment.c"
 738  return (retValue_acc);
 739}
 740}
 741#line 1 "wsllib_check.o"
 742#pragma merger(0,"wsllib_check.i","")
 743#line 3 "wsllib_check.c"
 744void __automaton_fail(void) 
 745{ 
 746
 747  {
 748  goto ERROR;
 749  ERROR: ;
 750#line 53 "wsllib_check.c"
 751  return;
 752}
 753}
 754#line 1 "libacc.o"
 755#pragma merger(0,"libacc.i","")
 756#line 73 "/usr/include/assert.h"
 757extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 758                                                                      char const   *__file ,
 759                                                                      unsigned int __line ,
Show full sources
↑