--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on March 2012 ---
Hi, On 27/03/2012 09:20, Magos?nyi ?rp?d wrote: > I am a new user to frama-c. I am playing around with the skein code. > I thought that for practice I run frama-c without any -slevel, and for > the warnings I see I add contracts and assertions. > This is what I have for Skein_256_Init for now. > The first five "ensures" are green, but the 6th is red for me in > frama-c-gui. > I presume that the greens could be proven, but the red one cannot. > Actually I wanted in #6 to express #2-#5 in one expression. > Had I overlook something, or just the prover needs some help to be able > to prove #6? > If the latter, how to tell the prover what to do? > > Thanks for any help. > > /*@ > requires \valid(ctx); > requires hashBitLen> 0; > ensures \valid(ctx->X); > ensures \valid(&ctx->X[0]); > ensures \valid(&ctx->X[1]); > ensures \valid(&ctx->X[2]); > ensures \valid(&ctx->X[3]); > ensures \forall int i; 0<= i< 4 ==> \valid(&ctx->X[i]); > assigns ctx->h.hashBitLen \from hashBitLen; > */ > int Skein_256_Init(Skein_256_Ctxt_t *ctx, size_t hashBitLen) 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). From what I can check, your spec for Skein_256_Init is fine. You do not need to prove the properties that have a green status, as the Value Analysis has already done this job for you: green means that the property is correct on all possible executions. 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. Anyway, the Value analysis does not currently handle universal or existential quantification, so your ensures clause cannot be proven by it. 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]); Hope this helps, -- Boris Yakobowski