Frama-clang has problems with "decreases" clauses
ID0001815: This issue was created automatically from Mantis Issue 1815. Further discussion may take place here.
|ID0001815||Frama-Clang||Plug-in > clang||public||2014-06-20||2014-09-26|
|Product Version||Frama-C Neon-20140301||Target Version||-||Fixed in Version||Frama-C GIT, precise the release id|
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.