LCLint Sample - Strict Library

Changes from Strict Checks

Differences

Fixed errors reported using strict mode checking.

Now, running LCLint in strict mode detects no anomalies.

Modules

   * employee - employee datatype (LCL, Code, Header)
   * empset - sets of employees (LCL, Code, Header)
   * dbase - database of employees (LCL, Code, Header)
   * eref - reference to an employee (LCL, Code, Header)
   * erc - collection of erefs (LCL, Code, Header)
   * ereftab - table of employees and erefs (LCL, Code, Header)

Strict Library

Now we check the code using +strictlib to select the stricter version of the
standard library.

LCLint reports 77 anomalies.

Ignored Return Values

Twenty-five messages report ignored return values for calls to printf and
fprint. The return value of printf is declared type int in the strict
library, but either int or void in the standard library (to avoid a torrent
of error messages for typical programs). The return value of the printf
function is the number of characters transmitted, or a negative value if an
error occurred. For each printf call, we should check the return value is
non-negative. We use the check function to do this. For a larger program, we
would want to write a wrapper function that calls printf and checks the
return value.

Use and Modification of standard I/O

The other 52 messages report uses and modifications of the standard steams,
stderr and stdout. In the standard library, these are declared using
/*@unchecked@*/, so no use or modification errors are reported (with normal
flag settings). In the strict library, type are declared using /*@checked@*;
so use and modification errors are reported.

Some of the modifications of stdout are for error messages. These should
really be sent to stderr instead, so we replace the printf calls at
eref.c:36, eref.c:46, eref.c:82, eref.c:90, erc.c:26, erc.c:78, and
erc.c:143 with calls to fprintf (stderr, ...). We add stderr to the modifies
clauses these functions. The test driver, main, is specified to modify
stdout and stderr.

These modifies clauses propagate to the calling functions, and 46 new
anomalies are detected. We add stderr to the modifies clauses of
empset_insertUnique, empset_disjointUnion, empset_union, empset_intersect,
empset_initMod, empset_create, empset_sprint, ereftab_create,
ereftab_insert, ereftab_initMod, erc_join, erc_initMod, db_initMod,
db_uncheckedHire, db_promote, and db_print.

These in turn propagate to two more functions: db_hire and empset_insert.
The modifies clause added to db_hire propagates to produce an error message
for db_addEmpls, and stderr is added to its modifies clause. This in turn
propagates to db_query. After adding the modifies clause to db_query, no
more anomalies are reported.

Now, it is clearly documented which functions may modify stderr.
