Showing error 1682

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


Source:

 536#line 213
 537  setClientAddressBookAddress(bob, 0, rjh);
 538#line 214
 539  setClientAddressBookAddress(bob, 1, chuck);
 540  }
 541#line 1851 "Test.c"
 542  return;
 543}
 544}
 545#line 220 "Test.c"
 546void rjhEnableForwarding(void) 
 547{ 
 548
 549  {
 550  {
 551#line 221
 552  setClientForwardReceiver(rjh, chuck);
 553  }
 554#line 1871 "Test.c"
 555  return;
 556}
 557}
 558#line 1 "wsllib_check.o"
 559#pragma merger(0,"wsllib_check.i","")
 560#line 3 "wsllib_check.c"
 561void __automaton_fail(void) 
 562{ 
 563
 564  {
 565  goto ERROR;
 566  ERROR: ;
 567#line 53 "wsllib_check.c"
 568  return;
 569}
 570}
 571#line 1 "Client.o"
 572#pragma merger(0,"Client.i","")
 573#line 4 "ClientLib.h"
 574int initClient(void) ;
 575#line 14
 576int getClientAddressBookSize(int handle ) ;
Show full sources