Showing error 1768

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


Source:

2210  return;
2211}
2212}
2213#line 210 "Test.c"
2214void bobSetAddressBook(void) 
2215{ 
2216
2217  {
2218  {
2219#line 211
2220  setClientAddressBookSize(bob, 1);
2221#line 212
2222  setClientAddressBookAlias(bob, 0, rjh);
2223#line 213
2224  setClientAddressBookAddress(bob, 0, rjh);
2225#line 214
2226  setClientAddressBookAddress(bob, 1, chuck);
2227  }
2228#line 1851 "Test.c"
2229  return;
2230}
2231}
2232#line 1 "wsllib_check.o"
2233#pragma merger(0,"wsllib_check.i","")
2234#line 3 "wsllib_check.c"
2235void __automaton_fail(void) 
2236{ 
2237
2238  {
2239  goto ERROR;
2240  ERROR: ;
2241#line 53 "wsllib_check.c"
2242  return;
2243}
2244}
2245#line 1 "Email.o"
2246#pragma merger(0,"Email.i","")
2247#line 6 "EmailLib.h"
2248int getEmailId(int handle ) ;
2249#line 10
2250int getEmailFrom(int handle ) ;
Show full sources