Frama-clang has problems with "decreases" clauses
ID0001815: This issue was created automatically from Mantis Issue 1815. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001815 | Frama-Clang | Plug-in > clang | public | 2014-06-20 | 2014-09-26 |
| Reporter | jens | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | Frama-C GIT, precise the release id |
Description :
Frama-Clang reports a "expecting function spec" when it encounters a decreases-clause in a function contract.
The decrease-clause and all following clauses in the same contract are then ignored and do not appear in the normalised representation.
Steps To Reproduce :
The attached file is also available under acslplusplus/C++Examples/Problems.