Showing error 1742

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


Source:

 588    {
 589#line 167
 590    tmp___3 = getEmailSignKey(msg);
 591#line 167
 592    tmp___4 = isKeyPairValid(tmp___3, pubkey);
 593    }
 594#line 167
 595    if (tmp___4) {
 596      {
 597#line 168
 598      setEmailIsSignatureVerified(msg, 1);
 599      }
 600    } else {
 601
 602    }
 603  } else {
 604
 605  }
 606#line 1213 "Client.c"
 607  return;
 608}
 609}
 610#line 1 "wsllib_check.o"
 611#pragma merger(0,"wsllib_check.i","")
 612#line 3 "wsllib_check.c"
 613void __automaton_fail(void) 
 614{ 
 615
 616  {
 617  goto ERROR;
 618  ERROR: ;
 619#line 53 "wsllib_check.c"
 620  return;
 621}
 622}
 623#line 1 "SignVerify_spec.o"
 624#pragma merger(0,"SignVerify_spec.i","")
 625#line 9 "SignVerify_spec.c"
 626int sent_signed  =    -1;
 627#line 13 "SignVerify_spec.c"
 628void __utac_acc__SignVerify_spec__1(int msg ) 
Show full sources