Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000346Frama-CDocumentation > ACSLpublic2009-12-01 09:582014-02-12 16:55
Reporternrousset 
Assigned Tovirgile 
PrioritynormalSeveritytextReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000346: Example 2.31 of ACSL 1.4 (Beryllium implementation) incorrect
Descriptionn for function even() (resp. x for function odd()) must be positive for the decreases clauses to hold
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2009-12-01 09:58 nrousset New Issue
2009-12-01 10:11 signoles Status new => assigned
2009-12-01 10:11 signoles Assigned To => virgile
2010-01-19 15:04 svn Checkin
2010-01-19 15:04 svn Status assigned => resolved
2010-01-19 15:04 svn Resolution open => fixed
2010-04-13 15:30 signoles Status resolved => new
2010-04-13 15:31 signoles Status new => closed
2010-04-13 15:33 signoles Fixed in Version => Frama-C Boron
2010-04-14 16:47 svn Checkin
2016-06-21 14:11 signoles Category Documentation => Documentation > ACSL


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker