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:
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 usedThese 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 an arbitrary integral type, 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_toSize function that converts an int to a size_t and reports a run-time errors if the conversion does not have the same value.
(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.