Frama-C Bug Tracking System - Frama-C
View Issue Details
0001023Frama-CDocumentation > ACSLpublic2011-11-18 17:022014-02-12 16:59
Jochen 
virgile 
normaltextN/A
closedfixed 
Frama-C Nitrogen-20111001 
Frama-C Oxygen-20120901 
0001023: \valid_range not mentioned in Acsl manual
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.
No tags attached.
Issue History
2011-11-18 17:02JochenNew Issue
2011-11-18 17:02JochenStatusnew => assigned
2011-11-18 17:02JochenAssigned To => signoles
2011-11-18 18:31virgileNote Added: 0002479
2011-11-18 18:31virgileAssigned Tosignoles => virgile
2012-02-23 18:32svnCheckin
2012-02-23 18:32svnStatusassigned => resolved
2012-02-23 18:32svnResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2014-02-12 16:59Note Added: 0004719
2014-02-12 16:59Statusclosed => resolved
2016-06-21 14:11signolesCategoryDocumentation => Documentation > ACSL

Notes
(0002479)
virgile   
2011-11-18 18:31   
Thanks for the report. \valid_range is indeed deprecated (\valid_range(p,min,max) is strictly equivalent to \valid(p+(min..max)), which in addition is more flexible (you can omit either or both bounds)). ACSL manual will be updated accordingly.
(0004719)
   
2014-02-12 16:59   
Fix committed to stable/neon branch.