label Pre in function contracts
ID0002265: This issue was created automatically from Mantis Issue 2265. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002265 | Frama-C | Kernel > ACSL implementation | public | 2017-01-02 | 2017-01-02 |
| Reporter | jens | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C 14-Silicon | Target Version | - | Fixed in Version | - |
Description :
I have recently noted that we use both 'Pre' and 'Old' in function contracts of "ACSL by Example". The ACSL description, however, mentions the label 'Pre' only for statement annotations.
Is there a reason to allow both labels in function contracts? If not, then I would suggest to forbid 'Pre' in function contracts.