incomplete loading of saved state when using WP?
ID0002290: This issue was created automatically from Mantis Issue 2290. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002290 | Frama-C | Plug-in > wp | public | 2017-03-09 | 2019-10-17 |
| Reporter | jens | Assigned To | correnson | Resolution | no change required |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | Linux/macOS | OS | - | OS Version | - |
| Product Version | Frama-C 14-Silicon | Target Version | - | Fixed in Version | - |
Description :
When I run the line frama-c -save swap.sav -wp -wp-rte swap.c on the attached line and then load the saved sate with frama-c-gui -load swap.sav
I observe the following:
1.) a message in the Frama-C-GUI:"1 state in saved file ingnored. It is invalid in this Frama-C configuration."
2.) the GUI shows which proof obligations have been verified but the tab "WP Goals" does not show any information about which prover was successful
Additional Information :
I am not sure whether this a problem of the kernel or of the WP plug-in.
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information