axiom about bounds of lsl result needed in the long run
ID0002296: This issue was created automatically from Mantis Issue 2296. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002296 | Frama-C | Plug-in > wp | public | 2017-05-08 | 2017-05-08 |
| Reporter | Jochen | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | Phosphorus-20170501-beta1 | OS | xubuntu 16.04.1 | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
Running "frama-c -wp and.c" on the attached program fails to prove the assertion in line 5, although it should follow immediately from the assignment in line 4.
Looking at the generated mlw file shows that "k=to_uint16(k)" can't be proven (variable name taken from c source). Apparently, the range boundaries of m from the contract in line 2 aren't propagated to m<<1.
In the long run, when bit operations will be handled in a satisfactory way, this issue should be resolved, too; the attached program can be used as a regeression test for it.