Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Cooperation with Splint

On Jun 24, 2009, at 1:06 PM, Benjamin Monate wrote:
> Disclaimer: I am a Frama-C developer :-)
>
> Hollas Boris (CR/AEY1) a ?crit :
>> Can Jessie be instructed to use a symbol other than @ to introduce
>> annotations?
>
> I add a third solution to David's quite sensible proposals:
>
> 3. Extensible framework solution: use a custom plugin. Here is a full
> example working for Beryllium beta1 based on the "hello world"  
> template.

Having over Benjamin the added advantage of not remembering the
command for changing the annotation delimiter, I grepped through
the source and I can now warn you that you should expect the
support for Clexer.annot_char to be partial: pretty-printing will almost
always be done with an hard-wired '@', be it in the GUI, in the file
specified with option -ocode, ...

If someone has been wishing ey could contribute to Frama-C for a long  
time
but didn't know where to start, fixing this is an easy task and, right  
now,
the development version is synchronized with the distribution.
diff -u format preferred :)

Pascal