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] proving a contract

  • Subject: [Frama-c-discuss] proving a contract
  • From: mag at magwas.rulez.org (Magosányi Árpád)
  • Date: Tue, 27 Mar 2012 11:07:49 +0200
  • In-reply-to: <CABbVA-Csjgd3w7iXLnQr=AFeepg7ynEAJr=Thoz7b961UJz9ug@mail.gmail.com>
  • References: <4F716A54.8000307@magwas.rulez.org> <CABbVA-Csjgd3w7iXLnQr=AFeepg7ynEAJr=Thoz7b961UJz9ug@mail.gmail.com>
On 03/27/2012 10:49 AM, Boris Yakobowski wrote:

> Since your are referring to Skein, I am assuming you are using  the
> Value analysis (we usually use the terminology "prover" for
> weakest-preconditions-based plugins such as Jessie or WP).
Opps, maybe I should not even use that plugin?
What I am really trying to learn is formal verification of the code,
in the sense that
- come up with contracts for code which does not have them
- ensure that contracts are adhered to throughout the code


> However, I am a bit puzzled by your "red status on "ensures \forall
> int i [...]", as I get an orange one using the Nitrogen release of
> Frama-C. Orange means that the property has not be proven by any
> plugin, while Red means that it is always false. 

Yes, it was orange, only I am not good at colors ;)

> Anyway, the Value
> analysis does not currently handle universal or existential
> quantification, so your ensures clause cannot be proven by it.

Another sign that I maybe not using the right plugin...

> However, you can easily rewrite it in a slightly more ACSL-idiomatic
> fashion, that encompasses your four ensures, and that is understood
>
>   ensures \valid(&ctx->X[0..3]);

Thank you, it is green this way.