Shape of VC depends on selection of properties
ID0002404: This issue was created automatically from Mantis Issue 2404. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002404 | Frama-C | Plug-in > wp | public | 2018-10-08 | 2019-10-17 |
| Reporter | jens | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | sometimes |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C 17-Chlorine | Target Version | - | Fixed in Version | - |
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.