LCLint Sample - Weak Checks

Here, we look run LCLint in -weak mode to detect the most obvious anomalies.

Changes from Original

Differences

This is the original version with LSL dependancies removed. The
specifications are less expressive, since there is no way of describing the
underlying semantics. Parts of the specification which rely on LSL traits
(e.g., more ensures and requires clause) have been replaced with comments.
LCLint checking does not exploit anything from LSL, however, and this
version can be run without installing lsl on your system.

A few other changes were made:

   * Replaced stdio.lcl with the standard stdio.lcl specification. This is
     in the imports/ directory in the release package, and is imported using
     imports <stdio>.
   * Replaced bool.h with the standard bool.h from the lib/ directory in the
     release package.
   * Added #include's for necessary system library headers.
   * Changed format of code to improve readability. In later directories, no
     superfluous changes will be made, so diff can be used to compare files.

Modules

   * 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)

Running LCLint

Run LCLint

Running make lint produces the 16 error messages (the same as were found for
original, except with slightly different locations because of the format
changes).

Four errors involve unused variables:

empset.c:28,8: Variable er declared but not used
empset.c:135,12: Variable e declared but not used
dbase.c:210,8: Variable er declared but not used
dbase.c:211,12: Variable e declared but not used

These are fixed simply by deleting the declaration.

Two errors involve abstraction violations:

erc.c:46,9: Operands of == are abstract type (eref): tmpc->val == er
erc.c:77,11: Operands of == are abstract type (eref): elem->val == er

Since eref is an abstract type, code outside the eref module should not
depend on its representation, and the == operator does. Instead, the code
should use eref_equal to compare eref's.

Two errors involve incompatible types:

employee.c:24,9: Function strncmp expects arg 3 to be size_t gets int:
                    maxEmployeeName
erc.c:139,27: Function malloc expects arg 1 to be size_t gets int:
                 erc_size(c) * (employeePrintSize + 1) + 1

Since size_t is unsigned long, an int cannot be used where a size_t is
expected. The maxEmployeeName constant is declare in employee.lcl:

   constant int maxEmployeeName;

We change this to:

   imports <stdio> ;  /* need stdio for size_t */

   constant size_t maxEmployeeName;

This leads to a new error in employee_setName:

employee.c:11,11: Operands of == have incompatible types (int, size_t):
                     i == maxEmployeeName

Hence, we change the type of i, to size_t.

The other error, is because the argument to malloc should be a size_t. We
need to make sure the argument is positive --- informally, we know this
because erc_size always returns a non-negative, and employeePrintSize is
non-negative. To confirm this in the code, we add the int_toUnsigned
function,

unsigned int_toUnsigned (int x)
{
  if (x < 0) /* generate run-time error */
  else return (unsigned) x;
}

(It would make most sense to put this in some kind of utilities library, but
since there is none, it is added to erc.c.)

Now, no errors are reported. Since +relaxquals is set in the weak mode, an
int may be passed as a long without error, since it is safe to assume no
information is lost when the implicit conversion from int to long is made.

Seven errors involve undocumented modifications produced through calls to
erc_iterStart in empset_disjointUnion, empset_union, empset_subset,
ereftab_lookup, and erc_sprint. We could fix the inconsistency by adding
appropriate modifies clauses to these functions; however, this would be
misleading since they should produce no client visible modification. The
problem is that the modification caused by erc_iterStart is undone before
the function returns, so no modification is visible to the client. For the
call in ereftab_lookup, this is not true, since the loop may exit without
undoing the modification, leading to a memory leak. This fixed by replacing
the return with an invokation of the erc_iterReturn macro which undoes the
modification. The /*@-mods@*/ and /*@=mods@*/ stylized comments are used
around the callsites, to suppress the modification error messages.

The final error,

drive.c: (in function main)
drive.c:123,4: Return value (type db_status) ignored: hire(e)
  Result returned by function call is not used.  If this is intended, can cast
  result to (void) to eliminate message.  Use -retvalother to suppress message.

Concerns an ignored result. The code should check the status code returned
by hire.

To do this we use a check macro, similar to the standard assert, except that
it is guaranteed to evaluate its argument exactly once. The checks macro is
added to bool.h. It would make more sense in a general utilities file if
there was one.)

This produces a macro variable namespace error:

drive.c:124,14: Variable m_res name is not a macro variable (it is a local
    variable), but matches the macro variable namespace prefix "m_"
  A variable declared outside a macro body starts with the macrovarprefix.  Use
  -macrovarprefixexclude to suppress message.

This error is produced because the check macro is expanded by LCLint, so the
m_res name appears to be a local variable in violation of a naming
convention. This will be fixed in the Macros iteration, and we will return
to namespaces in Name Conventions. For now, we add the
-macrovarprefixexclude flag to suppress the message.
