Download LCLint User's Guide

18
LCLint User’s Guide
The basic memory allocator, malloc, is declared:14
/*@only@*/ void *malloc (size_t size);
It returns an object that is referenced only by the function return value.
The deallocator, free, is declared:15
void free (/*@only@*/ void *ptr);
The parameter to free must reference an unshared object. Since the parameter is declared using
only, the caller may not use the referenced object after the call, and may not pass in a reference to a
shared object. There is nothing special about malloc and free — their behavior can be described
entirely in terms of the provided annotations.
only.c
1
extern /*@only@*/ int *glob;
/*@only@*/ int *
f (/*@only@*/ int *x, int *y,
int *z)
/*@globals glob;@*/
{
8 int *m = (int *)
9
malloc (sizeof (int));
glob = y;
free (x);
13 *m = *x;
14 return z;
}
11
12
Memory leak
Use after free
Memory leak detected
Running LCLint
> lclint only.c
LCLint 2.4 --- 10 Apr 98
only.c:11: Only storage glob not released before
assignment: glob = y
only.c:1: Storage glob becomes only
only.c:11: Implicitly temp storage y assigned to only:
glob = y
only.c:13: Dereference of possibly null pointer m: *m
only.c:8: Storage m may become null
only.c:13: Variable x used after being released
only.c:12: Storage x released
only.c:14: Implicitly temp storage z returned as only: z
only.c:14: Fresh storage m not released before return
only.c:9: Fresh storage m allocated
Finished LCLint checking --- 6 code errors found
Figure 6. Deallocation errors.
5.2.2 Temporary Parameters
The temp annotation is used to declare a function parameter that is used temporarily by the function.
An error is reported if the function releases the storage associated with a temp formal parameter or
14
The full declaration of malloc also includes a null annotation (Section 7.2) to indicate that the
result may be NULL (as it is when the requested storage cannot be allocated) and an out annotation
(Section 7.1) to indicate that the result points to undefined storage.
15
The full declaration of free also has out and null annotations on the parameter to indicate that
the argument may be NULL and need not point to defined storage. According to [ANSI, 4.10.3.2],
NULL may be passed to free without an error. On some UNIX platforms, passing NULL to free causes
a program crash so the UNIX version of the standard library (Appendix F) specifies free without the
null annotation on its parameter. To check that allocated objects are completely destroyed (e.g., all
unshared objects inside a structure are deallocated before the structure is deallocated), LCLint checks
that any parameter passed as an out only void * does not contain references to live, unshared
objects. This makes sense, since such a parameter could not be used sensibly in any way other than
deallocating its storage.