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