Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0001023Frama-CDocumentation > ACSLpublic2011-11-18 17:022014-02-12 16:59
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeveritytextReproducibilityN/A
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001023: \valid_range not mentioned in Acsl manual
DescriptionIn 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.
Steps To Reproduce
Additional Information
TagsNo tags attached.
Relationships
Attached Files
Issue History
Date ModifiedUsernameFieldChange
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.