Showing error 1585

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


Source:

 210          } else {
 211#line 1188
 212            if (person == 5) {
 213#line 1193
 214              retValue_acc = 3;
 215#line 1195
 216              return (retValue_acc);
 217            } else {
 218#line 1201 "Person.c"
 219              retValue_acc = 0;
 220#line 1203
 221              return (retValue_acc);
 222            }
 223          }
 224        }
 225      }
 226    }
 227  }
 228#line 1210 "Person.c"
 229  return (retValue_acc);
 230}
 231}
 232#line 1 "wsllib_check.o"
 233#pragma merger(0,"wsllib_check.i","")
 234#line 3 "wsllib_check.c"
 235void __automaton_fail(void) 
 236{ 
 237
 238  {
 239  goto ERROR;
 240  ERROR: ;
 241#line 53 "wsllib_check.c"
 242  return;
 243}
 244}
 245#line 1 "Specification1_spec.o"
 246#pragma merger(0,"Specification1_spec.i","")
 247#line 38 "Elevator.h"
 248int areDoorsOpen(void) ;
 249#line 40
 250int getCurrentFloorID(void) ;
Show full sources