|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0002404||Frama-C||Plug-in > wp||public||2018-10-08 13:53||2019-10-17 17:04|
|Product Version||Frama-C 17-Chlorine|
|Target Version||Fixed in Version|
|Summary||0002404: Shape of VC depends on selection of properties|
|Description||WP 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 Information||Is 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.
|Tags||No tags attached.|
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.
|Under development means that it will not be ready for Argon?|
|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|
|2019-10-17 17:04||correnson||Status||assigned => acknowledged|