Add remark about additional axioms for read clauses
ID0001698: This issue was created automatically from Mantis Issue 1698. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001698 | Frama-C | Documentation > ACSL | public | 2014-03-14 | 2016-06-22 |
| Reporter | jens | Assigned To | patrick | Resolution | won't fix |
| Priority | normal | Severity | text | Reproducibility | N/A |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | - |
Description :
As long as WP does not generate foot prints for reads clauses of axiomatic declarations (see https://bts.frama-c.com/view.php?id=1693), it might be helpful for users to understand, that it is their responsibility to formulate additional axioms/lemmas to express the foot print. This could be added to Section 2.6.10 of "ACSL Version 1.8 Implementation in Neon-20140301".