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.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002179 | Frama-C | Plug-in > wp | public | 2015-10-18 | 2015-10-18 |
| Reporter | kroeckx | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Sodium | Target Version | - | Fixed in Version | - |
Description :
Hi,
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.)