Showing error 1693

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


Source:

2144  return;
2145}
2146}
2147#line 203 "Test.c"
2148void bobSetAddressBook(void) 
2149{ 
2150
2151  {
2152  {
2153#line 204
2154  setClientAddressBookSize(bob, 1);
2155#line 205
2156  setClientAddressBookAlias(bob, 0, rjh);
2157#line 206
2158  setClientAddressBookAddress(bob, 0, rjh);
2159#line 207
2160  setClientAddressBookAddress(bob, 1, chuck);
2161  }
2162#line 1827 "Test.c"
2163  return;
2164}
2165}
2166#line 1 "wsllib_check.o"
2167#pragma merger(0,"wsllib_check.i","")
2168#line 3 "wsllib_check.c"
2169void __automaton_fail(void) 
2170{ 
2171
2172  {
2173  goto ERROR;
2174  ERROR: ;
2175#line 53 "wsllib_check.c"
2176  return;
2177}
2178}
2179#line 1 "ClientLib.o"
2180#pragma merger(0,"ClientLib.i","")
2181#line 4 "ClientLib.h"
2182int initClient(void) ;
2183#line 6
2184char *getClientName(int handle ) ;
Show full sources