Showing error 1784

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


Source:

1956  if (handle == 1) {
1957#line 674
1958    __ste_client_idCounter0 = value;
1959  } else {
1960#line 675
1961    if (handle == 2) {
1962#line 676
1963      __ste_client_idCounter1 = value;
1964    } else {
1965#line 677
1966      if (handle == 3) {
1967#line 678
1968        __ste_client_idCounter2 = value;
1969      } else {
1970
1971      }
1972    }
1973  }
1974#line 2682 "ClientLib.c"
1975  return;
1976}
1977}
1978#line 1 "wsllib_check.o"
1979#pragma merger(0,"wsllib_check.i","")
1980#line 3 "wsllib_check.c"
1981void __automaton_fail(void) 
1982{ 
1983
1984  {
1985  goto ERROR;
1986  ERROR: ;
1987#line 53 "wsllib_check.c"
1988  return;
1989}
1990}
1991#line 1 "libacc.o"
1992#pragma merger(0,"libacc.i","")
1993#line 73 "/usr/include/assert.h"
1994extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
1995                                                                      char const   *__file ,
1996                                                                      unsigned int __line ,
Show full sources