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

Checks Mode 2

Changes from Checks Mode 1

Differences

Fixed errors reported in first iteration.

Modules

Checks Mode 2

Running LCLint detects 4 anomalies.

Inconsistent Declarations

Two messages report inconsistent declarations:
empset.c:38,6: Function empset_insertUnique inconsistently redeclared with
                  known in globals list
  A function, variable or constant is redefined with a different type.  Use
  -incondefs to suppress message.
   empset.lcl:27: Specification of empset_insertUnique
empset.c:144,6: Function empset_initMod inconsistently redeclared with known in
                   globals list
   empset.lcl:83: Specification of empset_initMod
The globals clauses we added in the previous iteration are inconsistent with the specifications. The variable known is declared in empset.h, but should really be a file static variable in empset.c. (If we had used the +exportlocal flag, LCLint will report declarations that do not use static but are used in only one module. An error is reported for known and several other variables. These are deferred until Strict Checks.) We more the declaration of known into empset.c. Now, one inconsistent definition error is reported:
empset.c:39,6: Globals list for empset_insertUnique includes internal state,
                  known, but previously declared without globals internalState.
  A function, variable or constant is redefined with a different type.  Use
  -incondefs to suppress message.
   empset.lcl:27: Specification of empset_insertUnique
The specification for empset_insertUnique does not include file static variables, but it should include internalState to indicate that some internal state may be modified.

Global Variables

One message reports an undocumented global use:
empset.c: (in function empset_disjointUnion)
empset.c:86,7: Called procedure empset_insertUnique may access file static
                  known
  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.
We add globals known to the declaration of empset_disjoinUnion. As before, we also need to add internalState to the specification.

Global State

One message reports a global state error:
empset.c:148,24: Function returns with global known undefined
  A global variable does not satisfy its annotations when control is
  transferred.  Use -globstate to suppress message.
   empset.lcl:83: Storage known becomes undefined
In fact, this return is only take if the empset_initMod has already been defined. So, we known known is defined at the return point. We add -globstate control comments to suppress the message.

Only Storage

Rerunning LCLint, one new error is reported:
empset.c:155,3: Only storage assigned to static: known = ereftab_create()
  The only reference to this storage is transferred to another reference (e.g.,
  by returning it) that does not have the only annotation.  This may lead to a
  memory leak, since the new reference is not necessarily released.  Use
  -onlytrans to suppress message.
We add an only annotation on the declaration of known.

Next: Continue to Name Checks
Return to Summary

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