Showing error 1830

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

Source: 

3651  {
3652  {
3653#line 205
3654  setClientAutoResponse(rjh, 1);
3655  }
3656#line 1821 "Test.c"
3657  return;
3658}
3659}
3660#line 211 "Test.c"
3661void rjhEnableForwarding(void) 
3662{ 
3663
3664  {
3665  {
3666#line 212
3667  setClientForwardReceiver(rjh, chuck);
3668  }
3669#line 1841 "Test.c"
3670  return;
3671}
3672}
3673#line 1 "wsllib_check.o"
3674#pragma merger(0,"wsllib_check.i","")
3675#line 3 "wsllib_check.c"
3676void __automaton_fail(void) 
3677{ 
3678
3679  {
3680  goto ERROR;
3681  ERROR: ;
3682#line 53 "wsllib_check.c"
3683  return;
3684}
3685}
3686#line 1 "libacc.o"
3687#pragma merger(0,"libacc.i","")
3688#line 73 "/usr/include/assert.h"
3689extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
3690                                                                      char const   *__file ,
3691                                                                      unsigned int __line ,
Show full sources
↑