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.
TagsNo tags attached.
Relationships
Attached Files

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.

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:32svn
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
2013-12-19 01:12Source_changeset_attached => framac master 25ded863
2014-02-12 16:54Source_changeset_attached => framac stable/neon 25ded863
2014-02-12 16:59Note Added: 0004719
2014-02-12 16:59Statusclosed => resolved
2016-06-21 14:11signolesCategoryDocumentation => Documentation > ACSL