Showing error 1726

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

Source: 

3379#line 227 "EmailLib.c"
3380void setEmailIsSignatureVerified(int handle , int value ) 
3381{ 
3382
3383  {
3384#line 233
3385  if (handle == 1) {
3386#line 229
3387    __ste_email_isSignatureVerified0 = value;
3388  } else {
3389#line 230
3390    if (handle == 2) {
3391#line 231
3392      __ste_email_isSignatureVerified1 = value;
3393    } else {
3394
3395    }
3396  }
3397#line 1511 "EmailLib.c"
3398  return;
3399}
3400}
3401#line 1 "wsllib_check.o"
3402#pragma merger(0,"wsllib_check.i","")
3403#line 3 "wsllib_check.c"
3404void __automaton_fail(void) 
3405{ 
3406
3407  {
3408  goto ERROR;
3409  ERROR: ;
3410#line 53 "wsllib_check.c"
3411  return;
3412}
3413}
3414#line 1 "libacc.o"
3415#pragma merger(0,"libacc.i","")
3416#line 73 "/usr/include/assert.h"
3417extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
3418                                                                      char const   *__file ,
3419                                                                      unsigned int __line ,
Show full sources
↑