suggest to provide FILE,LINE references for proof obligations in WP cmd-line output
ID0001011: This issue was created automatically from Mantis Issue 1011. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001011 | Frama-C | Plug-in > wp | public | 2011-11-04 | 2011-11-04 |
| Reporter | Jochen | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | - |
Description :
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.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information