Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002404Frama-CPlug-in > wppublic2018-10-08 13:532018-10-09 10:14
Reporterjens 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilitysometimes
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C 17-Chlorine 
Target VersionFixed in Version 
Summary0002404: Shape of VC depends on selection of properties
DescriptionWP allows to select properties by using the option -wp-prop. I have noticed the following:
When selecting a property 'foo' by -wp-prop=foo, sometimes all VCs that belong to that property are verified.
However, when I wish to verify all properties, some VC's of the property 'foo' are not verified.
This might be caused by the fact that the the actual "shape" of a VC appears to depend on -wp-prop.
(I attach an example of the slight differences between a VC that belongs to a certain property "foo" depending on whether -wp-prop=foo is used or not.)

This of course defeats somehow the purpose of using -wp-prop and it would be a welcome feature
if the generation of a VC of a property 'foo' is not affected by "-wp-prop=foo".
Additional InformationIs this maybe a problem of Qed?

Also, if there are several ways to generate/simplify a VC, it would be nice if one chooses one that has a higher likelihood to be verified.
TagsNo tags attached.
Attached Filestxt file icon diff.txt [^] (756 bytes) 2018-10-08 13:53 [Show Content]

- Relationships

-  Notes
(0006661)
correnson (manager)
2018-10-08 17:04

This is a bad and unwanted side-effects or how VCs are computed nowadays.
Actually, this is due to how new Qed variable are generated on a lazy basis.

The new VC engine is more robust regarding this problem, but it is still under development.
(0006662)
jens (reporter)
2018-10-09 10:03

Under development means that it will not be ready for Argon?
(0006663)
correnson (manager)
2018-10-09 10:14

Exact.

- Issue History
Date Modified Username Field Change
2018-10-08 13:53 jens New Issue
2018-10-08 13:53 jens Status new => assigned
2018-10-08 13:53 jens Assigned To => correnson
2018-10-08 13:53 jens File Added: diff.txt
2018-10-08 17:04 correnson Note Added: 0006661
2018-10-09 10:03 jens Note Added: 0006662
2018-10-09 10:14 correnson Note Added: 0006663


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker