lclint-interest message 48

From johnm@vlibs.com Tue Mar 19 15:55:01 1996
Date: Mon, 18 Mar 1996 20:00:09 -0800 (PST)
From: John Gerard Malecki 
To: lclint-interest@larch.lcs.mit.edu
Subject: Re: Specifying a side-effect-free parameter.  (Spec. vs Annotation)

> Is there a general recipe to determine the LCL specification
> corresponding to a known LCLint annotation?

Sorry for replying to my own email but after re-reading "Static
Detection of Dynamic Memory Errors" I see the answer.  Simply remove
the /*@word@*/ sugar and place word as a typeSpecifier prefix.  For
example, the specification

	only Point new_point ( int x, int y ) {
	  ensures fresh(result);
	}

Generates 

	extern /*@only@*/ Point new_point (int x, int y);

This is great.  I guess the complete list is those tokens returned by
the processSpec() calls in cscanner.l.  I'll look into this in detail
later.

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).

-- 
John Gerard Malecki                  VLSI Libraries Incorporated;  408/487-5302
        2077 Gateway Place, Suite 300; San Jose, CA 95110; USA