lclint-interest message 120

From Fri Nov  8 11:43:43 1996
Date: Fri, 8 Nov 1996 19:28:01 +0300 (MSK)
From: "George K.Bronnikov" 
In-Reply-To: <>
Mime-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII


> Please post a brief message introducing yourself and describing your
> professional interests.  Feel free to also include any ideas you have
> for lclint development or comments on your experiences using lclint.

I am currently a student of Russian State University for Humanitaries,
in the Linguistics department, but this has nothing to do with my interest
to LCLint.

Me and my friends are starting a huge project of a nonstandard DBMS (a
semantic net driven by daemons); we are using LCLint as a tool to
formalize our interfaces.

>    o Experiences using lclint ---
> 	how is your organization using lclint?

We are writing the interfaces for our project's subpackages as .lcl files.
Of course, source files are also tested by LCLint.

We have a memory management subsystem of our own, so it is unlikely that
we will be able to use LCLint's memory checking extensively.

> 	which checks are most effective in catching real bugs?

Most errors I found were concerning uninitialized variables.

>    o Ideas for improvements to lclint ---

It would be great to have a way to tell LCLint some information that it
cannot figure out itself. For example, suppose we have a structure

struct qz
  int array_len;
  int *array;

,where array should be NULL if and only if array_len == 0. I would like to

struct qz q;
if (q.array_len == 0)
  /*@believe q.array == NULL @*/
  /*@believe q.array != NULL @*/

Further, I could imagine three kinds of such declarations:
  believe - LCLint should think the condition is true without checking it.
  prove   - LCLInt should prove the condition and report an error if it
  force   - LCLint should think the condition is true even if it can prove
	    the opposite (useful for some kludges).

In the end, I am sorry to say that I have already found some bugs in
	1. Type va_list is declared in the library file stdio.lcl and is
NOT declared in stdarg.lcl.
	2. In most cases, .lcl files cannot contain ANSI C keyword const.
For example,

void fun (const char *arg);

does not work.
	3. (the worse) The LCLint distribution I downloaded in source form
>from and compiled without any
modifications on my Linux box sometimes crashes (it seems like it cannot
extend the nametable). A member of our team, Yura Filimonov, is currently
investigating the problem; we will report as soon as we find something.


Previous Message Next Message Archive Summary LCLint Home Page David Evans
University of Virginia, Computer Science