Showing error 1688

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


Source:

1292#line 47 "Email.c"
1293int createEmail(int from , int to ) 
1294{ int retValue_acc ;
1295  int msg ;
1296
1297  {
1298  {
1299#line 48
1300  msg = 1;
1301#line 49
1302  setEmailFrom(msg, from);
1303#line 50
1304  setEmailTo(msg, to);
1305#line 751 "Email.c"
1306  retValue_acc = msg;
1307  }
1308#line 753
1309  return (retValue_acc);
1310#line 760
1311  return (retValue_acc);
1312}
1313}
1314#line 1 "wsllib_check.o"
1315#pragma merger(0,"wsllib_check.i","")
1316#line 3 "wsllib_check.c"
1317void __automaton_fail(void) 
1318{ 
1319
1320  {
1321  goto ERROR;
1322  ERROR: ;
1323#line 53 "wsllib_check.c"
1324  return;
1325}
1326}
1327#line 1 "Test.o"
1328#pragma merger(0,"Test.i","")
1329#line 16 "ClientLib.h"
1330void setClientAddressBookSize(int handle , int value ) ;
1331#line 22
1332void setClientAddressBookAlias(int handle , int index , int value ) ;
Show full sources