Subject: LCLint Version 1.4 Now Available for linux
From: [email-masked] (David Evans)
Date: Mon, 17 Oct 1994 15:40:19 GMT
Newsgroups: comp.os.linux.announce

LCLint Version 1.4 is now available via anonymous ftp.

Contents:
   1. Overview
   2. Changes from Version 1.3
   3. Availability
   4. References
   5. Feedback and Mailing Lists

1. Overview

LCLint is a lint-like tool for ANSI C.  It can be used like a traditional
lint to detect certain classes of C errors statically; if formal
specifications are also supplied, it can do more powerful checking to
detect inconsistencies between specifications and code.

Without specifications, LCLint does many of the checks done by a
traditional lint.  It reports unused declarations, type inconsistencies,
use-before-definition, unreachable code, ignored return values,
execution paths with no return, likely infinite loops, and fall-through
cases.  It provides options for stricter type-checking than standard C
(e.g., char and bool types can be treated as distinct from ints.).  It
does not do much of the portability checking (e.g., pointer alignment)
done by typical lints.

With partial specifications, written in the Larch interface language,
LCL, LCLint does stronger checking.  For example, a one-line
specification file can declare a type as abstract; LCLint checks that
the data abstraction barrier is maintained in clients of the type.  This
provides the advantages of data encapsulation, making programs easier to
understand and maintain.

Adding more specifications enables further checking, including the
detection of:

   o inconsistent use of global variables
   o undocumented modification of client-visible state
   o inconsistent use of an uninitialized formal parameter or
        failure to initialize an actual parameter
   o macros specified as functions do not behave functionally

LCLint can be customized to a particular coding style using command line
flags.  Stylized comments may be used to suppress messages and control
checking at a local level.

2. Changes from Version 1.3

This list briefly describes the main changes between version 1.3 and
version 1.4.  For more details, see the User's Guide.  Since some of
these changes produce stricter checking, new errors may be programs
which were checked using old versions of lclint.

New Platforms:

In addition to the original platforms (DEC Alpha AXP running OSF/1,
DECstation running Ultrix, Sun workstation (Sparc) running Solaris 2,
and Sun workstation (Sparc) running SunOS4.1/Solaris), lclint now
supports PC running linux and SGIs runing IRIX.  It has also been
compiled sucessfully on several other platforms.  Source code is freely
available if you are interested in building a version for some other
platform.

Changes:

o must modify checking (off in default mode, use +mustmod)
    reports instances where a specified modification is not detected in
    the implementation.

o rep exposure (off in default mode, use +repexpose, +retexpose, +assignexpose)
    reports instances where an abstract representation is exposed by
    either:
	1. returning a pointer or mutable object which is a
	      component of an abstract representation (+retexpose)
        2. assigning a component of an abstract type to a pointer or
	      mutable object to which the client has access (+assignexpose)
    (+repexpose turns both on)

o return aliases (off in default mode, use +retalias)
    reports instances where the return value is an alias to a parameter
    or global

o support for stylized iterators
    see User's Guide, section 1.5.

o checking unspecified macros as functions (off in default mode,
	use +allmacros)
    prevents expansion of all parameterized macros and checks them
    as functions of unknown type.  When using +allmacros, a single
    macro definition can be preceded by /*@notfunction*/ to force
    its expansion and prevent it being checked as a function.

o printf, scanf (and variants) format arguments checking
    checks types of additional arguments to printf and scanf calls
    if the format string is known at compile time.

o boolean comparisons (on in default mode, use -boolcompare to suppress)
    reports instances where bool values are compared
    (dangerous since C allows multiple true values)

o checks mode
    new mode with checking between standard and strict

o .lclintrc
    the .lclintrc file in the current directory (if it exists) is now
    read, after the ~/.lclintrc file.

Bug fixes:

As far as I know, all known bugs in version 1.3 have been fixed.  If you
encountered a bug in version 1.3 that has not been fixed in version 1.4,
please send a bug report to [email-masked].

o grammar parse problems
o include file semantics in different directories
o abstract bool (+bool) now handles abstract access correctly

3. Availability

LCLint is available by anonymous ftp from larch.lcs.mit.edu in
pub/Larch/lclint/.

Installation pacakages are available for the following platforms:

    o DEC Alpha AXP running OSF/1 (alpha)
    o DECstation running Ultrix (decmips)
    o Sun workstation (Sparc) running Solaris 2 (solaris2)
    o Sun workstation (Sparc) running SunOS4.1/Solaris 1 (sun4)
    o PC running linux (linux)
    o SGIs runing IRIX (irix)

The easiest, most complete way is to pick up one file containing
everything you need to run lclint.  These are called:

	lclint<version>.<platform>.tar.gz

Each installation package includes the lclint executable, library files,
manual pages, user's guide, an emacs mode, and a few samples.  Packages
may be uncompressed using gunzip.

For more information on installation packages, read the file
pub/Larch/lclint/INSTALL.  (This file is included in the installation
packages also.)

4. References

More information on LCLint is available in "Using Specifications to
Check Source Code", David Evans, MIT/LCS/TR-628.  Available as hard-copy
from MIT Laboratory of Computer Science, Reading Room, 545 Technology
Square, Cambridge, MA 02139.  Available electronically as
ftp://larch.lcs.mit.edu/pub/Larch/lclint/tr.ps.Z.

A web page on the Larch project is available at URL
    http://larch-www.lcs.mit.edu:8001/larch/

A web page for LCLint specifically, including an html version of the
User's Guide, is available at URL

   http://larch-www.lcs.mit.edu:8001/larch/lclint.html

5. Feedback and Mailing Lists

We are very interested in hearing about your experiences using LCLint.
Send any questions or comments to [email-masked].

There are two mailing lists associated with LCLint:

   [email-masked]

      Reserved for announcements of new releases and bug fixes.

   [email-masked]

      Informal discussions on the use and development of lclint.

Send a (human-readable) message to [email-masked] to
subscribe to a list.

Send bugs and compilation problems to [email-masked].

-------------------------------------------------------------------------

LCLint is the result of a joint R&D project (Larch) involving Digital
Equipment Corporation and MIT.  It was written in ANSI C by David Evans,
building on an LCL checker written by Yang Meng Tan, which in turn built
on work done by Gary Feldman, Steve Garland, and Joe Wild.  Thanks to
Chris Flatters for producing the Solaris port and Thomas G. McWilliams
for the linux port.  Many others have reported bugs or provided useful
suggestions for improving LCLint.

--
Send submissions for comp.os.linux.announce to: [email-masked]
Be sure to include Keywords: and a short description of your software.