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

Memory Checks 3

Changes from Memory Checks 2

Differences

Fixed all messages reported in second run using memory checks.

Modules

Memory Checking

Now, the annotations we added propagate to detect new anomalies.

LCLint reports 8 anomalies.

Undefined Fields

The 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 Pointers

The 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 null
This 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 Leaks

The 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 allocated
All 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

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