--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on March 2012 ---
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)