Showing error 1696

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

Source: 

4486  return;
4487}
4488}
4489#line 210 "Test.c"
4490void bobSetAddressBook(void) 
4491{ 
4492
4493  {
4494  {
4495#line 211
4496  setClientAddressBookSize(bob, 1);
4497#line 212
4498  setClientAddressBookAlias(bob, 0, rjh);
4499#line 213
4500  setClientAddressBookAddress(bob, 0, rjh);
4501#line 214
4502  setClientAddressBookAddress(bob, 1, chuck);
4503  }
4504#line 1851 "Test.c"
4505  return;
4506}
4507}
4508#line 1 "wsllib_check.o"
4509#pragma merger(0,"wsllib_check.i","")
4510#line 3 "wsllib_check.c"
4511void __automaton_fail(void) 
4512{ 
4513
4514  {
4515  goto ERROR;
4516  ERROR: ;
4517#line 53 "wsllib_check.c"
4518  return;
4519}
4520}
Show full sources
↑