Showing error 1706

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_spec11_product18_safe.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    {
3816#line 164
3817    tmp___3 = getEmailSignKey(msg);
3818#line 164
3819    tmp___4 = isKeyPairValid(tmp___3, pubkey);
3820    }
3821#line 164
3822    if (tmp___4) {
3823      {
3824#line 165
3825      setEmailIsSignatureVerified(msg, 1);
3826      }
3827    } else {
3828
3829    }
3830  } else {
3831
3832  }
3833#line 1316 "Client.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 "DecryptAutoResponder_spec.o"
3851#pragma merger(0,"DecryptAutoResponder_spec.i","")
3852#line 11 "DecryptAutoResponder_spec.c"
3853void __utac_acc__DecryptAutoResponder_spec__1(int client , int msg ) 
3854{ int tmp ;
3855
Show full sources
↑