Splint - Secure Programming Lint
Download - Documentation - Manual - Links Sponsors - Credits

Strict Library

Changes from Strict Checks


Fixed errors reported using strict mode checking.

Now, running LCLint in strict mode detects no anomalies.


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.

Next: Continue to Final
Return to Summary

Splint - Secure Programming Lint evans@virginia.edu
Download - Documentation - Manual - Links
Source - Linux - Publications - Talks
Reporting Bugs    Sponsors - Credits