Showing error 1602

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

Source: 

4757          } else {
4758#line 1188
4759            if (person == 5) {
4760#line 1193
4761              retValue_acc = 3;
4762#line 1195
4763              return (retValue_acc);
4764            } else {
4765#line 1201 "Person.c"
4766              retValue_acc = 0;
4767#line 1203
4768              return (retValue_acc);
4769            }
4770          }
4771        }
4772      }
4773    }
4774  }
4775#line 1210 "Person.c"
4776  return (retValue_acc);
4777}
4778}
4779#line 1 "wsllib_check.o"
4780#pragma merger(0,"wsllib_check.i","")
4781#line 3 "wsllib_check.c"
4782void __automaton_fail(void) 
4783{ 
4784
4785  {
4786  goto ERROR;
4787  ERROR: ;
4788#line 53 "wsllib_check.c"
4789  return;
4790}
4791}
Show full sources
↑