--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on March 2012 ---
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.