lclint-interest message 47

From johnm@vlibs.com Tue Mar 19 15:54:50 1996
Date: Mon, 18 Mar 1996 11:37:37 -0800 (PST)
From: John Gerard Malecki 
To: lclint-interest@larch.lcs.mit.edu
Subject: 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?  For example,

In ystr.lcl I have:

	Ynode ystr_pred ( Ynode p ) {
	  modifies nothing;
	}

In ystr.h I have:

	#define ystr_pred(p) (((p)->prev == &yhead)? NULL: (p)->prev)

LCLint 2.0 --- 11 Mar 96 produces the message

	ystr.h:31,19: Macro parameter p used more than once...
  A macro parameter is not used exactly once in all possible invocations of the
  macro.  To behave like a function, each macro parameter must be used exactly
  once on all invocations of the macro so that parameters with side-effects are
  evaluated exactly once.  Use /*@sef@*/ to denote parameters that must be
  side-effect free.  Use -macroparams to suppress message.

I would now like to specify that p must be a side-effect-free
parameter.  I can do this by manually writing my own ystr.lh but I
like LCL sepcifications and having lclint build the .lh file for me.

Is there a general recipe for concocting the specification given the
annotation?  If not, is there a list of the specific rememdies?

-cheers

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