Showing error 1764

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

Source: 

 601    {
 602#line 180
 603    tmp___3 = getEmailSignKey(msg);
 604#line 180
 605    tmp___4 = isKeyPairValid(tmp___3, pubkey);
 606    }
 607#line 180
 608    if (tmp___4) {
 609      {
 610#line 181
 611      setEmailIsSignatureVerified(msg, 1);
 612      }
 613    } else {
 614
 615    }
 616  } else {
 617
 618  }
 619#line 1216 "Client.c"
 620  return;
 621}
 622}
 623#line 1 "wsllib_check.o"
 624#pragma merger(0,"wsllib_check.i","")
 625#line 3 "wsllib_check.c"
 626void __automaton_fail(void) 
 627{ 
 628
 629  {
 630  goto ERROR;
 631  ERROR: ;
 632#line 53 "wsllib_check.c"
 633  return;
 634}
 635}
 636#line 1 "Util.o"
 637#pragma merger(0,"Util.i","")
 638#line 1 "Util.h"
 639int prompt(char *msg ) ;
 640#line 9 "Util.c"
 641int prompt(char *msg )
Show full sources
↑