Showing error 1833

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

Source: 

4440  return;
4441}
4442}
4443#line 203 "Test.c"
4444void bobSetAddressBook(void) 
4445{ 
4446
4447  {
4448  {
4449#line 204
4450  setClientAddressBookSize(bob, 1);
4451#line 205
4452  setClientAddressBookAlias(bob, 0, rjh);
4453#line 206
4454  setClientAddressBookAddress(bob, 0, rjh);
4455#line 207
4456  setClientAddressBookAddress(bob, 1, chuck);
4457  }
4458#line 1827 "Test.c"
4459  return;
4460}
4461}
4462#line 1 "wsllib_check.o"
4463#pragma merger(0,"wsllib_check.i","")
4464#line 3 "wsllib_check.c"
4465void __automaton_fail(void) 
4466{ 
4467
4468  {
4469  goto ERROR;
4470  ERROR: ;
4471#line 53 "wsllib_check.c"
4472  return;
4473}
4474}
Show full sources
↑