Showing error 1674

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


Source:

1771#line 44 "Email.c"
1772int createEmail(int from , int to ) 
1773{ int retValue_acc ;
1774  int msg ;
1775
1776  {
1777  {
1778#line 45
1779  msg = 1;
1780#line 46
1781  setEmailFrom(msg, from);
1782#line 47
1783  setEmailTo(msg, to);
1784#line 735 "Email.c"
1785  retValue_acc = msg;
1786  }
1787#line 737
1788  return (retValue_acc);
1789#line 744
1790  return (retValue_acc);
1791}
1792}
1793#line 1 "wsllib_check.o"
1794#pragma merger(0,"wsllib_check.i","")
1795#line 3 "wsllib_check.c"
1796void __automaton_fail(void) 
1797{ 
1798
1799  {
1800  goto ERROR;
1801  ERROR: ;
1802#line 53 "wsllib_check.c"
1803  return;
1804}
1805}
1806#line 1 "Test.o"
1807#pragma merger(0,"Test.i","")
1808#line 16 "ClientLib.h"
1809void setClientAddressBookSize(int handle , int value ) ;
1810#line 22
1811void setClientAddressBookAlias(int handle , int index , int value ) ;
Show full sources