Anonymous | Login | Signup for a new account | 2019-02-21 12:00 CET | ![]() |
Main | My View | View Issues | Change Log | Roadmap | Repositories |
View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
0002404 | Frama-C | Plug-in > wp | public | 2018-10-08 13:53 | 2018-10-09 10:14 | ||||||||
Reporter | jens | ||||||||||||
Assigned To | correnson | ||||||||||||
Priority | normal | Severity | minor | Reproducibility | sometimes | ||||||||
Status | assigned | Resolution | open | ||||||||||
Platform | OS | OS Version | |||||||||||
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. | ||||||||||||
Attached Files | ![]() | ||||||||||||
![]() |
|
(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. |
![]() |
|||
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 - 2019 MantisBT Team |