2021-01-18 18:33 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000346Frama-CDocumentation > ACSLpublic2014-02-12 16:55
Reporternrousset 
Assigned Tovirgile 
PrioritynormalSeveritytextReproducibilityhave not tried
StatusclosedResolutionfixed 
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
+Relationships

-Notes
There are no notes attached to this issue.
+Notes

-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
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
2013-12-19 01:13 Source_changeset_attached => framac master ed856954
2013-12-19 01:13 Source_changeset_attached => framac master 5fe24c3c
2014-02-12 16:55 Source_changeset_attached => framac stable/neon ed856954
2014-02-12 16:55 Source_changeset_attached => framac stable/neon 5fe24c3c
2016-06-21 14:11 signoles Category Documentation => Documentation > ACSL
+Issue History