Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001011Frama-CPlug-in > wppublic2011-11-04 15:452011-11-04 15:45
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeverityfeatureReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in Version 
Summary0001011: suggest to provide FILE,LINE references for proof obligations in WP cmd-line output
DescriptionCurrently, the command-line (i.e. non-gui) version of WP gives internally-generated names of proof obligations, like e.g. [wp] [Simplify] Goal store_axiom_pop_of_push_pre31_push_stack_s1 : Valid [wp] [Simplify] Goal store_axiom_pop_of_push_pre26_pop_stack_s2 : Timeout In order to support the user in improving his program to get it verified, it should be made clear where an unproven obligation originated from, by providing file name and line number. Although a lot of information can be found in the directory specified with "-wp-out", the FILE,LINE information cannot.
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:45 Jochen New Issue
2011-11-04 15:45 Jochen Status new => assigned
2011-11-04 15:45 Jochen Assigned To => correnson


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker