Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001010Frama-CPlug-in > wppublic2011-11-04 15:342012-06-09 23:05
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeverityfeatureReproducibilityN/A
StatusassignedResolutionopen 
PlatformOSOS Version
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

- Relationships

-  Notes
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


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker