--- layout: fc_discuss_archives title: Message 83 from Frama-C-discuss on June 2009 ---
[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