Splint - Secure Programming Lint
info@splint.org
Download - Documentation - Manual - Links Reporting Bugs - Mailing Lists      Sponsors - Credits

Strict Checks

Changes from Naming Conventions

Differences

Replaced names to match selected naming convention.

Now, running LCLint in checks mode detects no anomalies.

Modules

Strict Checks

Now we check the code using strict mode. Strict mode turns on many checks not done in checks mode. Some of these checks are probably too severe for real programs.

Running with +strict reports 115 anomalies.

Empty/Block Bodies

Twenty-six messages report empty statements or unblocked bodies of loop and selection statements. We turn these statements into compound blocks by adding braces. It makes the code longer, but easier to read and edit.

Unspecified Exports

Nineteen anomalies report declarations that are exported but not specified.

Five of them concern type definitions:

eref.h:9,36: Type exported, but not specified: erefStatus
  A type is exported, but not specified.  Use -exporttype to suppress message.
eref.h:14,3: Type exported, but not specified: erefTable
< checking empset.c >
erc.h:7,67: Type exported, but not specified: ercElem
erc.h:8,18: Type exported, but not specified: ercList
erc.h:9,55: Type exported, but not specified: ercInfo
The two types in eref.h can be moved to eref.c. There is no need for these types to be exported.

The three types in erc.h are used in macros defined in erf.h Hence, they cannot be moved to erc.c. They shouldn't be part of the interface though, so are not documented in the specification. We add -exporttype comments around the type declarations.

Another 5 messages concern functions. The functions bool_initMod, bool_unparse, bool_not, bool_equal, and check are not specified. We add a specification file bool.lcl containing specifications of the boolean function, and check.lcl containing a specification of check.

The other 7 (of the original 9, two are no longer reported since the declarations of ST_USED and ST_AVAIL were moved with the erefStatus type definition) messages concern constants.

All of these are "pre-processor" constants, that are used to prevent multiple inclusion of header files. Instead of adding them to the specifications, we use the -exportconstant flag to suppress the messages.

Missing Globals

Seven messags warn that global variables that appear in a modifies clause are not listed in the globals list. For example.
employee.lcl:49: Modifies list for employee_initMod uses global internal state,
                    not included in globals list.
  A global variable is used in the modifies clause, but it not listed in the
  globals list.   The variable will be added to the globals list.  Use
  -warnmissingglobs to suppress message.
   employee.lcl:49: Specification of employee_initMod
Normally, a variable (or special state) that appears in a modifies clause but no in the globals list is added to the globals list silently. In strict mode, a message is reported. We add internalState to the globals lists for employee_initMod. The other six messages are fixed similarly.

Undocumented Global Uses

One message reports an undocumented use of a global variable:
dbase.c: (in function db_keyGet)
dbase.c:68,26: Undocumented use of file static db
  A checked global variable is used in the function, but not listed in its
  globals clause.  By default, only globals specified in .lcl files are
  checked.  To check all globals, use +allglobals.  To check globals
  selectively use /*@checked@*/ in the global declaration.  Use -globs to
  suppress message.
This message was not reported earlier, since db_keyGet is declared with no globals list. Without +globnoglobs and +impcheckedstrictstatics (both are set on in strict mode) this message would not be produced.

We add /*@globals db@*/ to the declaration of db_keyGet. This propagates to produce two new messages:

dbase.c: (in function db_hire)
dbase.c:119,23: Called procedure db_keyGet may access file static db
  A checked global variable is used in the function, but not listed in its
  globals clause.  By default, only globals specified in .lcl files are
  checked.  To check all globals, use +allglobals.  To check globals
  selectively use /*@checked@*/ in the global declaration.  Use -globs to
  suppress message.
dbase.c: (in function db_setSalary)
dbase.c:228,8: Called procedure db_keyGet may access file static db
We add globals lists to db_hire and db_setSalary. After this, no undocumented globals use messages are reported.

Indirect Internal State

Twenty-two messages report calls to functions that use or modify internalState from a function that does not include internalState in its globals list. Although no internal state in the calling function is used or modified directly, internal state in a called function is used or modified. This may be important for checking evaluation order, side-effect free parameters, etc. We add internalState to the globals and modifies lists of eref_initMod, empset_insert, db_initMod and main.

These changes propagate, leading us to add internalState to the globals and modifies lists of several other functions: empset_union, empset_intersect, db_addEmpls, and db_query.

Unconstrained Calls

Sixteen messages report possible undetected modifications through unconstrained function calls. When an unspecified function declared with no modifies clause is called, LCLint has no information about what the function may modify. If +moduncon (and +modunconnomods for functions with no modifies clause) is set, an error is reported.

We add modifies clauses to the unconstrained (file static) functions empset_get, int_toSize, and db_ercKeyGet. The shorthand /*@*/ is used to indicate the function uses no global state and modifies nothing.

Undocumented Modifications

Some of the original modification errors have been eliminated by the previous changes. Nine modification errors remain, all concerning the file static variable db in db_uncheckedHire, db_fire and db_promote.

We add db to the source-code modifies clauses for db_uncheckedHire, db_fire and db_promote.

Sizeof Types

The parameter to the sizeof operator can be an expression or a type. If +sizeoftype is set (as it is in strict mode), LCLint will report places where the argument is a type. This is considered "dangerous", since is the type of the variable changes the sizeof could produce the wrong value.

Six sizeoftype messages are reported. For example,

eref.c: (in function eref_alloc)
eref.c:32,48: Parameter to sizeof is type employee: sizeof(employee)
  Parameter to sizeof operator is a type.  (Safer to use expression, int *x =
  sizeof (*x); instead of sizeof (int).)  Use -sizeoftype to suppress message.
We fix these by using expression arguments to the sizeof operator, as suggested by the error message.

Empty Macro

One message reports an empty macro body:
bool.h: (in macro bool_initMod)
bool.h:24,1: Macro definition for bool_initMod is empty
  A macro definition has no body.  Use -macroempty to suppress message.
Empty macro bodies can cause syntax problems, so we replace the definition with, do { ; } while (FALSE).

Local Exports

The final eight messages report declarations that are exported but not used outside the defining module. If this were a complete system, these declarations should be changed to static. Since we only have a simple test driver instead of a real application, we leave the declarations as exported since it makes sense for a real application to use them. (We might wonder if the test driver is adequate if these functions are not tested, however.)

We add the -exportlocal flag to suppress these messages.

Next: Continue to Strict Library
Return to Summary

Splint - Secure Programming Lint info@splint.org
Download - Documentation - Manual - Links
Source - Linux - Publications - Talks
Reporting Bugs - Mailing Lists       Sponsors - Credits