Showing error 1628

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


Source:

4478#line 20 "featureselect.c"
4479void select_helpers(void) 
4480{ 
4481
4482  {
4483#line 112 "featureselect.c"
4484  return;
4485}
4486}
4487#line 25 "featureselect.c"
4488int valid_product(void) 
4489{ int retValue_acc ;
4490
4491  {
4492#line 130 "featureselect.c"
4493  retValue_acc = 1;
4494#line 132
4495  return (retValue_acc);
4496#line 139
4497  return (retValue_acc);
4498}
4499}
4500#line 1 "wsllib_check.o"
4501#pragma merger(0,"wsllib_check.i","")
4502#line 3 "wsllib_check.c"
4503void __automaton_fail(void) 
4504{ 
4505
4506  {
4507  goto ERROR;
4508  ERROR: ;
4509#line 53 "wsllib_check.c"
4510  return;
4511}
4512}
4513#line 1 "libacc.o"
4514#pragma merger(0,"libacc.i","")
4515#line 73 "/usr/include/assert.h"
4516extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
4517                                                                      char const   *__file ,
4518                                                                      unsigned int __line ,
Show full sources