Generate footprint from reads clauses of logic declarations
ID0001693: This issue was created automatically from Mantis Issue 1693. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001693 | Frama-C | Plug-in > wp | public | 2014-03-13 | 2014-03-14 |
| Reporter | jens | Assigned To | correnson | Resolution | open |
| Priority | high | Severity | feature | Reproducibility | N/A |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | - |
Description :
It would be helpful if the reads clause of an axiomatic definition would be used to generate additional hypothesis for coq proofs.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information