--- layout: fc_discuss_archives title: Message 87 from Frama-C-discuss on November 2013 ---
Dear David, Thank you very much. On 12 November 2013 14:12, David MENTRE <dmentre at linux-france.org> wrote: > In an ideal world, programmer would not produce "important" code > (safety critical or commercial code) without such annotations. We are > very far from it to say the least but it is up to us to build such a > world. > 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. > > If your loops have small, known, bounds, you might have more luck with > Value analysis plug-in. Value analysis needs less annotations, at the > expense of verifying somewhat simpler properties (e.g. absence of Run > Time Errors). Of course, your mileage may vary a lot depending on your > actual code, properties you want to prove, way to express those > properties in ACSL, etc. :-) :-) Actually I had used the value analysis plugin for a period of time. The value analysis plugin nearly needs no annotations at all. uhm, as you said, it is not very suitable for verifying some properties. That's why i change to the wp plugin. Thanks again. Best regards, -david