Showing error 1639

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

Source: 

4298    if (expectedDirection == 1) {
4299      {
4300#line 40
4301      tmp = getCurrentHeading();
4302      }
4303#line 40
4304      if (tmp == 0) {
4305        {
4306#line 41
4307        __automaton_fail();
4308        }
4309      } else {
4310
4311      }
4312    } else {
4313
4314    }
4315  }
4316#line 41
4317  return;
4318}
4319}
4320#line 1 "wsllib_check.o"
4321#pragma merger(0,"wsllib_check.i","")
4322#line 3 "wsllib_check.c"
4323void __automaton_fail(void) 
4324{ 
4325
4326  {
4327  goto ERROR;
4328  ERROR: ;
4329#line 53 "wsllib_check.c"
4330  return;
4331}
4332}
4333#line 1 "libacc.o"
4334#pragma merger(0,"libacc.i","")
4335#line 73 "/usr/include/assert.h"
4336extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
4337                                                                      char const   *__file ,
4338                                                                      unsigned int __line ,
Show full sources
↑