Showing error 1689

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

Source: 

4309#line 206
4310  setClientAddressBookAddress(bob, 0, rjh);
4311#line 207
4312  setClientAddressBookAddress(bob, 1, chuck);
4313  }
4314#line 1827 "Test.c"
4315  return;
4316}
4317}
4318#line 213 "Test.c"
4319void rjhEnableForwarding(void) 
4320{ 
4321
4322  {
4323  {
4324#line 214
4325  setClientForwardReceiver(rjh, chuck);
4326  }
4327#line 1847 "Test.c"
4328  return;
4329}
4330}
4331#line 1 "wsllib_check.o"
4332#pragma merger(0,"wsllib_check.i","")
4333#line 3 "wsllib_check.c"
4334void __automaton_fail(void) 
4335{ 
4336
4337  {
4338  goto ERROR;
4339  ERROR: ;
4340#line 53 "wsllib_check.c"
4341  return;
4342}
4343}
Show full sources
↑