lclint-interest message 23

Date: Mon, 14 Nov 94 13:34:54 -0500
From: evs (David Evans)
To: 72634.2402@compuserve.com
Cc: lclint-interest@larch.lcs.mit.edu
In-Reply-To: "JR (John Rogers)"'s message of 14 Nov 94 13:04:42 EST <941114180441_72634.2402_DHL75-1@CompuServe.COM>
Subject: /*NOTREACHED*/ vs. /*@ -unreachable */ ?


JR,

> My questions are:
>
> (1) In LCLint, does /*@ -unreachable */ act as /*NOTREACHED*/ does?
>
> (2) If not, is there a way in LCLint to achieve the same effect?

We can approximate the effect of /*NOTREACHED*/ by using
/*@-unreachable*/ to turn off reachability checking and
/*@=unreachable*/ to restore reachability checking to its previous
setting.  (If /*@=unreachable*/ is not used, then reachability checking
is turned off for the remainder of the file.)

For example,

	int f()
	{
	  int x = 3;
	  exit(3);
	/*@-unreachable*/
	  x++;
	}
	/*@=unreachable*/     

will produce no errors.  (I'm at a loss to understand why one would want
to leave known unreachable code, though.)  [ Note that the
/*@=unreachable*/ has to be after the "}" for this to work correctly. ]

--- Dave