incomplete loading of saved state when using WP?
ID0002290: This issue was created automatically from Mantis Issue 2290. Further discussion may take place here.
|Plug-in > wp
|no change required
|Fixed in Version
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.