Showing error 1778

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

Source: 

3815#line 227 "EmailLib.c"
3816void setEmailIsSignatureVerified(int handle , int value ) 
3817{ 
3818
3819  {
3820#line 233
3821  if (handle == 1) {
3822#line 229
3823    __ste_email_isSignatureVerified0 = value;
3824  } else {
3825#line 230
3826    if (handle == 2) {
3827#line 231
3828      __ste_email_isSignatureVerified1 = value;
3829    } else {
3830
3831    }
3832  }
3833#line 1511 "EmailLib.c"
3834  return;
3835}
3836}
3837#line 1 "wsllib_check.o"
3838#pragma merger(0,"wsllib_check.i","")
3839#line 3 "wsllib_check.c"
3840void __automaton_fail(void) 
3841{ 
3842
3843  {
3844  goto ERROR;
3845  ERROR: ;
3846#line 53 "wsllib_check.c"
3847  return;
3848}
3849}
3850#line 1 "libacc.o"
3851#pragma merger(0,"libacc.i","")
3852#line 73 "/usr/include/assert.h"
3853extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
3854                                                                      char const   *__file ,
3855                                                                      unsigned int __line ,
Show full sources
↑