Showing error 1607

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

Source: 

4796    } else {
4797      {
4798#line 17
4799      tmp___1 = areDoorsOpen();
4800      }
4801#line 17
4802      if (tmp___1) {
4803        {
4804#line 15
4805        __automaton_fail();
4806        }
4807      } else {
4808
4809      }
4810    }
4811  } else {
4812
4813  }
4814#line 15
4815  return;
4816}
4817}
4818#line 1 "wsllib_check.o"
4819#pragma merger(0,"wsllib_check.i","")
4820#line 3 "wsllib_check.c"
4821void __automaton_fail(void) 
4822{ 
4823
4824  {
4825  goto ERROR;
4826  ERROR: ;
4827#line 53 "wsllib_check.c"
4828  return;
4829}
4830}
4831#line 1 "scenario.o"
4832#pragma merger(0,"scenario.i","")
4833#line 1 "scenario.c"
4834void test(void) 
4835{ 
4836
Show full sources
↑