--- layout: fc_discuss_archives title: Message 97 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?



Hello David,

2013/11/12 David Yang <abiao.yang at gmail.com>:
> Indeed, for the safety critical or commercial code, they usually have
> such annotations.
>
> But for open source software code, it 's very hard for us to use the
> formal verification method on these code .
>
> This would becomes an obstacle while research want to combine using
> the formal verification and program analysis methods together.

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.

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?

Best regards,
david