| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0001693 | Frama-C | Plug-in > wp | public | 2014-03-13 17:02 | 2014-03-14 13:22 |
|
| Reporter | jens | |
| Assigned To | correnson | |
| Priority | high | Severity | feature | Reproducibility | N/A |
| Status | assigned | Resolution | open | |
| Platform | | OS | | OS Version | |
| Product Version | Frama-C Neon-20140301 | |
| Target Version | | Fixed in Version | | |
|
| Summary | 0001693: Generate footprint from reads clauses of logic declarations |
| Description | It would be helpful if the reads clause of an axiomatic definition would be
used to generate additional hypothesis for coq proofs. |
| Tags | No tags attached. |
|
| Attached Files | |
|
Relationships 
Notes