--- layout: fc_discuss_archives title: Message 86 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] unproven VC with newer why version



Hello,

2009/12/8 Claude Marche <Claude.Marche at inria.fr>:
> But I think it would be possible to implement another plugin devoted to
> suggest simple annotations like this. Then running Jessie on the
> automatically annotated code could be done, and do a manual modification
> for wrong generated annotations.

Or maybe "simply" suggest such annotations in an help zone of the GUI
if certain syntactic patterns are recognized. Probably more
complicated from a development point of view. :-)

> In other words, I don't think it is a good idea to generate such an
> annotation without telling the user.

I agree.

Yours,
d.