\valid_range not mentioned in Acsl manual
ID0001023: This issue was created automatically from Mantis Issue 1023. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001023 | Frama-C | Documentation > ACSL | public | 2011-11-18 | 2014-02-12 |
| Reporter | Jochen | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | text | Reproducibility | N/A |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
Description :
In the manual "ACSL: ANSI/ISO C Specification Language Version 1.5", \valid_range is not mentioned.
On p.70, it says " the ACSL built-in predicate \valid (p) is now equivalent to \validrange (p,0,0)." where the "_" seems to be missing.
No other occurrences of "\valid" followed by "range" could be found using my pdf search button.