Showing error 1835

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

Source: 

3768    {
3769#line 203
3770    tmp___3 = getEmailSignKey(msg);
3771#line 203
3772    tmp___4 = isKeyPairValid(tmp___3, pubkey);
3773    }
3774#line 203
3775    if (tmp___4) {
3776      {
3777#line 204
3778      setEmailIsSignatureVerified(msg, 1);
3779      }
3780    } else {
3781
3782    }
3783  } else {
3784
3785  }
3786#line 1281 "Client.c"
3787  return;
3788}
3789}
3790#line 1 "wsllib_check.o"
3791#pragma merger(0,"wsllib_check.i","")
3792#line 3 "wsllib_check.c"
3793void __automaton_fail(void) 
3794{ 
3795
3796  {
3797  goto ERROR;
3798  ERROR: ;
3799#line 53 "wsllib_check.c"
3800  return;
3801}
3802}
3803#line 1 "Test.o"
3804#pragma merger(0,"Test.i","")
3805#line 2 "Test.h"
3806int bob  ;
3807#line 5 "Test.h"
3808int rjh  ;
Show full sources
↑