Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001443Frama-CPlug-in > wppublic2013-06-11 20:442014-03-13 15:57
Reportervirgile 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130501 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001443: Property reported as inconditionnally valid when its dependency graph shows some orange box
DescriptionUsing 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.
Steps To Reproducecommand line used:
frama-c-gui -wp -wp-model Typed+ref -wp-split binary_search_proved.c -wp-rte -wp-proof alt-ergo,why3:Z3
TagsNo tags attached.
Attached Filesc file icon binary_search_proved.c [^] (1,137 bytes) 2013-06-11 20:44 [Show Content]

- Relationships

-  Notes
(0003944)
signoles (manager)
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.

- Issue History
Date Modified Username Field Change
2013-06-11 20:44 virgile New Issue
2013-06-11 20:44 virgile Status new => assigned
2013-06-11 20:44 virgile Assigned To => correnson
2013-06-11 20:44 virgile File Added: binary_search_proved.c
2013-06-12 09:04 signoles Note Added: 0003944
2013-06-19 15:45 signoles Assigned To correnson => signoles
2013-06-19 15:45 signoles Status assigned => confirmed
2013-06-20 08:56 svn Checkin
2013-06-20 13:48 svn Checkin
2013-06-20 13:48 signoles Status confirmed => resolved
2013-06-20 13:48 signoles Resolution open => fixed
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker