Showing error 1749

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


Source:

 267#line 62 "Email.c"
 268int createEmail(int from , int to ) 
 269{ int retValue_acc ;
 270  int msg ;
 271
 272  {
 273  {
 274#line 63
 275  msg = 1;
 276#line 64
 277  setEmailFrom(msg, from);
 278#line 65
 279  setEmailTo(msg, to);
 280#line 797 "Email.c"
 281  retValue_acc = msg;
 282  }
 283#line 799
 284  return (retValue_acc);
 285#line 806
 286  return (retValue_acc);
 287}
 288}
 289#line 1 "wsllib_check.o"
 290#pragma merger(0,"wsllib_check.i","")
 291#line 3 "wsllib_check.c"
 292void __automaton_fail(void) 
 293{ 
 294
 295  {
 296  goto ERROR;
 297  ERROR: ;
 298#line 53 "wsllib_check.c"
 299  return;
 300}
 301}
 302#line 1 "EmailLib.o"
 303#pragma merger(0,"EmailLib.i","")
 304#line 4 "EmailLib.h"
 305int initEmail(void) ;
 306#line 8
 307void setEmailId(int handle , int value ) ;
Show full sources