Showing error 1838

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


Source:

 421#line 23
 422  if (in_encrypted) {
 423    {
 424#line 23
 425    tmp = isEncrypted(msg);
 426    }
 427#line 23
 428    if (tmp) {
 429
 430    } else {
 431      {
 432#line 24
 433      __automaton_fail();
 434      }
 435    }
 436  } else {
 437
 438  }
 439#line 24
 440  return;
 441}
 442}
 443#line 1 "wsllib_check.o"
 444#pragma merger(0,"wsllib_check.i","")
 445#line 3 "wsllib_check.c"
 446void __automaton_fail(void) 
 447{ 
 448
 449  {
 450  goto ERROR;
 451  ERROR: ;
 452#line 53 "wsllib_check.c"
 453  return;
 454}
 455}
 456#line 1 "Email.o"
 457#pragma merger(0,"Email.i","")
 458#line 6 "EmailLib.h"
 459int getEmailId(int handle ) ;
 460#line 10
 461int getEmailFrom(int handle ) ;
Show full sources