--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on March 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] proving a contract



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)