Showing error 1656

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

Source: 

4452  return (retValue_acc);
4453#line 1721
4454  return (retValue_acc);
4455}
4456}
4457#line 1 "scenario.o"
4458#pragma merger(0,"scenario.i","")
4459#line 1 "scenario.c"
4460void test(void) 
4461{ 
4462
4463  {
4464  {
4465#line 2
4466  bigMacCall();
4467#line 3
4468  cleanup();
4469  }
4470#line 53 "scenario.c"
4471  return;
4472}
4473}
4474#line 1 "wsllib_check.o"
4475#pragma merger(0,"wsllib_check.i","")
4476#line 3 "wsllib_check.c"
4477void __automaton_fail(void) 
4478{ 
4479
4480  {
4481  goto ERROR;
4482  ERROR: ;
4483#line 53 "wsllib_check.c"
4484  return;
4485}
4486}
4487#line 1 "Specification9_spec.o"
4488#pragma merger(0,"Specification9_spec.i","")
4489#line 7 "Specification9_spec.c"
4490int floorButtons_spc9_0  ;
4491#line 8 "Specification9_spec.c"
4492int floorButtons_spc9_1  ;
Show full sources
↑