lclint-interest message 50

From evs Tue Mar 19 16:24:15 1996
Date: Tue, 19 Mar 96 15:59:02 -0500
From: evs (David Evans)
In-Reply-To: John Gerard Malecki's message of Mon, 18 Mar 1996 20:00:09 -0800 (PST) <>
Subject: Specifying a side-effect-free parameter.  (Spec. vs Annotation)

Just to elaborate on John's message, all the source-code annotations
except the /*@abstract@*/ and /*@concrete@*/ type definition tags (since
specs have a different way of declaring abstract types) can be used in
LCL specifications with the same meaning as they have in source-code.
For a complete list of annotations, you can do lclint -help annotations.

> I must mention that using specifications seems to be less robust than
> using annotations.  Although I have had success with 'only' I have not
> had much success with 'sef' (Bus error).

The LCL annotations should be as robust as source-code one, but I've
focused most of my testing on source-code annotations.  If you could,
please send me the example that is producing this error.


--- Dave

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