2021-01-15 19:24 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001010Frama-CPlug-in > wppublic2012-06-09 23:05
Assigned Tocorrenson 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in Version 
Summary0001010: warn on stderr about current restrictions, and list them in WP manual
DescriptionWhen 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.
TagsNo tags attached.
Attached Files


There are no notes attached to this issue.

-Issue History
Date Modified Username Field Change
2011-11-04 15:34 Jochen New Issue
2011-11-04 15:34 Jochen Status new => assigned
2011-11-04 15:34 Jochen Assigned To => signoles
2011-11-04 15:35 signoles Assigned To signoles => correnson
2012-06-09 23:05 yakobowski Category Documentation => Plug-in > wp
+Issue History