0002404: Shape of VC depends on selection of properties

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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 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

Notes
(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.

Issue History
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