8              Control Flow

The section describes checking done by Splint related to control flow.  Many of these checks are significantly improved because of the extra information that is known about the program when annotations are provided.

8.1            Execution

To detect certain errors and avoid spurious errors, it is important to know something about the control flow behavior of called functions. Without additional information, Splint assumes that all functions eventually return and execution continues normally at the call site. 

The noreturn annotation is used to denote a function that never returns [8].  For example,

extern /*@noreturn@*/ void fatalerror (/*@observer@*/ char *s);

declares fatalerror to never return.  This enables Splint to correctly analyze code like,

   if (x == NULL) fatalerror ("Yikes!");

   *x = 3;

Other functions may return, but sometimes (or usually) return normally.  The maynotreturn annotation denotes a function that may or may not return.  This may be useful for documentation, but does not help checking much, since Splint must assume that a function declared with maynotreturn returns normally when checking the code.  The alwaysreturns annotation denotes a function that always returns (but Splint does no checking to verify this).

To describe non-returning functions more precisely, the noreturnwhentrue and noreturnwhenfalse annotations may be used.  Similar to nullwhentrue and falsewhennull (see Section 2.1.1), noreturnwhentrue and noreturnwhenfalse mean that a function never returns if the value of its first argument is true (noreturnwhentrue) or false (noreturnwhenfalse).  They may be used only on functions whose first argument is a Boolean.  

Hence, a function declared with noreturnwhenwfalse must not return if the value of its argument is false.  For example, the standard library declares assert as[9]:

/*@noreturnwhenfalse@*/ void

assert (/*@sef@*/ bool /*@alt int@*/ pred);

This way, code like,

   assert (x != NULL);

   *x = 3;

is checked without reporting a false warning, since the noreturnwhenwfalse annotation on assert means the deference of x is not reached is x != NULL is false.

8.2            Undefined Behavior

The order in which side effects take place in a C program is not entirely defined by the code.  Certain execution points are known as sequence points — a function call (after the arguments have been evaluated), the end of a full expression (an initializer, expression in an expression statement, the control expression of an if, switch, while or do statement, each expression of a for statement, and the expression in a return statement), and after the first operand or a &&, ||, ? or , operand.

All side effects before a sequence point must be complete before the sequence point, and no evaluations after the sequence point shall have taken place.  Between sequence points, side effects and evaluations may take place in any order.  Hence, the order in which expressions or arguments are evaluated is not specified.  Compilers are free to evaluate function arguments and parts of expressions (that do not contain sequence points) in any order.  The behavior of code is undefined if it uses a value that is modified by another expression that is not required to be evaluated before or after the other use.

Splint detects instances where undetermined order of evaluation produces undefined behavior.  If modifies clauses and globals lists are used, this checking is enabled in expressions involving function calls. Evaluation order checking is controlled by the eval-order flag.

When checking systems without modifies and globals information (see Section 7), evaluation order checking may report errors when unconstrained functions are called in procedure arguments.  Since Splint has no annotations to constrain what these functions may modify, it cannot be guaranteed that the evaluation order is defined if another argument calls an unconstrained function or uses a global variable or storage reachable from a parameter to the unconstrained function.  Its best to add modifies and globals clauses to constrain the unconstrained functions in ways that eliminate the possibility of undefined behavior.  For large legacy systems, this may require too much effort.  Instead, the ‑eval-order-uncon flag may be used to prevent reporting of undefined behavior due to the order of evaluation of unconstrained functions.  Figure 16 illustrates detection of undefined behavior.

8.3            Problematic Control Structures

A number of control structures that are syntactically legal may indicate likely bugs in programs.  Splint can detect errors involving likely infinite loops (Section 8.3.1), fall through cases and missing cases in switch statements (Section 8.3.2), break statements within deeply nested loops or switches (Section 8.3.3), clauses of if, while or for statements that are empty statements or unblocked single statements (Section 8.3.4) and incomplete if-else logic (Section 8.3.5).  Although any of these may appear in a correct program, depending on the programming style used they may indicate likely bugs or style violations that should be detected and eliminated.

8.3.1        Likely Infinite Loops

Splint reports an error if it detects a loop that appears to be infinite.  An error is reported for a loop that does not modify any value used in its condition test inside the body of the loop or in the condition test itself.  This checking is enhanced by modifies clauses and globals lists (see Section 7) since they provide more information about what global variable may be used in the condition test and what values may be modified by function calls in the loop body.

Figure 17 shows examples of infinite loops detected by Splint. An error is reported for the loop in line 14, since neither of the values used in the loop condition (x directly and glob1 through the call to f) is modified by the body of the loop.  If the declaration of g is changed to include glob1 in the modifies clause no error is reported.  (In this example, if we assume the annotations are correct, then the programmer has probably called the wrong function in the loop body.  This isn’t surprising, given the horrible choices of function and variable names!)

If an unconstrained function is called within the loop body, Splint will assume that it modifies a value used in the condition test and not report an infinite loop error, unless infloopsuncon is on.  If infloopsuncon is on, Splint will report infinite loop errors for loops where there is no explicit modification of a value used in the condition test, but where they may be an undetected modification through a call to an unconstrained function (e.g., line 12 in Figure 17).

8.3.2        Switches

The automatic fall through of C switch statements is almost never the intended behavior.[10]  Splint detects case statements with code that may fall through to the next case.  The casebreak flag controls reporting of fall through cases.  A single fall through case may be marked by preceding the case keyword with /*@fallthrough@*/ to indicate explicitly that execution falls through to this case.  See Figure 18 for an example.

For switches on enum types, Splint reports an error if a member of the enumerator does not appear as a case in the switch body (and there is no default case).  (Controlled by misscase.)

8.3.3        Deep Breaks

There is no syntax provided by C (other than goto) for breaking out of a nested loop.  All break and continue statements act only on the innermost surrounding loop or switch.  This can lead to serious problems[11] when a programmer intends to break the outer loop or switch instead.  Splint optionally reports warnings for break and continue statements in nested contexts.

Four types of break warnings are reported:

·      break inside a loop (while or for) that is inside a loop.  Controlled by looploopbreak.  To indicate that a break is inside an inner loop, precede the break by /*@innerbreak@*/.

·      break inside a loop that is inside a switch statement.  Controlled by switchloopbreak.  To mark the break as a loop break, precede the break by /*@loopbreak@*/.

·      break inside a switch statement that is inside a loop.  Controlled by loopswitchbreak.  To mark the break as a switch break, precede the break by /*@switchbreak@*/.

·      break inside a switch inside another switch.  Controlled by switchswitchbreak.  To indicate that the break is for the inner switch, use /*@innerbreak@*/.

Since continue only makes sense within loops, a warning (Controlled by looploopcontinue.) is reported only for continue statements within nested loops.  A safe inner continue may be preceded by /*@innercontinue@*/ to suppress error messages locally. The deepbreak flag sets all nested break and continue checking flags.

Splint warns if the marker preceding a break is not consistent with its placement.  A warning results if innerbreak precedes a break that is not breaking an inner loop, switchbreak precedes a break that is not breaking a switch, or loopbreak precedes a break that is not breaking a loop.

8.3.4        Loop and If Bodies

An empty statement after an if, while or for often indicates a potential bug.  A single statement (i.e., not a compound block) after an if, while or for is not likely to indicate a bug, but make the code harder to read and edit.  Splint can report errors for if or loop statements with empty bodies or bodies that are not compound statements.  Separate flags control checking for statements following an if, while or for:

·      [if,while, for]empty — report errors for empty bodies (e.g., if (x > 3) ; )

·      [if,while, for]block — report errors for non-block bodies (e.g., if (x > 3) x++;)

The if statement checks also apply to the body of the else clause.  No ifblock warning is reported if the body of the else clause is an if statement, to allow conventional else if chains. 

8.3.5        Complete Logic

Although it may be perfectly reasonable in many contexts, an if-else chain with no final else may indicate missing logic or forgetting to check error cases.  If elseif-complete is on, Splint warns when an if statement that is the body of an else clause does not have a matching else clause.  For example, the code,

   if (x == 0) { return "nil"; }

   else if (x == 1) { return "many"; }

results in a warning since the second if has no matching else branch.

8.4            Suspicious Statements

Splint detects errors involving statements with no apparent effects (Section 8.4.1) and statements that ignore the result of a called function (Section 8.4.2).

8.4.1        Statements with No Effects

Splint can report errors for statements that have no effect.  (Controlled by no-effect.)   Because of modifies clauses, Splint can detect more errors than traditional checkers.  Unless the no-effect-uncon flag is on, errors are not reported for statements that involve calls to unconstrained functions since the unconstrained function may cause a modification.  Figure 19 shows examples of Splint’s no effect checking.

8.4.2        Ignored Return Values

Splint reports an error when a return value is ignored.  Checking may be controlled based on the type of the return value: ret-val-int controls reporting of ignored return values of type int, and ret-val-bool for return values of type bool, and ret-val-others for all other types.  A function statement may be cast to void to prevent this error from being reported.

Alternate types (Section 4.4) can be used to declare functions that return values that may safely be ignored by declaring the result type to alternately be void.  Several functions in the standard library are specified to alternately return void to prevent ignored return value errors for standard library functions (e.g., strcpy) where the result may be safely ignored (see Section 14.1).  Figure 20 shows examples of ignored return value errors reported by Splint.

Next: 9. Buffer Sizes
Return to Contents