LCLint Sample - Final Version

Changes from Strict Library

Differences

Fixed errors reported using strict library.

Now, running LCLint detects no anomalies.

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)

Summary

We've just about reached the limit of what can be done usefully with LCLint
2.0. In the course of checking, we have discovered a number of bugs in the
code, enhanced missing or incomplete specifications, improved the
documentation by adding annotations, adopted a naming convention, and
checked the code against a stricted version of the standard library.

Although this is a toy example, it closely mirrors how LCLint has been used
to find real problems in large programs.

If we are still unsatisfied with the trustworthiness of the code, we could:

   * Add claims to the LCL specifications and use LP to prove they are
     correct.
   * Use run-time checking tools.

