Showing error 1745

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

Source: 

4389#line 206
4390  setClientAddressBookAddress(bob, 0, rjh);
4391#line 207
4392  setClientAddressBookAddress(bob, 1, chuck);
4393  }
4394#line 1831 "Test.c"
4395  return;
4396}
4397}
4398#line 213 "Test.c"
4399void rjhEnableForwarding(void) 
4400{ 
4401
4402  {
4403  {
4404#line 214
4405  setClientForwardReceiver(rjh, chuck);
4406  }
4407#line 1851 "Test.c"
4408  return;
4409}
4410}
4411#line 1 "wsllib_check.o"
4412#pragma merger(0,"wsllib_check.i","")
4413#line 3 "wsllib_check.c"
4414void __automaton_fail(void) 
4415{ 
4416
4417  {
4418  goto ERROR;
4419  ERROR: ;
4420#line 53 "wsllib_check.c"
4421  return;
4422}
4423}
Show full sources
↑