Showing error 1758

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

Source: 

4220    {
4221#line 164
4222    tmp___3 = getEmailSignKey(msg);
4223#line 164
4224    tmp___4 = isKeyPairValid(tmp___3, pubkey);
4225    }
4226#line 164
4227    if (tmp___4) {
4228      {
4229#line 165
4230      setEmailIsSignatureVerified(msg, 1);
4231      }
4232    } else {
4233
4234    }
4235  } else {
4236
4237  }
4238#line 1316 "Client.c"
4239  return;
4240}
4241}
4242#line 1 "wsllib_check.o"
4243#pragma merger(0,"wsllib_check.i","")
4244#line 3 "wsllib_check.c"
4245void __automaton_fail(void) 
4246{ 
4247
4248  {
4249  goto ERROR;
4250  ERROR: ;
4251#line 53 "wsllib_check.c"
4252  return;
4253}
4254}
4255#line 1 "Util.o"
4256#pragma merger(0,"Util.i","")
4257#line 1 "Util.h"
4258int prompt(char *msg ) ;
4259#line 9 "Util.c"
4260int prompt(char *msg )
Show full sources
↑