Showing error 1817

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


Source:

 555#line 23
 556  if (in_encrypted) {
 557    {
 558#line 23
 559    tmp = isEncrypted(msg);
 560    }
 561#line 23
 562    if (tmp) {
 563
 564    } else {
 565      {
 566#line 24
 567      __automaton_fail();
 568      }
 569    }
 570  } else {
 571
 572  }
 573#line 24
 574  return;
 575}
 576}
 577#line 1 "wsllib_check.o"
 578#pragma merger(0,"wsllib_check.i","")
 579#line 3 "wsllib_check.c"
 580void __automaton_fail(void) 
 581{ 
 582
 583  {
 584  goto ERROR;
 585  ERROR: ;
 586#line 53 "wsllib_check.c"
 587  return;
 588}
 589}
 590#line 1 "Email.o"
 591#pragma merger(0,"Email.i","")
 592#line 6 "EmailLib.h"
 593int getEmailId(int handle ) ;
 594#line 10
 595int getEmailFrom(int handle ) ;
Show full sources