Showing error 1603

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

Source: 

 725    } else {
 726      {
 727#line 17
 728      tmp___1 = areDoorsOpen();
 729      }
 730#line 17
 731      if (tmp___1) {
 732        {
 733#line 15
 734        __automaton_fail();
 735        }
 736      } else {
 737
 738      }
 739    }
 740  } else {
 741
 742  }
 743#line 15
 744  return;
 745}
 746}
 747#line 1 "wsllib_check.o"
 748#pragma merger(0,"wsllib_check.i","")
 749#line 3 "wsllib_check.c"
 750void __automaton_fail(void) 
 751{ 
 752
 753  {
 754  goto ERROR;
 755  ERROR: ;
 756#line 53 "wsllib_check.c"
 757  return;
 758}
 759}
 760#line 1 "libacc.o"
 761#pragma merger(0,"libacc.i","")
 762#line 73 "/usr/include/assert.h"
 763extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 764                                                                      char const   *__file ,
 765                                                                      unsigned int __line ,
Show full sources
↑