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: Wed, 13 Nov 2013 15:57:01 +0000
  • In-reply-to: <CAC3Lx=Z=ceJnqJ8j=MqThESC2am+sgsJnF5LR5V1dmhBa_BN-A@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> <CAA1cxujxwjN-qo8iWhqLrb7CG8MQnMbke9tLrvCbNc20+taKyw@mail.gmail.com> <CAC3Lx=Z=ceJnqJ8j=MqThESC2am+sgsJnF5LR5V1dmhBa_BN-A@mail.gmail.com>
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