Showing error 1736

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

Source: 

3551    tmp = getEmailFrom(msg);
3552#line 18
3553    tmp___0 = findPublicKey(client, tmp);
3554#line 18
3555    pubkey = tmp___0;
3556    }
3557#line 19
3558    if (pubkey == 0) {
3559      {
3560#line 20
3561      __automaton_fail();
3562      }
3563    } else {
3564
3565    }
3566  } else {
3567
3568  }
3569#line 20
3570  return;
3571}
3572}
3573#line 1 "wsllib_check.o"
3574#pragma merger(0,"wsllib_check.i","")
3575#line 3 "wsllib_check.c"
3576void __automaton_fail(void) 
3577{ 
3578
3579  {
3580  goto ERROR;
3581  ERROR: ;
3582#line 53 "wsllib_check.c"
3583  return;
3584}
3585}
3586#line 1 "libacc.o"
3587#pragma merger(0,"libacc.i","")
3588#line 73 "/usr/include/assert.h"
3589extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
3590                                                                      char const   *__file ,
3591                                                                      unsigned int __line ,
Show full sources
↑