2021-02-27 10:56 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001023Frama-CDocumentation > ACSLpublic2014-02-12 16:59
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeveritytextReproducibilityN/A
StatusclosedResolutionfixed 
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.
Attached Files

-Relationships
+Relationships

-Notes

~0002479

virgile (developer)

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

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2011-11-18 17:02 Jochen New Issue
2011-11-18 17:02 Jochen Status new => assigned
2011-11-18 17:02 Jochen Assigned To => signoles
2011-11-18 18:31 virgile Note Added: 0002479
2011-11-18 18:31 virgile Assigned To signoles => virgile
2012-02-23 18:32 svn
2012-02-23 18:32 svn Status assigned => resolved
2012-02-23 18:32 svn Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2013-12-19 01:12 Source_changeset_attached => framac master 25ded863
2014-02-12 16:54 Source_changeset_attached => framac stable/neon 25ded863
2014-02-12 16:59 Note Added: 0004719
2014-02-12 16:59 Status closed => resolved
2016-06-21 14:11 signoles Category Documentation => Documentation > ACSL
+Issue History