Splint - Secure Programming Lint
Download - Documentation - Manual - Links Sponsors - Credits

Standard Checks

Changes from Iterators

Differences

Code has be rewritted to use stylized iterators.

Running LCLint with weak checking detects no errors.

Modules

Standard Checking

Now we run LCLint in standard mode, but use -memchecks to turn off checks relating to memory management (they will be covered in the next section).

LCLint reports 43 anomalies.

Ignored Return Values

Eighteen errors involved ignored boolean return values: 
empset.c:104,2: Return value (type bool) ignored: empset_insert(re...
  Result returned by function call is not used.  If this is intended, can cast
  result to (void) to eliminate message.  Use -retvalbool to suppress message.
empset.c: (in function empset_intersect)
empset.c:117,2: Return value (type bool) ignored: empset_insert(to...
empset.c:122,7: Return value (type bool) ignored: empset_delete(s1...
ereftab.c: (in function ereftab_delete)
ereftab.c:24,3: Return value (type bool) ignored: erc_delete(t, er)
dbase.c: (in function _db_addEmpls)
dbase.c:78,4: Return value (type bool) ignored: empset_insert(s, e)
dbase.c: (in function fire)
dbase.c:133,8: Return value (type bool) ignored: erc_delete(db[i]...
dbase.c: (in function promote)
dbase.c:165,7: Return value (type bool) ignored: erc_delete(db[mN...
dbase.c:170,7: Return value (type bool) ignored: erc_delete(db[fN...
drive.c:49,7: Return value (type bool) ignored: employee_setName...
drive.c:50,7: Return value (type bool) ignored: empset_insert(em...
drive.c:65,7: Return value (type bool) ignored: employee_setName...
drive.c:66,7: Return value (type bool) ignored: empset_delete(em...
drive.c:83,7: Return value (type bool) ignored: employee_setName...
drive.c:84,7: Return value (type bool) ignored: empset_insert(em...
drive.c:108,7: Return value (type bool) ignored: empset_delete(em...
drive.c:120,7: Return value (type bool) ignored: employee_setName...
drive.c:135,3: Return value (type bool) ignored: fire(17)
drive.c:159,3: Return value (type bool) ignored: fire(empset_choo...
These anomalies were not reported using weak checking, since the flag retvalbool that controls reporting of ignored boolean return values is not set. We could use -retvalbool to suppress these errors. Instead, we check to see if it is really safe to ignore the return values. The result of empset_insert, empset_delete and erc_delete indicate whether the given element was in the set. Its okay to ignore this value, so we change the declarations to indicate that the result may be ignores: 
| bool : void | empset_insert (empset s, employee e)
In a C file we would use: 
bool /*@alt void@*/ empset_insert (empset s, employee e)
The other six ignored return value messages are for calls to employee_setName and fire in the test driver. The result of fire and employee_setName is an error code --- it returns TRUE unless an error has occurred. So, it would be a good idea to check these results. Originally, I added assertions around the calls. This produces new messages: 
drive.c:83,15: Parameter 1 to assert is declared sef, but the argument may
                  modify e.name: employee_setName(&e, na)
  An actual parameter corresponding to a sef parameter may have a side-effect. 
  Use -sefparams to suppress message.
The standard library declares the parameter to assert to be side-effect free. This is a good idea, since if NDEBUG is set the parameter is not evaluated. We replace the calls to assert with a check macro (introduced in Weak Checks.)

Exit Calls

Seven of the errors involve calls to the system exit function, e.g.: 
eref.c: (in function eref_alloc)
eref.c:25,10: Argument to exit has implementation defined behavior: 1
  The argument to exit should be 0, EXIT_SUCCESS or EXIT_FAILURE  Use -exitarg
  to suppress message.
The argument to exit should not be 1, since its meaning is implementation defined. We replace these calls to use EXIT_FAILURE instead.

No Effect

Eleven messsages report statements with no effect: 
eref.c:60,3: Statement has no effect: employee_initMod()
  Statement has no visible effect --- no values are modified.  Use -noeffect to
  suppress message.
empset.c: (in function empset_initMod)
empset.c:143,3: Statement has no effect: employee_initMod()
empset.c:145,3: Statement has no effect: erc_initMod()
empset.c:146,3: Statement has no effect: ereftab_initMod()
ereftab.c: (in function ereftab_initMod)
ereftab.c:44,3: Statement has no effect: erc_initMod()
erc.h: (in macro erc_initMod)
erc.h:16,36: Statement has no effect: employee_initMod()
dbase.c: (in function db_initMod)
dbase.c:27,3: Statement has no effect: employee_initMod()
dbase.c:29,3: Statement has no effect: erc_initMod()
dbase.c:30,3: Statement has no effect: empset_initMod()
drive.c: (in function main)
drive.c:23,3: Statement has no effect: employee_initMod()
drive.c:24,3: Statement has no effect: empset_initMod()
All involve calls to initMod functions that were specified to modify nothing. They should have been specified with, 
   modifies internalState;
to indicate that no client-visible state is modified, but the state internal to the implementation module may be modified.

Boolean Comparisons

One message reports a boolean comparison: 
eref.c: (in function eref_alloc)
eref.c:53,7: Use of == with bool variables (risks inconsistency because of
                multiple true values): needsInit == FALSE
  Two bool values are compared directly using a C primitive.  This may produce
  unexpected results since all non-zero values are considered TRUE, so different
  TRUE values may not be equal.  The file bool.h (included in lclint/lib)
  provides bool_equal for safe bool comparisons.  Use -boolcompare to suppress
  message.
Since the comparison was to FALSE, we replace it with !needsInit. (An equality comparison with FALSE should be safe, anyway, since there is usually only one FALSE value. Whether or not this makes the code more readable is infinitely debatable.)

Use Before Definition

One message reports a use before definition: 
drive.c:132,34: Variable j used before definition
  An rvalue is used that may not be initialized to a value on some execution
  path.  Use -usedef to suppress message.
Here, the loop before the use of j defines j on one branch inside the loop but not the other one. Looking at the code, we know the branch that defined j must be taken since it is taken every other time through the loop and the loop iterates from 0 to 19. We suppress the error by surrounding the use of j with -usedef and =usedef control comments.

Macro Parenthesis

Four messages concern missing parenthesis on macro parameters: 
eref.h: (in macro eref_assign)
eref.h:24,54: Macro parameter used without parentheses: e
  A macro parameter is used without parentheses.  This could be dangerous if the
  macro is invoked with a complex expression and precedence rules will change
  the evaluation inside the macro.  Use -macroparens to suppress message.
eref.h: (in macro eref_equal)
eref.h:26,32: Macro parameter used without parentheses: er1
eref.h:26,39: Macro parameter used without parentheses: er2
erc.h: (in macro erc_choose)
erc.h:15,26: Macro parameter used without parentheses: c
In some contexts it is dangerous to use a macro parameter without enclosing parenthesis, since the macro may be invoked with an argument in a way that it does not have the expected evaluation order. These are fixed by added parentheses around the parameters where there are used.

Unused Parameters

One message reports an unused paramter: 
drive.c: (in function main)
drive.c:12,26: Parameter argv not used
  A function parameter is not used in the body of the function.  If the argument
  is needed for type compatibility or future plans, use /*@unused@*/ in the
  argument declaration.  Use -paramuse to suppress message.
Its okay not to use the argv parameter to main. To suppress the error, we add /*@unused@*/ before the parameter declaration.

Next: Continue to Memory Checks 1
Return to Summary

Splint - Secure Programming Lint evans@virginia.edu
Download - Documentation - Manual - Links
Source - Linux - Publications - Talks
 		Reporting Bugs    Sponsors - Credits