Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Related Changesets ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002203Frama-CDocumentation > ACSLpublic2016-01-26 21:252016-06-21 14:08
Reporterjens 
Assigned Tovirgile 
PriorityhighSeveritytextReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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

-  Notes
(0006143)
virgile (developer)
2016-01-27 15:13

 Fix committed to master branch.

- 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 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

Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker