\valid(a + (0..9)) vs \valid(a[0..9])
ID0002225: This issue was created automatically from Mantis Issue 2225. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002225 | Frama-C | Kernel > ACSL implementation | public | 2016-04-13 | 2016-04-13 |
| Reporter | DavidCok | Assigned To | yakobowski | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | Windows | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
The Frama-C kernel appears to accept \valid(a + (0..9)) , but not \valid(a[0..9]). Is this intended? That is must the argument of \valid and similar functions be a set of pointers, but not an equivalent set of l-value locations?