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

Memory Checks 2

Changes from Memory Checks 1

Differences

Fixed all messages reported in first run using memory checks.

Modules

Memory Checking

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

LCLint reports 10 anomalies.

Null Pointers

In part 1, we added a null annotation to the vals field of ercInfo. Three new anomalies result: 
erc.c: (in function erc_insert)
erc.c:88,2: Function returns with possibly null storage derivable from
               parameter c->vals->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:85,19: Storage c->vals->next may become null
erc.h: (in macro erc_choose)
erc.h:14,25: Arrow access from possibly null pointer c->vals: ((c)->vals)->val
erc.h: (in macro erc_elements)
erc.h:19,149: Arrow access from possibly null pointer M__ec: M__ec->val
   erc.h:19,69: Storage M__ec may become null
The first suggests a null annotation should be added to the next field of ercList: 
typedef struct _elem { eref val; /*@null@*/ struct _elem *next; } ercElem;
The other two indicate places where a null-pointer may be dereferenced.

For erc_choose there is a constraint on the caller that it only be called for a non-empty set. If the set is non-empty, vals is not null. Since there is nothing to enforce the caller constraint, it is good defensive programming practice to add an assertion to check that vals is not null before it is dereferenced.

The other error is similar. In erc_elements we iterate through the elements of the erc. The number of non-null val indirections should be the number of elements, but it makes good sense to add an assertion to make sure this is the case. (Alternately, we could rewrite the loop as, while ((M__ec) != NULL) and remove the M_i variable.)

Returning Fresh Storage

Five errors report returning fresh or only storage as unqualified: 
empset.c: (in function empset_disjointUnion)
empset.c:83,10: Fresh storage returned as unqualified (should be only): result
  Fresh storage (newly allocated in this function) is transferred in a way that
  the obligation to release storage is not propagated.   Use the /*@only@*/
  annotation to indicate the a return value is the only reference to the
  returned storage.  Use -freshtrans to suppress message.
   empset.c:67,3: Fresh storage result allocated
empset.c: (in function empset_union)
empset.c:107,10: Fresh storage returned as unqualified (should be only): result
   empset.c:91,3: Fresh storage result allocated
empset.h: (in macro empset_create)
empset.h:28,27: Only storage returned as unqualified: (erc_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.
empset.h: (in macro empset_sprint)
empset.h:34,28: Only storage returned as unqualified: (erc_sprint(es))
< checking ereftab.c >
ereftab.c: (in function ereftab_create)
ereftab.c:10,10: Only storage returned as unqualified: erc_create()
These result from the only annotations we added in Memory Checks 1. These are fixed by adding only annotations on the function results in the specifications of empset_create, empset_union, empset_disjointUnion, empset_sprint, and ereftab_create.

Releasing Temporary Storage

The only annotation we added to erc_final leads to one message reporting releasing temporary storage: 
empset.h: (in macro empset_final)
empset.h:29,37: Implicitly temp storage s passed as only param: erc_final (s)
  Temp storage (associated with a formal parameter) is transferred to a
  non-temporary reference.  The storage may be released or new aliases created.
   Use -temptrans to suppress message.
An only annotation is added to the parameter of empset_final.

Unreleased Field

The final message reports a failure to release storage: 
eref.c: (in function eref_initMod)
eref.c:70,3: Only storage eref_Pool.status not released before assignment:
    eref_Pool.status = (eref_status *)malloc(size * sizeof(eref_status))
  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.
The problem is that eref_Pool is not initialized before the call. There is no memory leak, but we need to add a globals list to indicate that eref_Pool is not defined before the call: 
void eref_initMod (void) 
   /*@globals undef eref_Pool@*/
The undef qualifier means the variable is not defined before the call, so it is not an error to assign its fields before deallocating them.

In order to make this work properly, we need to make eref_Pool a file static variable. Otherwise, we will get a consistency error since the specification does not list eref_Pool. We could add eref_Pool to the specification globals list, and declared it as an interface variable, but it is really not intended to be exported. It was exported originally so that macros exported by eref.h could use it. Now, we make it a file static variable, and rewrite the macros that use it as functions.

Next: Continue to Memory Checks 3
Return to Summary

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