lclint-interest message 93

From Fri Jul 19 10:31:46 1996
Date: Fri, 19 Jul 96 10:18:20 -0400
From: (David Evans)
In-Reply-To: David Evans's message of Thu, 18 Jul 96 22:10:30 -0400 <>
Subject: Initialising arrays in loops

> The parameter to MARK_DEFINED is annotated with /*@out@*/.  This means
> it need not be defined before the call, but is completely defined after
> the call returns.  (This version of MARK_DEFINED only works for
> pointers;  if we need to make it work for other types as well, we could
> use alternate types, e.g., /*@alt int@*/, in the declaration.)

Opps, what I meant to say is: one wouldn't be able to do this for an int
directly (since one can't have scalar out parameters), but instead would
need to take the address.  So, if we just wanted to say the x field is
defined, we could do,

	MARK_DEFINED (&st->x);

--- Dave

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