Functions communicate with their calling environment through an interface. The caller communicates the values of actual parameters and global variables to the function, and the function communicates to the caller through the return value, global variables and storage reachable from the actual parameters. By keeping interfaces narrow (restricting the amount of information visible across a function interface), we can understand and implement functions independently.
A function prototype documents the interface to a function. It serves as a contract between the function and its caller. In early versions of C, the function “prototype” was very limited. It described the type returned by the function but nothing about its parameters. ANSI C (1989) provided function prototypes with the ability to add information on the number and types of parameter to a function. Splint provides the means to express much more about a function interface such as what global variable the function may use and what values visible to the caller it may modify.
The extra interface information places constraints on both how the function may be called and how it may be implemented. Splint reports places where these constraints are not satisfied. Typically, these indicate bugs in the code or errors in the interface documentation.
This section describes annotations that may be added to a function declaration to document what global variables the function implementation may use and what values visible to its caller it may modify.
The modifies clause lists what values visible to the caller may be modified by a function. Modifies clauses limit what values a function may modify, but they do not require that listed values are always modified. The declaration,
int f (int *p, int *q) /*@modifies *p@*/;
declares a function f that may modify the value pointed to by its first argument but may not modify the value of its second argument or any global state.
Splint checks that a function does not modify any caller-visible value not encompassed by its modifies clause and does modify all values listed in its modifies clause on some possible execution of the function. Figure 12 shows an example of modifies checking done by Splint.
|
Running Splint | |
|
void setx (int *x, int *y) /*@modifies *x@*/ { 4 *y = *x; }
void sety (int *x, int *y) /*@modifies *y@*/ { setx (y, x); } |
> splint modify.c +checks modify.c:4: Undocumented modification of *y: *y = *x modify.c:5: Suspect object listed in modifies of setx not modified: *x modify.c:1: Declaration of setx
There are
no errors
for sety– the call to
setxmodifies the value |
|
Figure 12. Modification |
A few special names are provided for describing function modifications that effect state not identifiable through parameters or global variables:
internalState
The function modifies some internal state (that is, the value of a static variable). Even though a client cannot access the internal state directly, it is important to know that something may be modified by the function call both for clear documentation and for checking undefined order of evaluation (Section 8.2) and side effect free parameters (Section 11.2.1).
fileSystem
The function modifies the file system. Any modification that may change the system state is considered a file system modification. All functions that modify an object of type pointer to FILE also modify the file system. In addition, functions that do not modify a FILE pointer but modify some state that is visible outside this process also modify the file system (e.g., rename). The flag mod-file-system controls reporting of undocumented file system modifications.
nothing
The function modifies nothing (i.e., it is side effect free).
The annotation, /*@*/ in a function declaration or definition (after the parameter list, before the semi-colon or function body) denotes a function that modifies nothing and does not use any global variables (see Section 7.2).
Splint is designed so programs with many functions that are declared without modifies clauses can be checked effectively. Unless modnomods is in on, no modification errors are reported checking a function declared with no modifies clause.
A function with no modifies clause is an unconstrained function since there are no documented constraints on what it may modify. When an unconstrained function is called, it is checked differently from a function declared with a modifies clause. To prevent spurious errors, no modification error is reported at the call site unless the mod-uncon flag is on. Flags control whether errors involving unconstrained functions are reported for other checks that depend on modifications (side effect free macro parameters (Section 11.2.1), undefined evaluation order (Section 8.2), and likely infinite loops (Section 8.3.1).)
Another aspect of a function’s interface, is the global variables it uses. A globals list in a function declaration lists external variables that may be used in the function body. Splint checks that global variables used in a procedure match those listed in its globals list. A global is used in a function if it appears in the body directly, or it is in the globals list of a function called in the body. Splint reports if a global that is used in a procedure is not listed in its globals list, and if a listed global is not used in the function implementation. Figure 13 shows an example function definition with a globals list and associated checking done by Splint.
|
globals.c |
Running Splint |
|
int glob1, glob2;
3 int f (void) /*@globals glob1;@*/ { 5 return glob2; } |
> splint globals.c +checks
globals.c:5: Undocumented use of global glob2 globals.c:3: Global glob1 listed but not used
|
|
Figure 13. Global Variables |
Whether on not an error is reported for a use of a global variable in a given function depends on the scope of the variable (file static or external), the checking annotation used in the variable declaration or the implicit annotation if no checking annotation is used, whether or not the function is declared with a globals list, and flag settings.
A global or file static variable declaration may be preceded by an annotation to indicate how the variable should be checked. In order of decreasing checks, the annotations are:
/*@checkedstrict@*/
Strictest checking. Undocumented uses and modifications of the variable are reported in all functions whether or not they have a globals list (unless check-strict-globs is off).
/*@checked@*/
Undocumented use of the variable is reported in a function with a globals list, but not in a function declared with no globals (unless glob-noglobs is on).
/*@checkmod@*/
Undocumented uses of the variable are not reported, but undocumented modifications are reported. (If mod-globs-nomods is on, errors are reported even in functions declared with no modifies clause or globals list.)
/*@unchecked@*/
No messages are reported for undocumented use or modification of this global variable.
If a variable has none of these annotations, an implicit annotation is determined by the flag settings.
Different flags control the implicit annotation for variables declared with global scope and variables declared with file scope (i.e., using the static storage qualifier). To set the implicit annotation for global variables declared in context (globs for external variables or statics for file static variable) to be annotation (checked, checkmod, checkedstrict) use imp<annotation> <context>. For example, +imp-checked-strict-statics makes the implicit checking on unqualified file static variables checkedstrict. See Appendix B for a complete list of globals checking flags.
Annotations can be used in the globals list of a function declaration to describe the states of global variables before and after the call. If a global is preceded by undef, it is assumed to be undefined before the call. Thus, no error is reported if the global is not defined when the function is called, but an error is reported if the global is used in the function body before it is defined. The killed annotation denotes a global variable that may be undefined when the call returns. For globals that contain dynamically allocated storage, a killed global variable is similar to an only parameter (Section 5.2). An error is reported if it contains the only reference to storage that is not released before the call returns. Figure 14 illustrated killed and undef globals.
|
annotglobs.c |
Running Splint |
|
int globnum;
struct { char *firstname, *lastname; int id; } globname;
void initialize (/*@only@*/ char *name) /*@globals undef globnum, undef globname @*/ { 13 globname.id = globnum; globname.lastname = name; 15}
void finalize (void) /*@globals killed globname@*/ { free (globname.lastname); 21 } |
> splint annotglobs.c
annotglobs.c:13: Undef global globnum used before definition annotglobs.c:15: Global storage globname contains 1 undefined field when call returns: firstname annotglobs.c:21: Only storage globname.firstname (type char *) derived from killed global is not released (memory leak) |
|
Figure 14. Annotated Globals Lists |
Splint checks that function declarations and definitions are consistent. The general rule is that the first declaration of a function implies all later declarations and definitions. If a function is declared in a header file, the first declaration processed is its first declaration (if it is declared in more than one header file an error is reported if redecl is set) . Otherwise, the first declaration in the file defining the function is its first declaration.
Later declarations may not include variables in the globals list that were not included in the first declaration. The exception to this is when the first declaration is in a header file and the later declaration or definition includes file static variables. Since these are not visible in the header file, they can not be included in the header file declaration. Similarly, the modifies clause of a later declaration may not include objects that are not modifiable in the first declaration. The later declaration may be more specific. For example, if the header declaration is:
extern void setName (employee e, char *s) /*@modifies e@*/;
the later declaration could be,
void setName (employee e, char *) /*@modifies e->name@*/;
If employee is an abstract type, the declaration in the header should not refer to a particular implementation (i.e., it shouldn’t rely on there being a name field), but the implementation declaration can be more specific.
This rule also applies to file static variables. The header declaration for a function that modifies a file static variable should use modifies internalState since file static variables are not visible to clients. The implementation declaration should list the actual file static variables that may be modified.
Sometimes it is necessary to specify function interfaces at a lower level than is possible with the standard annotations. For example, if a function defines some fields of a returned structure but does not define all the fields. The /*@special@*/ annotation is used to mark a parameter, global variable, or return value that is described using state clauses.
State clauses may be used to constrain the state of a parameter or return value before or after a call. One or more state clauses may appear in a function declaration, before the modifies or globals clauses. State clauses may be listed in any order, but the same state clause should not be used more than once. In a state clause list, result is used to refer to the return value of the function.
The following state clauses are used to describe the definition state or parameters before and after the function is called and the return value after the function returns:
/*@uses <references>@*/
References in a uses clause must be completely defined before the function is called. They are assumed to be defined at function entrance when the function is checked.
/*@sets <references>@*/
References in a sets clause must be allocated before the function is called. They are completely defined after the function returns. They are assumed to be allocated but undefined storage at function entrance and an error is reported if there is a path on which they are not defined before the function returns.
/*@defines <references>@*/
References in a defines clause must not refer to unshared, allocated storage before the function is called. They are completely defined after the function returns. When the function is checked, they are assumed to be undefined at function entrance and an error is reported if there is a path on which they are not defined before the function returns.
/*@allocates <references>@*/
References in an allocates clause must be unallocated before the function is called. They are allocated but not necessarily defined after the function returns. An error is reported if there is a path through the function on which they are not allocated before the function returns.
/*@releases <references>@*/
References in the releases clause are deallocated by the function. They must be storage that could be passed as an only parameter before the function is called, and are dead pointers after the function returns. They are assumed to be defined at function entrance and an error is reported if they refer to live, allocated storage at any return point.
Some examples of state clauses are shown in Figure 15. The defines clause for record_new indicates that the id field of the structure pointed to by the result is defined, but the name field is not. So, record_create needs to call record_setName to define the name field. Similarly, the releases clause for record_clearName indicates that no storage is associated with the name field of its parameter after the return, so no failure to deallocate storage message is produced for the call to free in record_free. The ensures isnull clause is described in the next section.
|
clauses.c |
|
typedef struct { int id; /*@only@*/ char *name; } *record;
static /*@special@*/ record record_new (void) /*@defines result->id@*/ { record r = (record) malloc (sizeof (*r));
assert (r != NULL); r->id = 3; return r; }
static void record_setName (/*@special@*/ record r, /*@only@*/ char *name) /*@defines r->name@*/ { r->name = name; }
record record_create (/*@only@*/ char *name) { record r = record_new (); record_setName (r, name); return r; }
void record_clearName (/*@special@*/ record r) /*@releases r->name@*/ /*@ensures isnull r->name@*/ { free (r->name); r->name = NULL; }
void record_free (/*@only@*/ record r) { record_clearName (r); free (r); }
|
|
Figure 15. State Clauses |
More general assumptions about state of parameters and globals before and after a function is called can be described using requires and ensures clauses. A requires clause specifies a predicate that must be true at a call site; when checking a function implementation Splint assumes the constraints given in its requires clauses are true at function entry. An ensures clause specifies a predicate that is true at a call site after the call returns; when checking a function implementation Splint warns if there is an execution path that does not return with a state that satifies the constraints given in its ensures clauses. A function declaration can have many requires and ensures clauses as long as their meanings are not contradictory.
The following constraints can be stated using requires and ensures clauses:
/*@requires only<references>@*/; /*@ensures only<references>@*/
/*@requires shared<references>@*/; /*@ensures shared<references>@*/
/*@requires owned<references>@*/; /*@ensures owned<references>@*/
/*@requires dependent<references>@*/; /*@ensures dependent<references>@*/
References refer to only, shared, owned or dependent storage before (requires) or after (ensures) the call.
/*@requires observer<references>@*/; /*@ensures observer<references>@*/
/*@requires exposed<references>@*/; /*@ensures exposed <references>@*/
References refer to observer or exposed storage before (requires) or after (ensures) the call.
/*@requires isnull<references>@*/; /*@ensures isnull<references>@*/
References have the value NULL before (requires) or after (ensures) the call. Note, this is not the same name or meaning as the null annotation (which means the value may or may not be NULL.)
/*@requires notnull<references>@*/; /*@ensures notnull<references>@*/
References do not have the value NULL before (requires) or after (ensures) the call.
Next: 8. Control Flow
Return to Contents