Showing error 1744

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

Source: 

3732    {
3733#line 187
3734    tmp___3 = getEmailSignKey(msg);
3735#line 187
3736    tmp___4 = isKeyPairValid(tmp___3, pubkey);
3737    }
3738#line 187
3739    if (tmp___4) {
3740      {
3741#line 188
3742      setEmailIsSignatureVerified(msg, 1);
3743      }
3744    } else {
3745
3746    }
3747  } else {
3748
3749  }
3750#line 1382 "Client.c"
3751  return;
3752}
3753}
3754#line 1 "wsllib_check.o"
3755#pragma merger(0,"wsllib_check.i","")
3756#line 3 "wsllib_check.c"
3757void __automaton_fail(void) 
3758{ 
3759
3760  {
3761  goto ERROR;
3762  ERROR: ;
3763#line 53 "wsllib_check.c"
3764  return;
3765}
3766}
3767#line 1 "libacc.o"
3768#pragma merger(0,"libacc.i","")
3769#line 73 "/usr/include/assert.h"
3770extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
3771                                                                      char const   *__file ,
3772                                                                      unsigned int __line ,
Show full sources
↑