Unable to prove things that are provable, gets confused
ID0002179: This issue was created automatically from Mantis Issue 2179. Further discussion may take place here.
|ID0002179||Frama-C||Plug-in > wp||public||2015-10-18||2015-10-18|
|Product Version||Frama-C Sodium||Target Version||-||Fixed in Version||-|
In the attached file as is using wp -wp-model Typed,cast test-final.c, the last assert can't be proven, resulting in the ensures and assigns to be valid under hypotheses. This is a minimal version that still shows the problem.
However, there are several ways to make it be able to prove it and as far as I can see should have no effect on it. The different ways are:
- Removing any of the following 3 lines: p[n] = 0x80; /* there is always room for one */ HASH_BLOCK_DATA_ORDER(c, p, 1); c->num = 0;
- Removing the first assert
- Removing the requires \valid_read(c->data+(0 .. c->num-1));
I assume it gets confused because the \valid_read() overlaps with the \valid(c). It's not really needed. (In the full version the \valid_read() should more be something like \initialized.)