Frama-C Bug Tracking System - Frama-C
View Issue Details
0002404Frama-CPlug-in > wppublic2018-10-08 13:532019-10-17 17:04
Frama-C 17-Chlorine 
0002404: Shape of VC depends on selection of properties
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".
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.
No tags attached.
txt diff.txt (756) 2018-10-08 13:53
Issue History
2018-10-08 13:53jensNew Issue
2018-10-08 13:53jensStatusnew => assigned
2018-10-08 13:53jensAssigned To => correnson
2018-10-08 13:53jensFile Added: diff.txt
2018-10-08 17:04corrensonNote Added: 0006661
2018-10-09 10:03jensNote Added: 0006662
2018-10-09 10:14corrensonNote Added: 0006663
2019-10-17 17:04corrensonStatusassigned => acknowledged

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.
2018-10-09 10:03   
Under development means that it will not be ready for Argon?
2018-10-09 10:14