Showing error 1623

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

Source: 

4754          {
4755#line 67
4756          __automaton_fail();
4757          }
4758        } else {
4759#line 68
4760          if (floorButtons_spc2_4) {
4761            {
4762#line 69
4763            __automaton_fail();
4764            }
4765          } else {
4766
4767          }
4768        }
4769      }
4770    }
4771  }
4772#line 69
4773  return;
4774}
4775}
4776#line 1 "wsllib_check.o"
4777#pragma merger(0,"wsllib_check.i","")
4778#line 3 "wsllib_check.c"
4779void __automaton_fail(void) 
4780{ 
4781
4782  {
4783  goto ERROR;
4784  ERROR: ;
4785#line 53 "wsllib_check.c"
4786  return;
4787}
4788}
4789#line 1 "UnitTests.o"
4790#pragma merger(0,"UnitTests.i","")
4791#line 24 "UnitTests.c"
4792void spec1(void) 
4793{ int tmp ;
4794  int tmp___0 ;
Show full sources
↑