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: mag at magwas.rulez.org (Magosányi Árpád)
  • Date: Tue, 27 Mar 2012 09:20:52 +0200
Hi!

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)