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: boris at yakobowski.org (Boris Yakobowski)
- Date: Tue, 27 Mar 2012 10:49:25 +0200
- In-reply-to: <4F716A54.8000307@magwas.rulez.org>
- References: <4F716A54.8000307@magwas.rulez.org>
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
- Follow-Ups:
- [Frama-c-discuss] proving a contract
- From: boris at yakobowski.org (Boris Yakobowski)
- [Frama-c-discuss] proving a contract
- From: mag at magwas.rulez.org (Magosányi Árpád)
- [Frama-c-discuss] proving a contract
- References:
- [Frama-c-discuss] proving a contract
- From: mag at magwas.rulez.org (Magosányi Árpád)
- [Frama-c-discuss] proving a contract
- Prev by Date: [Frama-c-discuss] proving a contract
- Next by Date: [Frama-c-discuss] proving a contract
- Previous by thread: [Frama-c-discuss] proving a contract
- Next by thread: [Frama-c-discuss] proving a contract
- Index(es):