LCLint Sample - Original

This is the original version published in the Larch Book. You must have lsl installed to check this version (you don't need lsl to check any of the later versions).

Modules

Each module includes an LCL specification describing the module interface, an LSL trait giving the abstract semantics of sorts used in the LCL specification. Checking done by LCLint does not exploit LSL traits or some of the information in LCL specifications. All the relevant information could be provided using stylized comments in the code instead.

• employee - employee datatype (LCL Interface Specification, LSL Trait, employeeConstants Trait, Code, Header)
• empset - sets of employees (LCL Interface Specification, Code, Header)
• dbase - database of employees (LCL Interface Specification, LSL Trait, dbaseAssumptions Trait, Code, Header)
• eref - reference to an employee (LCL Interface Specification, Code, Header)
• erc - collection of erefs (LCL Interface Specification, LSL Trait, Code, Header)
• ereftab - table of employees and erefs (LCL Interface Specification, LSL Trait, Code, Header)
• Auxillary Traits - file.lsl, refTable.lsl, sprint.lsl

Running LCLint

Here, the -weak mode is used so only the most relevant errors are reported.

lclint +lh -weak +showscan +stats +showscan +stats employee eref empset ereftab erc dbase drive.c
LCLint 2.1a --- 18 Apr 96

Warning: setting +showscan redundant with current value
Warning: setting +stats redundant with current value
< reading spec employee.lcl >
< reading spec eref.lcl >
< reading spec empset.lcl >
< reading spec ereftab.lcl >
< reading spec erc.lcl >
< reading spec dbase.lcl >
< preprocessing >
< checking employee.c >
employee.c: (in function employee_equal)
employee.c:18,17: Function strncmp expects arg 3 to be size_t gets int:
                     maxEmployeeName
  To allow arbitrary integral types to match any integral type, use
  +matchanyintegral.
< checking eref.c >
< checking empset.c >
empset.c: (in function empset_insert)
empset.c:22,8: Variable er declared but not used
  A variable is declared but never used. Use /*@unused@*/ in front of
  declaration to suppress message. Use -varuse to suppress message.
empset.c: (in function empset_disjointUnion)
empset.c:58,32: Undocumented modification of s1 possible from call to
                   erc_iterStart (through alias s2): erc_iterStart(s2)
  An externally-visible object is modified by a function, but not listed in its
  modifies clause. Use -mods to suppress message.
empset.c:58,32: Undocumented modification of s2 possible from call to
                   erc_iterStart: erc_iterStart(s2)
empset.c: (in function empset_union)
empset.c:75,32: Undocumented modification of s2 possible from call to
                   erc_iterStart (through alias s1): erc_iterStart(s1)
empset.c:75,32: Undocumented modification of s1 possible from call to
                   erc_iterStart: erc_iterStart(s1)
empset.c: (in function empset_subset)
empset.c:99,32: Undocumented modification of s1 possible from call to
                   erc_iterStart: erc_iterStart(s1)
empset.c:95,12: Variable e declared but not used
< checking ereftab.c >
ereftab.c: (in function ereftab_lookup)
ereftab.c:30,32: Undocumented modification of t possible from call to
                    erc_iterStart: erc_iterStart(t)
< checking erc.c >
erc.c: (in function erc_member)
erc.c:34,9: Operands of == are abstract type (eref): tmpc->val == er
  An abstraction barrier is broken. If necessary, use /*@access @*/ to
  allow access to an abstract type. Use -abstract to suppress message.
erc.c: (in function erc_delete)
erc.c:58,9: Operands of == are abstract type (eref): elem->val == er
erc.c: (in function erc_sprint)
erc.c:103,26: Function malloc expects arg 1 to be size_t gets int:
                 erc_size(c) * (employeePrintSize + 1) + 1
erc.c:110,32: Undocumented modification of c possible from call to
                 erc_iterStart: erc_iterStart(c)
< checking dbase.c >
dbase.c: (in function query)
dbase.c:137,8: Variable er declared but not used
dbase.c:138,12: Variable e declared but not used
< checking drive.c >
drive.c: (in function main)
drive.c:87,25: 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.
< checking macros bool.h >
< global checks >
< cleaning .......... >

Finished LCLint checking --- 16 code errors found
299 spec, 2449 source (948 before pre-processing) lines in 8.83 s.

Before looking at these messages, we will remove the lsl dependencies and reformat the code a bit for readability.

Next: Continue to Weak Checks
Return to Summary

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