Showing error 1733

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

Source: 

4199    {
4200#line 203
4201    tmp___3 = getEmailSignKey(msg);
4202#line 203
4203    tmp___4 = isKeyPairValid(tmp___3, pubkey);
4204    }
4205#line 203
4206    if (tmp___4) {
4207      {
4208#line 204
4209      setEmailIsSignatureVerified(msg, 1);
4210      }
4211    } else {
4212
4213    }
4214  } else {
4215
4216  }
4217#line 1273 "Client.c"
4218  return;
4219}
4220}
4221#line 1 "wsllib_check.o"
4222#pragma merger(0,"wsllib_check.i","")
4223#line 3 "wsllib_check.c"
4224void __automaton_fail(void) 
4225{ 
4226
4227  {
4228  goto ERROR;
4229  ERROR: ;
4230#line 53 "wsllib_check.c"
4231  return;
4232}
4233}
4234#line 1 "Email.o"
4235#pragma merger(0,"Email.i","")
4236#line 15 "Email.h"
4237int cloneEmail(int msg ) ;
4238#line 9 "Email.c"
4239void printMail__wrappee__Keys(int msg )
Show full sources
↑