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#*/.
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