2021-03-02 03:21 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002203Frama-CDocumentation > ACSLpublic2016-06-21 14:08
Reporterjens 
Assigned Tovirgile 
PriorityhighSeveritytextReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Magnesium 
Target VersionFixed in VersionFrama-C Aluminium 
Summary0002203: LoopEntry vs LoopInit
DescriptionIn Example 2.30 (Page 43) of the ACSL implementation document (for both Magnesium and Sodium)
the code snippet uses the label "LoopInit".
I think "LoopEntry" is meant.
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0006143

virgile (developer)

Fix committed to master branch.
+Notes

-Issue History
Date Modified Username Field Change
2016-01-26 21:25 jens New Issue
2016-01-26 23:23 signoles Product Version Frama-C GIT, precise the release id => Frama-C Magnesium
2016-01-27 15:13 virgile Source_changeset_attached => framac master 5f083ba8
2016-01-27 15:13 virgile Note Added: 0006143
2016-01-27 15:13 virgile Assigned To => virgile
2016-01-27 15:13 virgile Status new => resolved
2016-01-27 15:13 virgile Resolution open => fixed
2016-06-21 14:08 signoles Fixed in Version => Frama-C Aluminium
2016-06-21 14:08 signoles Status resolved => closed
2016-06-21 14:11 signoles Category Documentation => Documentation > ACSL
+Issue History