--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on March 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] proving a contract



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.