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)
To: lclint-interest@larch.lcs.mit.edu
Cc: johnm@vlibs.com
In-Reply-To: John Gerard Malecki's message of Mon, 18 Mar 1996 20:00:09 -0800 (PST) <199603190400.UAA06577@owl.vlibs.com>
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.

Thanks,

--- Dave