Showing error 1667

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


Source:

 541  {
 542  {
 543#line 198
 544  generateKeyPair(rjh, 666);
 545  }
 546#line 1797 "Test.c"
 547  return;
 548}
 549}
 550#line 204 "Test.c"
 551void rjhEnableForwarding(void) 
 552{ 
 553
 554  {
 555  {
 556#line 205
 557  setClientForwardReceiver(rjh, chuck);
 558  }
 559#line 1817 "Test.c"
 560  return;
 561}
 562}
 563#line 1 "wsllib_check.o"
 564#pragma merger(0,"wsllib_check.i","")
 565#line 3 "wsllib_check.c"
 566void __automaton_fail(void) 
 567{ 
 568
 569  {
 570  goto ERROR;
 571  ERROR: ;
 572#line 53 "wsllib_check.c"
 573  return;
 574}
 575}
 576#line 1 "Email.o"
 577#pragma merger(0,"Email.i","")
 578#line 6 "EmailLib.h"
 579int getEmailId(int handle ) ;
 580#line 10
 581int getEmailFrom(int handle ) ;
Show full sources