--- layout: fc_discuss_archives title: Message 98 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Why wp plugin failed to prove such naive properties?



Dear David,

On 13 November 2013 12:42, David MENTRE <dmentre at linux-france.org> wrote:
> CEA has a plug-in that allows to put annotations in a file separated
> from the code (I don't know to which extent, i.e. would it allow to
> add loop invariant?). Unfortunately this plug-in is proprietary.
>

Yeah, they seems already have such a plugin named "GenAssigns" that
can infer missing assigns for source code.
This page you suggested for me yesterday mentioned that plugin:
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-September/003831.html


> That's said, I am wondering if open source project would not accept
> patches for annotations. After all, Frama-C is open source (so anybody
> can replay the verification) and annotations are in comments (so no
> impact on binary). If it brings additional guarantees on the code, a
> reasonable maintainer should accept such annotations. Have you tried
> to send annotations upstream?

I haven't tried to send annotations upstream before.
Since they are in comments, I also think they might accept such annotations.

Inferring loop invariant is always a research top in these years.

Currently, maybe there does not exist a good way to automatically
generate such loop invariants. ;-)

Many thanks.

-david