Frama-C Bug Tracking System - Frama-C
View Issue Details
0001010Frama-CPlug-in > wppublic2011-11-04 15:342012-06-09 23:05
Frama-C Nitrogen-20111001 
0001010: warn on stderr about current restrictions, and list them in WP manual
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.
No tags attached.
Issue History
2011-11-04 15:34JochenNew Issue
2011-11-04 15:34JochenStatusnew => assigned
2011-11-04 15:34JochenAssigned To => signoles
2011-11-04 15:35signolesAssigned Tosignoles => correnson
2012-06-09 23:05yakobowskiCategoryDocumentation => Plug-in > wp

There are no notes attached to this issue.