Guide Contents 1. Overview 2. Operation 3. Abstract Types	4. Function Interfaces 5. Memory Management 6. Sharing 7. Value Constraints	8. Macros 9. Naming Conventions 10. Other Checks Contact: lclint@cs.virginia.edu
This guide is preserved to maintain old links, but has been replaced by the Splint Manual.

4. Function Interfaces

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 (i.e., 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. The main improvement provided by ANSI C was the ability to add information on the number and types of parameter to a function. LCLint provides the means to express much more about a function interface: what global variable the function may use, what values visible to the caller it may modify, if a pointer parameter may be a null pointer or point to undefined storage, if storage pointed to by a parameter is deallocated before the function returns, if the function may create new aliases to a parameter, can the caller modify or deallocate the return value, etc.

The extra interface information places constraints on both how the function may be called and how it may be implemented. LCLint reports places where these constrains are not satisfied. Typically, these indicate bugs in the code or errors in the interface documentation.

This section describes syntactic comments 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. Sections 5-7 describe annotations may be added to parameters to constrain valid arguments to a function and how these arguments may be used after the call and to the return value to constrain results.

4.1 Modifications

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.

LCLint 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 4 shows an example of modifies checking done by LCLint.

4.1.1 Special Modifications

A few special names are provided for describing function modifications:

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 10.1) and side-effect free parameters (Section 8.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 syntactic comment, /*@*/ 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 4.2).

Figure 4. Modifies checking.

4.1.2 Missing Modifies Clauses

LCLint 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 moduncon 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 8.2.1), undefined evaluation order (Section 10.1), and likely infinite loops (Section 10.2.1).)

4.1.3 Limitations

Determining whether a function modifies a particular parameter or global is in general an undecidable[9] problem. To enable useful checking, certain simplifying assumptions are necessary. LCLint assumes an object is modified when it appears on the left hand side of an assignment or it is passed to a function as a parameter which may be modified by that function (according to the called function's modifies clause). Hence, LCLint will report spurious modification errors for assignments that do not change the value of an object or modifications that are always reversed before a procedure returns. The /*@-mods@*/ and /*@=mods@*/ control comments can be used around these modifications to suppress the message.

4.2 Global Variables

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. LCLint 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. LCLint 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 5 shows an example function definition with a globals list and associated checking done by LCLint.

4.2.1 Controlling Globals Checking

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 checkstrictglobs 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 globnoglobs is on).

/*@checkmod@*/

Undocumented uses of the variable are not reported, but undocumented modifications are reported. (If modglobsnomods 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, +impcheckedstrictstatics makes the implicit checking on unqualified file static variables checkedstrict. (See Apppendix C, page 51, for a complete list of globals checking flags.)

4.3 Declaration Consistency

LCLint checks that function declarations and definitions are consistent. The general rule is that the first declaration of a function imply 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.

Next: Memory Management
Contents

This guide is preserved to maintain old links, but has been replaced by the Splint Manual.
	Guide Contents 1. Overview 2. Operation 3. Abstract Types	4. Function Interfaces 5. Memory Management 6. Sharing 7. Value Constraints	8. Macros 9. Naming Conventions 10. Other Checks Contact: lclint@cs.virginia.edu