Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002290Frama-CKernelpublic2017-03-09 11:442017-03-10 11:35
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
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.


- 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


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker