Checks Mode 1

Changes from All Macros

Added declarations for all macros.

Now, running in standard more reports 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)

Checks Mode 1

Using +checks selects the checks mode. This turns on many more checks then are done in standard mode. Using +checks, LCLint detects 133 anomalies. This is a large number of messages, so we have added the +showsummary flag to see a summary of what kind of errors are reported:

Error Type                Reported  Suppressed
===================       ========  =========
usedef                       0           1
exporttype                   0           5
globs                       57           1
macroempty                   0           1
compdef                      0           1
onlyunqglobaltrans           2           0
readonlytrans                6           0
mods                        16           0
mustmod                      1           0
ansireserved                 4           0
sizeoftype                   0           6
type                        17           5
enumindex                   24           0
exportheader                 4           0
exportheadervar              2           0
                          ========  =========
Total:                     133          20

The error types correspond to flag names (e.g., 57 errors were reported involving uses of global variables).

Enumerator Indexes

There are 24 messages reporting instances where an enumerator type is used to index an array. This is probably okay (we could just use +enumindex to allow enum types to be used as array indexes), but we don't know what equivalent type the compiler will use to implement enums, so it safer to cast the enums to int before using them to index arrays.

Enumerator Type Mismatches

There are 17 messages reporting instances there is a type mismatch involving and enum. These errors were not reported before, since in standard more +enumint is set to make enum and int types interchangeable.

Fifteen of the errors involve loops that use an int to index through the elements of the employeeKinds enumerator:

dbase.c: (in function db_initMod)
dbase.c:37,8: Assignment of employeeKinds to int: i = firstERC
dbase.c:37,22: Operands of <= have incompatible types (int, employeeKinds):
                  i <= lastERC
dbase.c:37,22: Incompatible types for <= (int, employeeKinds) (in post loop
                  test): i <= lastERC
dbase.c: (in function _db_keyGet)
dbase.c:60,8: Assignment of employeeKinds to int: i = firstERC
dbase.c:60,22: Operands of <= have incompatible types (int, employeeKinds):
                  i <= lastERC
dbase.c:60,22: Incompatible types for <= (int, employeeKinds) (in post loop
                  test): i <= lastERC
dbase.c: (in function fire)
dbase.c:132,8: Assignment of employeeKinds to int: i = firstERC
dbase.c:132,22: Operands of <= have incompatible types (int, employeeKinds):
                   i <= lastERC
dbase.c:132,22: Incompatible types for <= (int, employeeKinds) (in post loop
                   test): i <= lastERC
dbase.c: (in function query)
dbase.c:222,9: Assignment of employeeKinds to int: i = firstERC
dbase.c:222,23: Operands of <= have incompatible types (int, employeeKinds):
                   i <= lastERC
dbase.c:222,23: Incompatible types for <= (int, employeeKinds) (in post loop
                   test): i <= lastERC
dbase.c: (in function db_print)
dbase.c:268,8: Assignment of employeeKinds to int: i = firstERC
dbase.c:268,22: Operands of <= have incompatible types (int, employeeKinds):
                   i <= lastERC
dbase.c:268,22: Incompatible types for <= (int, employeeKinds) (in post loop
                   test): i <= lastERC
< checking drive.c >

The simplest way of fixing this would be to change the type of the index variable to the enum type. Instead, we add an iterator for cycling through the elements of the enumerator:

/*@iter employeeKinds_all (yield employeeKinds ek); @*/
# define employeeKinds_all(m_ek) \
  { employeeKinds m_ek; for (m_ek = firstERC; m_ek <= lastERC; m_ek++) {

# define end_employeeKinds_all }}

and rewrite the loops to use the iterator.

There are two more enumerator type errors. One is:

dbase.c: (in macro numERCS)
dbase.c:16,20: Incompatible types for + (enum { mMGRS, fMGRS, mNON, fNON },
                  int): lastERC - firstERC + 1

The addition is safe, so we use the +enumint flag to suppress the message:

# define numERCS (/*@+enumint@*/ (lastERC - firstERC + 1) /*@=enumint@*/)

The final enumerator type anomaly is:

drive.c: (in function main)
drive.c:128,22: Assignment of db_status to int: j = hire(e)

Here, the local variable j was declared with the wrong type. We change the declaration to be db_status (and the name to status). After this change, a new error is reported:

drive.c:132,48: Format argument 1 to printf (%d) expects int gets db_status:
                   status

for the line,

  printf("Should print 4: %d\n", /*@-usedef@*/ status /*@=usedef@*/);

The code should not rely on the value assigned to enumerator members, so it makes more sense to change this to:

  printf("Should print true: %s\n", 
	 bool_unparse (/*@-usedef@*/ status == duplERR /*@=usedef@*/));

Use and Modification of Global Variables

Fifty-seven message report undocumented uses of global variables, and 16 concern undocumented modifications. Of these, 21 concern uses of eref_Pool in eref.c:

eref.c: (in function eref_alloc)
eref.c:12,14: Undocumented use of global eref_Pool
eref.c:12,51: Undocumented use of global eref_Pool
eref.c:12,73: Undocumented use of global eref_Pool (in post loop test)
eref.c:16,14: Undocumented use of global eref_Pool
eref.c:18,7: Undocumented use of global eref_Pool
eref.c:19,24: Undocumented use of global eref_Pool
eref.c:20,14: Undocumented use of global eref_Pool
eref.c:22,11: Undocumented use of global eref_Pool
eref.c:28,7: Undocumented use of global eref_Pool
eref.c:29,27: Undocumented use of global eref_Pool
eref.c:30,10: Undocumented use of global eref_Pool
eref.c:32,11: Undocumented use of global eref_Pool
eref.c:38,7: Undocumented use of global eref_Pool
eref.c:38,26: Undocumented use of global eref_Pool
eref.c:40,27: Undocumented use of global eref_Pool
eref.c:41,9: Undocumented use of global eref_Pool
eref.c:41,37: Undocumented use of global eref_Pool (in post loop test)
eref.c:44,3: Undocumented use of global eref_Pool
eref.c: (in function eref_free)
eref.c:91,3: Undocumented use of global eref_Pool
eref.c: (in function eref_assign)
eref.c:96,3: Undocumented use of global eref_Pool
eref.c: (in function eref_get)
eref.c:101,10: Undocumented use of global eref_Pool

These errors are reported now, since checks mode turns on allglobs to report undocumented uses of all global and file scope variables that are not annotated with unchecked. We add globals lists (and modifies clauses) to the functions that use eref_Pool. For example, eref_alloc is declared:

eref eref_alloc (void) 
   /*@globals eref_Pool@*/
   /*@modifies eref_Pool@*/

(In Check Mode Checks 2, inconsistencies between the new clauses and the original specifications are reported.) Similar errors reported for known and initDone in empset.c, initDone and db in dbase.c are also fixed by adding globals and modifies clauses.

Read-Only Strings

Checks mode sets readonlytrans on, so transfer errors involving read-only string literals are reported. Six anomalies were detected:

employee.c: (in function employee_sprint)
employee.c:29,28: Read-only string literal storage used as initial value for
                     unqualified storage: gender[0] = "male"
  A read-only string literal is assigned to a non-observer reference.  Use
  -readonlytrans to suppress message.
employee.c:29,36: Read-only string literal storage used as initial value for
                     unqualified storage: gender[1] = "female"
employee.c:29,46: Read-only string literal storage used as initial value for
                     unqualified storage: gender[2] = "?"
employee.c:30,27: Read-only string literal storage used as initial value for
                     unqualified storage: jobs[0] = "manager"
employee.c:30,38: Read-only string literal storage used as initial value for
                     unqualified storage: jobs[1] = "non-manager"
employee.c:30,53: Read-only string literal storage used as initial value for
                     unqualified storage: jobs[2] = "?"

An error is reported since the initializer assigns a read-only string literal to an unqualified array element. We need to use the /*@observer@*/ annotation in the array declaration to indicate that the elements may not be modified. Since annotations only apply to the outermost declaration, a type definition is necessary:

typedef /*@observer@*/ char *obscharp;

void employee_sprint (char s[], employee e) 
{
  static obscharp gender[] = { "male", "female", "?" };
  static obscharp jobs[] = { "manager", "non-manager", "?" };

Now, an error will be reported if any code may modify an element of the array.

Reserved Names

In checks mode, LCLint reports identifiers that may conflict with names reserved for the system. Four messages report naming conflicts:

empset.c:5,6: Name _empset_get is in the implementation name space (any
                 identifier beginning with underscore)
dbase.c:45,6: Name _db_ercKeyGet is in the implementation name space (any
                 identifier beginning with underscore)
dbase.c:55,6: Name _db_keyGet is in the implementation name space (any
                 identifier beginning with underscore)
dbase.c:72,5: Name _db_addEmpls is in the implementation name space (any
                 identifier beginning with underscore)

Names beginning with _ are reserved for the compiler. We change these names to avoid the naming conflicts.

Must Modify

In checks mode, an error is reported is something listed in the modifies clause for a function is not modified by the function body. One message reports an undetected modification:

dbase.c: (in function query)
dbase.c:259,1: Suspect object listed in modifies of query not modified: s
  An object listed in the modifies clause is not modified by the implementation
  of the function.  The modification may not be detected if it is done through
  a call to an unspecified function.  Use -mustmod to suppress message.
   dbase.lcl:49: Specification of query

In fact, query does modify s, but the modification is through calls to file static functions declared with not modifies clause. If we had set +moduncon, these calls would produce errors. Without it, no error is reported, but the modification is not detected. We add a modifies clause to db_addEmpls.

Only/Unqualified Global Transfers

Two errors report transfers of only storage to unqualified globals:

empset.c:147,3: Only storage assigned to unqualified: known = ereftab_create()
  The only reference to this storage is transferred to another reference that
  does not have an aliasing annotation. This may lead to a memory leak, since
  the new reference is not necessarily released. Use -onlyunqglobaltrans to
  suppress message.
dbase.c:39,7: Only storage assigned to unqualified: db[i] = erc_create()

Here, only storage is assigned to a global (file static) variable with no annotation. These were not reported in the memory checking iterations, since onlyunqglobaltrans is not on. If we used implicit annotations, the only annotations would be assumed. Since we didn't, we add the explict only annotations to known and the elements of db. For db we need to use a typedef to apply the annotation to inner storage:

typedef /*@only@*/ erc o_erc;
static o_erc db[numERCS];

Exported Declarations

Six message report unnecessarily exported declarations missing from header files:

dbase.c:18,17: Variable db exported but not declared in header file
  A variable declaration is exported, but does not appear in a header file. 
  (Used with exportheader.)  Use -exportheadervar to suppress message.
empset.c:5,6: Function _empset_get exported but not declared in header file
  A declaration is exported, but does not appear in a header file.  Use
  -exportheader to suppress message.
   empset.c:15,1: Definition of _empset_get
dbase.c:20,6: Variable initDone exported but not declared in header file
dbase.c:45,6: Function _db_ercKeyGet exported but not declared in header file
   dbase.c:53,1: Definition of _db_ercKeyGet
dbase.c:55,6: Function _db_keyGet exported but not declared in header file
   dbase.c:70,1: Definition of _db_keyGet
dbase.c:72,5: Function _db_addEmpls exported but not declared in header file
   dbase.c:89,1: Definition of _db_addEmpls

Two variables and four functions are not declared in header files. All of these should have been declared using static to limit their scope. This produces a new error, since the empset_member macro in empset.h used _empset_get. We replace the macro with a real function, so the file state function can be called.

Next: Continue to Check Checks 2
Return to Summary