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.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001017 | Frama-C | Kernel > ACSL implementation | public | 2011-11-10 | 2015-08-03 |
| Reporter | Jochen | Assigned To | virgile | Resolution | no change required |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | - |
Description :
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.