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 >
