You can use the commentchar flag to set splint's command character to
something other than @.  For example, -commentchar # (and then the splint
annotations would be marked as /*#only#*/.

--- Dave

On Tue, 1 Oct 2002, Filippo Ferrara wrote:

> Hi to everybody
> I have some problem with the "Cosmic" compiler statement @tiny which is not
> recognised by Splint.
> What can I do to make Splint ignore "@tiny" (without commenting it)?
> or what ca I do to Splint to recognise such statement?
> Filippo Ferrara

Reply via email to