Showing error 1810

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


Source:

3447#line 227 "EmailLib.c"
3448void setEmailIsSignatureVerified(int handle , int value ) 
3449{ 
3450
3451  {
3452#line 233
3453  if (handle == 1) {
3454#line 229
3455    __ste_email_isSignatureVerified0 = value;
3456  } else {
3457#line 230
3458    if (handle == 2) {
3459#line 231
3460      __ste_email_isSignatureVerified1 = value;
3461    } else {
3462
3463    }
3464  }
3465#line 1511 "EmailLib.c"
3466  return;
3467}
3468}
3469#line 1 "wsllib_check.o"
3470#pragma merger(0,"wsllib_check.i","")
3471#line 3 "wsllib_check.c"
3472void __automaton_fail(void) 
3473{ 
3474
3475  {
3476  goto ERROR;
3477  ERROR: ;
3478#line 53 "wsllib_check.c"
3479  return;
3480}
3481}
3482#line 1 "EncryptAutoResponder_spec.o"
3483#pragma merger(0,"EncryptAutoResponder_spec.i","")
3484#line 7 "EncryptAutoResponder_spec.c"
3485int in_encrypted  =    0;
3486#line 11 "EncryptAutoResponder_spec.c"
3487__inline void __utac_acc__EncryptAutoResponder_spec__1(int msg ) 
Show full sources