Showing error 1633

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

Source: 

1412          } else {
1413#line 1188
1414            if (person == 5) {
1415#line 1193
1416              retValue_acc = 3;
1417#line 1195
1418              return (retValue_acc);
1419            } else {
1420#line 1201 "Person.c"
1421              retValue_acc = 0;
1422#line 1203
1423              return (retValue_acc);
1424            }
1425          }
1426        }
1427      }
1428    }
1429  }
1430#line 1210 "Person.c"
1431  return (retValue_acc);
1432}
1433}
1434#line 1 "wsllib_check.o"
1435#pragma merger(0,"wsllib_check.i","")
1436#line 3 "wsllib_check.c"
1437void __automaton_fail(void) 
1438{ 
1439
1440  {
1441  goto ERROR;
1442  ERROR: ;
1443#line 53 "wsllib_check.c"
1444  return;
1445}
1446}
1447#line 1 "Elevator.o"
1448#pragma merger(0,"Elevator.i","")
1449#line 359 "/usr/include/stdio.h"
1450extern int printf(char const   * __restrict  __format  , ...) ;
1451#line 16 "Person.h"
1452void enterElevator(int p ) ;
Show full sources
↑