Showing error 1823

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

Source: 

2379#line 252
2380  setClientAddressBookAddress(bob, 0, rjh);
2381#line 253
2382  setClientAddressBookAddress(bob, 1, chuck);
2383  }
2384#line 1938 "Test.c"
2385  return;
2386}
2387}
2388#line 259 "Test.c"
2389void rjhEnableForwarding(void) 
2390{ 
2391
2392  {
2393  {
2394#line 260
2395  setClientForwardReceiver(rjh, chuck);
2396  }
2397#line 1958 "Test.c"
2398  return;
2399}
2400}
2401#line 1 "wsllib_check.o"
2402#pragma merger(0,"wsllib_check.i","")
2403#line 3 "wsllib_check.c"
2404void __automaton_fail(void) 
2405{ 
2406
2407  {
2408  goto ERROR;
2409  ERROR: ;
2410#line 53 "wsllib_check.c"
2411  return;
2412}
2413}
2414#line 1 "libacc.o"
2415#pragma merger(0,"libacc.i","")
2416#line 73 "/usr/include/assert.h"
2417extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
2418                                                                      char const   *__file ,
2419                                                                      unsigned int __line ,
Show full sources
↑