#2 /*@releases does not work as expected
-- Sorry for duplicate but the system forgot my login.
Hello,
does anybody know what I am doing wrong here:
extern void
C_String_Finalize (
// Buffer der gelöcht werden soll
/*@in@*/ C_String* Value )
/*@releases Value->Data @*/
/*@ensures Value->Data == 0 /\
Value->Size == 0 @*/;
I do call C_String_Finalize but still I get:
Source/tester-string.c:109:12: Only storage Text.Data (type char
*) derived from variable declared in this scope is not released
(memory leak)
A storage leak due to incomplete deallocation of a structure or
deep pointer is suspected. Unshared storage that is reachable
from a reference that is being deallocated has not yet been
deallocated. Splint assumes when an object is passed as an out
only
void pointer that the outer object will be deallocated, but the
inner objects will not.
Any Ideas?
Martin
Logged In: YES
user_id=572001
by the way:
I can not help in this case directly.
But are you sure that your code example is complete?
I am missing curly braces for the function definition.
Logged In: YES
user_id=697486
Hello,
This is an /*@external@*/ function - not even programmed in C.
Actualy, by now found the problem
And I would consider this a "documentation bug". In the documentation
there is a deveral places documenting the definition states /*@in@*/,
/*@out@*/, /*@partial@*/ and /*@reldev@*/. However non of this
places document the 5th definition state /*@special@*/.
Without /*@special@*/, splint silenty ignores /*@releases
Value->Data @*/.
With Regards
Martin
Please try the mailing list. http://www.splint.org/lists.html