Showing error 1713

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


Source:

2219  {
2220  {
2221#line 198
2222  generateKeyPair(rjh, 666);
2223  }
2224#line 1801 "Test.c"
2225  return;
2226}
2227}
2228#line 204 "Test.c"
2229void rjhSetAutoRespond(void) 
2230{ 
2231
2232  {
2233  {
2234#line 205
2235  setClientAutoResponse(rjh, 1);
2236  }
2237#line 1821 "Test.c"
2238  return;
2239}
2240}
2241#line 1 "wsllib_check.o"
2242#pragma merger(0,"wsllib_check.i","")
2243#line 3 "wsllib_check.c"
2244void __automaton_fail(void) 
2245{ 
2246
2247  {
2248  goto ERROR;
2249  ERROR: ;
2250#line 53 "wsllib_check.c"
2251  return;
2252}
2253}
2254#line 1 "libacc.o"
2255#pragma merger(0,"libacc.i","")
2256#line 73 "/usr/include/assert.h"
2257extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
2258                                                                      char const   *__file ,
2259                                                                      unsigned int __line ,
Show full sources