Showing error 1678

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


Source:

 292#line 62 "Email.c"
 293int createEmail(int from , int to ) 
 294{ int retValue_acc ;
 295  int msg ;
 296
 297  {
 298  {
 299#line 63
 300  msg = 1;
 301#line 64
 302  setEmailFrom(msg, from);
 303#line 65
 304  setEmailTo(msg, to);
 305#line 797 "Email.c"
 306  retValue_acc = msg;
 307  }
 308#line 799
 309  return (retValue_acc);
 310#line 806
 311  return (retValue_acc);
 312}
 313}
 314#line 1 "wsllib_check.o"
 315#pragma merger(0,"wsllib_check.i","")
 316#line 3 "wsllib_check.c"
 317void __automaton_fail(void) 
 318{ 
 319
 320  {
 321  goto ERROR;
 322  ERROR: ;
 323#line 53 "wsllib_check.c"
 324  return;
 325}
 326}
 327#line 1 "libacc.o"
 328#pragma merger(0,"libacc.i","")
 329#line 73 "/usr/include/assert.h"
 330extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 331                                                                      char const   *__file ,
 332                                                                      unsigned int __line ,
Show full sources