Frama-C Bug Tracking System - Frama-C
View Issue Details
0000346Frama-CDocumentation > ACSLpublic2009-12-01 09:582014-02-12 16:55
nrousset 
virgile 
normaltexthave not tried
closedfixed 
Frama-C Beryllium-20090902 
Frama-C Boron-20100401 
0000346: Example 2.31 of ACSL 1.4 (Beryllium implementation) incorrect
n for function even() (resp. x for function odd()) must be positive for the decreases clauses to hold
No tags attached.
Issue History
2009-12-01 09:58nroussetNew Issue
2009-12-01 10:11signolesStatusnew => assigned
2009-12-01 10:11signolesAssigned To => virgile
2010-01-19 15:04svnCheckin
2010-01-19 15:04svnStatusassigned => resolved
2010-01-19 15:04svnResolutionopen => fixed
2010-04-13 15:30signolesStatusresolved => new
2010-04-13 15:31signolesStatusnew => closed
2010-04-13 15:33signolesFixed in Version => Frama-C Boron
2010-04-14 16:47svnCheckin
2016-06-21 14:11signolesCategoryDocumentation => Documentation > ACSL

There are no notes attached to this issue.