Frama-C Bug Tracking System - Frama-C
View Issue Details
0001011Frama-CPlug-in > wppublic2011-11-04 15:452011-11-04 15:45
Jochen 
correnson 
normalfeaturealways
assignedopen 
Frama-C Nitrogen-20111001 
 
0001011: suggest to provide FILE,LINE references for proof obligations in WP cmd-line output
Currently, 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.
No tags attached.
Issue History
2011-11-04 15:45JochenNew Issue
2011-11-04 15:45JochenStatusnew => assigned
2011-11-04 15:45JochenAssigned To => correnson

There are no notes attached to this issue.