suggest to warn about ensures clauses containing only \old variables
ID0001017: This issue was created automatically from Mantis Issue 1017. Further discussion may take place here.
|ID0001017||Frama-C||Kernel > ACSL implementation||public||2011-11-10||2015-08-03|
|Reporter||Jochen||Assigned To||virgile||Resolution||no change required|
|Product Version||Frama-C Nitrogen-20111001||Target Version||-||Fixed in Version||-|
A novice student wrote "ensures 0<=\old(n)<10;" when he actually meant "requires 0<=n<10;" in his solution to an Acsl exercise.
As this kind of error can be detected easily (ensures clauses should contain at least one identifier outside of \old), I suggest to add a warning in these cases.
See attached file for an own minimal example.