Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002290Frama-CPlug-in > wppublic2017-03-09 11:442019-10-17 17:07
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionno change required 
PlatformLinux/macOSOSOS Version
Product VersionFrama-C 14-Silicon 
Target VersionFixed in Version 
Summary0002290: incomplete loading of saved state when using WP?
DescriptionWhen 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 InformationI am not sure whether this a problem of the kernel or of the WP plug-in.
TagsNo tags attached.
Attached Filesc file icon swap.c [^] (204 bytes) 2017-03-09 11:44 [Show Content]

- Relationships

-  Notes
(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`.

- Issue History
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
2019-10-17 17:05 correnson Status assigned => resolved
2019-10-17 17:05 correnson Resolution open => no change required
2019-10-17 17:07 signoles Status resolved => closed

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker