Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Why wp plugin failed to prove such naive properties?
  • From: abiao.yang at gmail.com (David Yang)
  • Date: Tue, 12 Nov 2013 15:21:10 +0000
  • In-reply-to: <CAC3Lx=ZvBaApioyvey2FdDDQycQmJAzoQFOxH_ASiujzp=TMNg@mail.gmail.com>
  • References: <CAA1cxuhDnFw9NJL0VQrEC8oUgbjyUkE+o=SHqURuO7gs0uDi-Q@mail.gmail.com> <CAC3Lx=axPxDRonpEGmkD5gFuKdmZQHz7dxdHxDDzGmBa6L8KKw@mail.gmail.com> <CAA1cxujWyMaLJaKLJ_-raOvDoHEk4rGGaq3tPMu_b3yin9MTSw@mail.gmail.com> <CAC3Lx=ZvBaApioyvey2FdDDQycQmJAzoQFOxH_ASiujzp=TMNg@mail.gmail.com>
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