Showing error 1716

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

Source: 

4059    {
4060#line 256
4061    tmp___3 = getEmailSignKey(msg);
4062#line 256
4063    tmp___4 = isKeyPairValid(tmp___3, pubkey);
4064    }
4065#line 256
4066    if (tmp___4) {
4067      {
4068#line 257
4069      setEmailIsSignatureVerified(msg, 1);
4070      }
4071    } else {
4072
4073    }
4074  } else {
4075
4076  }
4077#line 1512 "Client.c"
4078  return;
4079}
4080}
4081#line 1 "wsllib_check.o"
4082#pragma merger(0,"wsllib_check.i","")
4083#line 3 "wsllib_check.c"
4084void __automaton_fail(void) 
4085{ 
4086
4087  {
4088  goto ERROR;
4089  ERROR: ;
4090#line 53 "wsllib_check.c"
4091  return;
4092}
4093}
4094#line 1 "featureselect.o"
4095#pragma merger(0,"featureselect.i","")
4096#line 41 "featureselect.h"
4097int select_one(void) ;
4098#line 43
4099void select_features(void) ;
Show full sources
↑