| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0002296 | Frama-C | Plug-in > wp | public | 2017-05-08 13:18 | 2017-05-08 13:18 |
|
| Reporter | Jochen | |
| Assigned To | correnson | |
| Priority | normal | Severity | feature | Reproducibility | always |
| Status | assigned | Resolution | open | |
| Platform | Phosphorus-20170501-beta1 | OS | xubuntu 16.04.1 | OS Version | |
| Product Version | | |
| Target Version | | Fixed in Version | | |
|
| Summary | 0002296: axiom about bounds of lsl result needed in the long run |
| 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. |
| Tags | No tags attached. |
|
| Attached Files |  and.c [^] (122 bytes) 2017-05-08 13:18 [Show Content] [Hide Content]
//@ requires 0 <= m <= 9;
static void foo(int m) {
short const k = (m << 1);
//@ assert k == (m << 1);
}
|
|
Relationships 
Relationships