Thank you very much for your effort in making splint such a good
product.
I am in the process to check our code (about 300'000 LOC).
I have some very interesting results and I would really like to
integrate
splint in our development process.
For the higher level parts I have no problems, but the nearer I come to
the OS (vxWorks in our case) the more problems I have formulating the
correct conditions.
We have a own buffer management. I simplified it to pass it through
splint but
it still produces too many errors. I call splint like this:
splint.exe +stats +checks +posix-lib tst.c.
The file tst.c looks like this:
#include <stdlib.h>
typedef struct
{
/*@only@*/ /*@null@*/ char *buffer;
int buf_length;
} buf_t ;
/*@only@*/ /*@null@*/ static buf_t *alloc_buffer(int size)
{
buf_t *bufPtr;
bufPtr = malloc((size_t)size);
if (bufPtr == 0)
{
return 0;
}
bufPtr->buffer = malloc((size_t)size);
if (bufPtr == 0)
{
free(bufPtr);
return 0;
}
bufPtr->buf_length = size;
return bufPtr;
}
static void alloc_buffer2(/*@notnull@*/ buf_t *bufPtr, int size)
{
free(bufPtr->buffer);
bufPtr->buffer = malloc((size_t)size);
if (bufPtr == 0)
{
bufPtr->buf_length = 0;
return;
}
bufPtr->buf_length = size;
return;
}
static void free_buffer(/*@only *bufPtr->buffer@*/
/*@null *bufPtr->buffer@*/
buf_t *bufPtr)
/*@requires maxRead(*bufPtr->buffer) <=
*bufPtr->cfg_length@*/
{
if (bufPtr == NULL)
{
return;
}
free(bufPtr->buffer);
free(bufPtr);
}
static void free_buffer2(
/*@null *bufPtr->buffer@*/
/*@notnull bufPtr@*/ buf_t *bufPtr)
{
if (bufPtr == NULL)
{
return;
}
free(bufPtr->buffer);
}
static /*@only@*/ /*@null@*/ buf_t *my_global_buf_ptr;
static /*@only@*/ /*@null@*/ buf_t *my_global_buf_ptr2;
static void test_one( void )
{
free_buffer(my_global_buf_ptr);
my_global_buf_ptr = alloc_buffer(1024);
alloc_buffer2(my_global_buf_ptr2, 1024);
}
static void test_two( void )
{
free_buffer(my_global_buf_ptr);
free_buffer2(my_global_buf_ptr2);
}
int main(/*@unused@*/int argc, /*@unused@*/char *argv[])
{
test_one();
test_two();
return 0;
}
I get the following errors:
Splint 3.0.1.6 --- 11 Feb 2002
tst.c: (in function alloc_buffer)
tst.c(25,11): Returned storage *bufPtr contains 1 undefined field:
buffer
Storage derivable from a parameter, return value or global is not
defined.
Use /*@out@*/ to denote passed or returned storage which need not be
defined.
(Use -compdef to inhibit warning)
tst.c: (in function alloc_buffer2)
tst.c(35,14): Storage *bufPtr reachable from parameter contains 1
undefined
field: buffer
tst.c(38,11): Storage *bufPtr reachable from parameter contains 1
undefined
field: buffer
tst.c: (in function free_buffer2)
tst.c(64,2): Released storage bufPtr->buffer reachable from parameter
at return
point
Memory is used after it has been released (either by passing as an
only param
or assigning to an only global). (Use -usereleased to inhibit
warning)
tst.c(63,9): Storage bufPtr->buffer is released
tst.c: (in function test_one)
tst.c(74,18): Possibly null storage my_global_buf_ptr2 passed as
non-null
param: alloc_buffer2 (my_global_buf_ptr2, ...)
A possibly null pointer is passed as a parameter corresponding to a
formal
parameter with no /*@null@*/ annotation. If NULL may be used for
this
parameter, add a /*@null@*/ annotation to the function parameter
declaration.
(Use -nullpass to inhibit warning)
tst.c(67,37): Storage my_global_buf_ptr2 may become null
tst.c: (in function test_two)
tst.c(81,2): Function returns with global my_global_buf_ptr
referencing
released storage
A global variable does not satisfy its annotations when control is
transferred. (Use -globstate to inhibit warning)
tst.c(78,15): Storage my_global_buf_ptr is released
Finished checking --- 6 code warnings
89 source lines in 0.16 s.
Does anybody have a hint how I can get rid of these warnings or
why my code is wrong?
Regards
Niklaus Giger
Netstal Maschinen AG
CH-8752 Naefels
+41 55 618 64 68
E-Mail: [EMAIL PROTECTED]
