Splint - Secure Programming Lint
|Download - Documentation - Manual - Links||Sponsors - Credits|
Checks Mode 2
Changes from Checks Mode 1Differences
Fixed errors reported in first iteration.
- 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)
Checks Mode 2Running LCLint detects 4 anomalies.
Inconsistent DeclarationsTwo 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_initModThe 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_insertUniqueThe 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 VariablesOne 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 StateOne 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 undefinedIn 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 StorageRerunning 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