Skip to content

Example 2.31 of ACSL 1.4 (Beryllium implementation) incorrect

ID0000346: This issue was created automatically from Mantis Issue 346. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0000346 Frama-C Documentation > ACSL public 2009-12-01 2014-02-12
Reporter nrousset Assigned To virgile Resolution fixed
Priority normal Severity text Reproducibility have not tried
Platform - OS - OS Version -
Product Version Frama-C Beryllium-20090902 Target Version - Fixed in Version Frama-C Boron-20100401

Description :

n for function even() (resp. x for function odd()) must be positive for the decreases clauses to hold

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information