Statement contracts and WP
ID0002317: This issue was created automatically from Mantis Issue 2317. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002317 | Frama-C | Documentation > manuals | public | 2017-07-18 | 2017-07-19 |
| Reporter | jens | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | text | Reproducibility | N/A |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C 15-Phosphorus | Target Version | - | Fixed in Version | - |
Description :
This is a follow-up on issue https://bts.frama-c.com/view.php?id=2300 which was rather briskly closed.
I can understand that the question on the semantics of statement contracts in WP is not discussed in the ACSL implementation manual. However, in my opinion, it should then be discussed in the WP manual.