| 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 | 2019-10-17 17:04 |
|
| Reporter | jens | |
| Assigned To | correnson | |
| Priority | normal | Severity | minor | Reproducibility | sometimes |
| Status | acknowledged | 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 |  diff.txt [^] (756 bytes) 2018-10-08 13:53 [Show Content] [Hide Content]< let x_5 = t_1[a_4] : int in
< let m = t_1[a_3 <- x_5] : (addr,int) farray in
< let x_6 = (x - 1) : int in
< let a_5 = shift_sint32(a, x_6) : addr in
< let x_7 = t_2[a_5] : int in
---
> let m = t_1[a_3 <- t_1[a_4]] : (addr,int) farray in
> let x_5 = (x - 1) : int in
> let a_5 = shift_sint32(a, x_5) : addr in
> let x_6 = t_2[a_5] : int in
1023,1024c1022,1023
< (x_7 <> x_4) ->
< (x_7 = x_3) ->
---
> (x_6 <> x_4) ->
> (x_6 = x_3) ->
1035c1034
< (L_UniquePartition(t_2, a_1, i, x_6) < i_1) ->
---
> (L_UniquePartition(t_2, a_1, i, x_5) < i_1) ->
1042d1040
< is_sint32(x_5) ->
1050,1051c1048
< is_sint32(m[a_4]) ->
< is_uint32(x_6) ->
---
> is_uint32(x_5) ->
1056c1053
< is_sint32(x_7) ->
---
> is_sint32(x_6) ->
|
|
Relationships 
Relationships