|
Splint - Secure Programming Lint |
info@splint.org |
| Manual Contents - Other Formats | Section: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 A B C D E Sponsors - Credits |
3 Undefined Values
Like many static checkers, Splint detects instances where the value of a location is used before it is defined. This analysis is done at the procedural level. If there is a path through the procedure that uses a local variable before it is defined, a use before definition error is reported. The usedef flag controls use before definition checking.
Splint can do more checking than standard checkers though, because the annotations can be used to describe what storage must be defined and what storage may be undefined at interface points. Unannotated references are expected to be completely defined at interface points. This means all storage reachable from a global variable, parameter to a function, or function return value is defined before and after a function call.
3.1.1 Undefined Parameters
Sometimes, function parameters or return values are expected to reference undefined or partially defined storage. For example, a pointer parameter may be intended only as an address to store a result, or a memory allocator may return allocated but undefined storage. The out annotation denotes a pointer to storage that may be undefined.
Splint does not report an error when a pointer to allocated but undefined storage is passed as an out parameter. Within the body of a function, Splint will assume an out parameter is allocated but not necessarily bound to a value, so an error is reported if its value is used before it is defined.
Splint reports an error if storage reachable by the caller after the call is not defined when the function returns. This can be suppressed by -must-define. After a call returns, an actual parameter corresponding to an out parameter is assumed to be completely defined.
When checking unannotated programs, many spurious use before definition errors may be reported If impouts is on, no error is reported when an incompletely-defined parameter is passed to a formal parameter with no definition annotation, and the actual parameter is assumed to be defined after the call. The /*@in@*/ annotation can be used to denote a parameter that must be completely defined, even if imp-outs is on. If imp-outs is off, there is an implicit in annotation on every parameter with no definition annotation.
usedef.c
Running Splint
extern void
setVal (/*@out@*/ int *x);
extern int
getVal (/*@in@*/ int *x);
extern int mysteryVal
(int *x);
int dumbfunc
(/*@out@*/ int *x, int i)
{
if (i > 3)
11 return *x;
else if (i > 1)
13 return getVal (x);
else if (i == 0)
15 return mysteryVal (x);
else
{
18 setVal (x);
19 return *x;
}
}
> splint usedef.c
usedef.c:11: Value *x used before definition
usedef.c:13: Passed storage x not completely defined
(*x is undefined): getVal (x)
usedef.c:15: Passed storage x not completely defined
(*x is undefined): mysteryVal (x)
Finished checking --- 3 code warnings
No error is reported for line 18, since the incompletely defined storage x is passed as an out parameter. After the call, x may be dereferenced, since setVal is assumed to completely define its out parameter. The warning for line 15 would not appear if +impouts were used since there is no in annotation on the parameter to mysteryVal.
3.1.2 Relaxing Checking
The reldef annotation relaxes definition checking for a particular declaration. Storage declared with a reldef annotation is assumed to be defined when it is used, but no error is reported if it is not defined before it is returned or passed as a parameter.
It is up to the programmer to check reldef fields are used correctly. They should be avoided in most cases, but may be useful for fields of structures that may or may not be defined depending on other constraints.
3.1.3 Partially Defined Structures
The partial annotation can be used to relax checking of structure fields. A structure with undefined fields may be passed as a partial parameter or returned as a partial result. Inside a function body, no error is reported when the field of a partial structure is used. After a call, all fields of a structure that is passed as a partial parameter are assumed to be completely defined.
Next: 4. Types
Return to Contents