warn on stderr about current restrictions, and list them in WP manual
ID0001010: This issue was created automatically from Mantis Issue 1010. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001010 | Frama-C | Plug-in > wp | public | 2011-11-04 | 2012-06-09 |
| Reporter | Jochen | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | feature | Reproducibility | N/A |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | - |
Description :
When run on a file containing Acsl axioms, WP warns about an implementation restriction.
However, when run on a file containing lemmas, WP just says it won't generate proof obligations for them, without giving any reason. I guess, lemmas aren't currently implemented; in this case, WP should tell this to the user.
Additionally, all current implementations restrictions should be listed in the WP manual. In the current version, neither axioms nor lemmas are mentioned at all.