--- layout: fc_discuss_archives title: Message 98 from Frama-C-discuss on November 2013 ---
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