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

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