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] 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.