Frama-C Bug Tracking System - Frama-C
View Issue Details
0001443Frama-CPlug-in > wppublic2013-06-11 20:442014-03-13 15:57
virgile 
signoles 
normalminoralways
closedfixed 
Frama-C Fluorine-20130501 
Frama-C Neon-20140301 
0001443: Property reported as inconditionnally valid when its dependency graph shows some orange box
Using wp on the attached files, the rte-generated asserts (and some loop invariants) are reported as valid (green bullet), while they are dependent of some unproved loop invariant. I flag it as WP bug, as it occurs only when specifying two provers with -wp-proof, so that I suspect some issue in reporting dependencies in this setting.
command line used: frama-c-gui -wp -wp-model Typed+ref -wp-split binary_search_proved.c -wp-rte -wp-proof alt-ergo,why3:Z3
No tags attached.
c binary_search_proved.c (1,137) 2013-06-11 20:44
https://bts.frama-c.com/file_download.php?file_id=502&type=bug
Issue History
2013-06-11 20:44virgileNew Issue
2013-06-11 20:44virgileStatusnew => assigned
2013-06-11 20:44virgileAssigned To => correnson
2013-06-11 20:44virgileFile Added: binary_search_proved.c
2013-06-12 09:04signolesNote Added: 0003944
2013-06-19 15:45signolesAssigned Tocorrenson => signoles
2013-06-19 15:45signolesStatusassigned => confirmed
2013-06-20 08:56svnCheckin
2013-06-20 13:48svnCheckin
2013-06-20 13:48signolesStatusconfirmed => resolved
2013-06-20 13:48signolesResolutionopen => fixed
2014-03-13 15:56signolesFixed in Version => Frama-C Neon-20140301
2014-03-13 15:57signolesStatusresolved => closed

Notes
(0003944)
signoles   
2013-06-12 09:04   
Virgile, I cannot reproduce your issue: the only green assertion is the one before the loop which depends on nothing (except a precondition actually, but WP does not include them). Though it may be a difference in our configurations.