Anonymous | Login | Signup for a new account | 2019-02-22 02:25 CET | ![]() |
Main | My View | View Issues | Change Log | Roadmap | Repositories |
View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
0002290 | Frama-C | Plug-in > wp | public | 2017-03-09 11:44 | 2018-09-06 16:57 | ||||||||
Reporter | jens | ||||||||||||
Assigned To | correnson | ||||||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||||||
Status | assigned | Resolution | open | ||||||||||
Platform | Linux/macOS | OS | OS Version | ||||||||||
Product Version | Frama-C 14-Silicon | ||||||||||||
Target Version | Fixed in Version | ||||||||||||
Summary | 0002290: incomplete loading of saved state when using WP? | ||||||||||||
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. | ||||||||||||
Tags | No tags attached. | ||||||||||||
Attached Files | ![]() | ||||||||||||
![]() |
|
(0006381) yakobowski (manager) 2017-03-10 11:35 edited on: 2017-03-10 11:35 |
The warning "1 state in saved file ignored. It is invalid in this Frama-C configuration." is already fixed in Phosphorus. (Loïc, the faulty state was Wp.Model.LogicCompiler.MemVar.VarUsage.Ref0MemTyped.Signature in case this if of interest to you.) I will let Loïc comment on the second part. |
(0006641) correnson (manager) 2018-09-06 16:57 |
The WP never saves its internal state on frama-c -save ; in particular, none of the generated proof obligation is available. The reason is twofold: - re-generating proof obligations on demand is super-fast ; - saving data to frama-c state is complicated and requires writing cumbersome serializers/deserializers for all WP and Qed internal types (huge task). However, the results (Properties status) are kept since they are registered into the kernel. If you re-run WP, only non-already proved goals would be tried. However, you can force WP to re-generate and re-prove goals by using `-wp-status-xxx` options, see `frama-c -wp-h`. |
![]() |
|||
Date Modified | Username | Field | Change |
2017-03-09 11:44 | jens | New Issue | |
2017-03-09 11:44 | jens | File Added: swap.c | |
2017-03-10 11:33 | yakobowski | Assigned To | => correnson |
2017-03-10 11:33 | yakobowski | Status | new => assigned |
2017-03-10 11:35 | yakobowski | Note Added: 0006381 | |
2017-03-10 11:35 | yakobowski | Note Edited: 0006381 | View Revisions |
2017-03-10 11:35 | yakobowski | Note Edited: 0006381 | View Revisions |
2018-09-06 16:45 | signoles | Category | Kernel => Plug-in > wp |
2018-09-06 16:57 | correnson | Note Added: 0006641 |
Copyright © 2000 - 2019 MantisBT Team |