Memory Checks 1

Changes from Standard

Differences

Fixed all messages reported in standard mode without memory checks.

Running LCLint with -memchecks detects no errors.

Modules

Memory Checking

Now we remove the -memchecks flags to turn on checks relating to memory management (they are done by default in the standard mode).

Here we us the -allimponly flag to disable all implicit only annotations. LCLint reports 15 anomalies. In instead we ran lclint using +allimponly, LCLint would assume that unannotated function results, structure fields and global variables are only storage. With +allimponly, LCLint reports 21 anomalies. We could find the real errors more quickly using implicit annotations, but for instructive purposes it will be clearer to see how LCLint checking leads us to add the annotations explicitly.

Null Pointers

Two messages reports a null pointer error: 
erc.c: (in function erc_create)
erc.c:39,10: Null storage c->vals derivable from return value: c
  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:37,13: Storage c->vals becomes null
erc.c: (in function erc_clear)
erc.c:55,2: Function returns with null storage derivable from parameter c->vals
   erc.c:53,13: Storage c->vals becomes null
Here, the value of c->vals is NULL (in one case in the return value, in the second, of a passed parameter when the function returns), but there is no null annotation in the type definition. We add the null annotation to the type definition of erc: 
typedef struct { /*@null@*/ ercList vals; int size; } *erc;
This annotation will propagate to detect new anomalies in the next iteration.

Returning Fresh Storage

Two errors concerning returning fresh storage as unqualified: 
erc.c: (in function erc_create)
erc.c:39,10: Fresh storage returned as unqualified (should be only): c
  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.
   erc.c:29,3: Fresh storage c allocated
Since there is no only annotation on the function result, the obligation to release storage was not transferred. We add only annotations to the specifications of erc_create and erc_sprint. These annotations propagate in the next iteration.

Only Transfers

Six messages report inconsistencies between unqualified and only or fresh storage. A reference annotated with only implies an obligation to release the storage associated with the reference before the reference is lost. Since we are not using implicit annotations here, errors are reported for assignments of freshly allocated storage to unqualified structure fields since the storage may never be released. Also, errors are reported when there structure fields are passed as only parameters to the library reallocation routine.

All of these errors relate to fields of eref_Pool, type eref_ERP: 

eref.c: (in function eref_alloc)
eref.c:19,24: Unqualified storage passed as only:
                 realloc (eref_Pool.conts, ...)
  Unqualified storage is transferred in an inconsistent way.  Use
  -unqualifiedtrans to suppress message.
eref.c:29,27: Unqualified storage passed as only:
                 realloc (eref_Pool.status, ...)
eref.c:45,21: Storage eref_Pool.status reachable from global is only (should be
                 unqualified)
  Storage derivable from a parameter does not match the alias kind expected for
  the formal parameter.  Use -compmempass to suppress message.
   eref.c:30,48: Storage eref_Pool.status becomes only
eref.c:45,21: Storage eref_Pool.conts reachable from global is only (should be
                 unqualified)
   eref.c:20,49: Storage eref_Pool.conts becomes only
eref.c: (in function eref_initMod)
eref.c:84,2: Storage eref_Pool.conts reachable from global is fresh (should be
                unqualified)
   eref.c:62,3: Fresh storage eref_Pool.conts allocated
eref.c:84,2: Storage eref_Pool.status reachable from global is fresh (should be
                unqualified)
   eref.c:70,3: Fresh storage eref_Pool.status allocated

We fix these by adding only annotations to two fields in the type definition: 

typedef struct {
  /*@only@*/ employee *conts;
  /*@only@*/ eref_status *status;
  int size;
} eref_ERP;

Releasing Temporary Storage

One message reports releasing temporary storage: 
erc.c:60,9: Implicitly temp storage c passed as only param: free (c)
  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.
Here, c is a parameter to erc_final. Since it has no annotation, it is implicitly temp storage, so it is an anomaly to pass it to free as an only parameter. An only annotation is added to the parameter declaration. This annotation will propagate to detect new anomalies in the next iteration.

Aliasing

One message concerns a possible aliasing error: 
employee.c: (in function employee_setName)
employee.c:14,11: Parameter 1 (e->name) to function strcpy is declared unique
                     but may be aliased externally by parameter 2 (na)
  A unique or only parameter may be aliased by some other parameter or visible
  global.  Use -mayaliasunique to suppress message.
The strcpy library function is declared, 
| void : char * | strcpy  (returned out unique char *s1, char *s2) 
{ modifies *s1; }
There is a unique qualifier on the first parameter since the behavior of strcpy is undefined if the parameters share storage. Here, e and na are parameters to employee_setName so there is no guaranteed that e->name and na do not share storage. We fix the problem by adding a unique annotation to the specification of employee_setName: 
bool employee_setName (employee *e, unique char na[])

Undefined Fields

Two errors report undefined fields in eref_initMod: 
eref.c:84,2: Global storage *(eref_Pool.conts) contains 4 undefined fields when
                call returns: ssNum, salary, gen, j
  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.
eref.c:84,2: Global storage eref_Pool contains 1 undefined field when call
                returns: status
The value of eref_Pool.conts is only defined if the size of the eref_Pool is greater than 0. We add a reldef qualifier to the conts field declaration to relax definition checking: 
 
typedef struct {
  /*@reldef@*/ /*@only@*/ employee *conts;
  /*@only@*/ eref_status *status;
  int size;
} eref_ERP;
The second error results from LCLint not being able to determine that the loop defining eref_Pool.status must always execute. We use the +loopexec syntactic comment to indicate that the loop must always execute at least once.

Spurious Error

The remaining error: 
erc.c:108,16: Released storage c->vals reachable from parameter at return point
  Memory is used after it has been released (either by passing as an only param
  or assigning to and only global. Use -usereleased to suppress message.
   erc.c:106,10: Storage c->vals is released
is a spurious error resulting from a complicated aliasing relationship.

In the loop, 

  for (prev = 0, elem = c->vals;
       elem != 0;
       prev = elem, elem = elem->next) 
    {
      if (eref_equal (elem->val, er))
	{ 
	  if (prev == 0)
	    c->vals = elem->next;
	  else 
	    prev->next = elem->next;
	  
	  free (elem); 
	  c->size--;
	  return TRUE;
	}
    }
elem aliases c->vals, but only on the first iteration where prev is 0. The free call releases elem (which may alias c->vals. Except, looking at the code, we know that elem only aliases c->vals when prev is 0, and if prev is 0, c->vals is reassigned. So, elem passed to free does not alias c->vals. LCLint's alias analysis is not good enough to figure this out, so an anomaly is reported to indicate that c->vals may be released when the function returns.

We could suppress the message using the -compmempass flag. Instead, we rewrite the code in a clearer way. This makes the loop easier for human readers to understand, and allows LCLint to check it correctly.

Next: Continue to Memory Checks 2
Return to Summary