Splint - Secure Programming Lint
|Download - Documentation - Manual - Links||Sponsors - Credits|
Memory Checks 3
Changes from Memory Checks 2Differences
Fixed all messages reported in second run using memory checks.
- 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)
Memory CheckingNow, the annotations we added propagate to detect new anomalies.
LCLint reports 8 anomalies.
Undefined FieldsThe first error reports undefined fields:eref.c: (in function eref_initMod) eref.c:56,14: Global storage eref_Pool contains 2 undefined fields when call returns: status, size Storage derivable from a parameter, return value or global is not defined. Use /*@out@*/ to denote passed or returned storage which need not be defined. Use -compdef to suppress message.Since we added the undef eref_Pool to the globals list for eref_initMod, LCLint assumes eref_Pool is undefined when the function is entered, and reports an error when there is a return path that does not defined all the fields of eref_Pool. In fact, this path is only taken if needsInit is false. If needsInit is false, eref_Pool is already defined. So, we use the /*@-compdef@*/ stylized comment to suppress the message.
Null PointersThe second message reports a possibly null pointer:erc.c: (in function erc_delete) erc.c:112,5: Arrow access from possibly null pointer prev: prev->next A possibly null pointer is dereferenced or misused. Value is either the result of a function which may return null (in which case, code should check it is not null), or a global, parameter or structure field declared with the null qualifier. Use -null to suppress message. erc.c:108,29: Storage prev may become nullThis is a spurious message, since we can tell from the loop structure that prev must not be null. To make sure (and to suppress the message), an assertion is added.
Memory LeaksThe remaining six messages report memory leaks in drive.c:drive.c: (in function main) drive.c:140,16: Fresh storage em1 not released before assignment: em1 = empset_create() A memory leak has been detected. Newly-allocated or only-qualified storage is not released before the last reference to is it lost. Use -mustfree to suppress message. drive.c:35,3: Fresh storage em1 allocated drive.c:146,16: Fresh storage em2 not released before assignment: em2 = empset_create() drive.c:74,3: Fresh storage em2 allocated drive.c:147,3: Fresh storage em3 not released before assignment: em3 = empset_disjointUnion(em2, em1) drive.c:87,3: Fresh storage em3 allocated drive.c:163,12: Fresh storage em1 not released before return drive.c:140,16: Fresh storage em1 allocated drive.c:163,12: Fresh storage em2 not released before return drive.c:146,16: Fresh storage em2 allocated drive.c:163,12: Fresh storage em3 not released before return drive.c:147,3: Fresh storage em3 allocatedAll involve failures to free storage before assigning a reference to a new value, or exiting from the function. We add calls to empset_final (which takes an empset as an only parameter) to fix the problems.
Next: Continue to Macros
Return to Summary