Frama-C Bug Tracking System - Frama-C
|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|
|Assigned To||correnson|| |
|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".
|Steps To Reproduce|
|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.|
|Attached Files|| diff.txt (756) 2018-10-08 13:53|
|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|