Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000724Frama-CGraphical User Interfacepublic2011-02-16 17:252014-02-12 16:54
ReporterAnne 
Assigned Tomonate 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000724: Selection of [loop variant] properties in GUI
DescriptionThe [loop variant] properties are not correctly identified when asking to compute WP on them.
Additional InformationTry for instance : frama-c-gui tests/wp/wp_loop.c -wp-verbose 3
and observe the "Console" window. Then calling Wp on the [loop variant] in [loop_var] function for instance, we get :

[wp] [wpAnnot.get_strategies] for behaviors names: default!
[wp] [wpAnnot.get_strategies] select stmt 148 properties
tests/wp/wp_loop.c:178:[wp] warning: [wpAnnot.get_strategies] no behaviors found

Compare for instance with the [loop assigns] property which works :
[wp] build strategy for 'loop_var', behavior 'default!', property loop_assigns_148, both assigns or not
[wp] [wp-cfg] start computing with the strategy for 'loop_var', behavior 'default!', property loop_assigns_148, both assigns or not

It also works normally for [loop invariant]...

When the WP is computed for the whole function, the [loop variant] is processed normally, and its green V mark is correctly set.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0001610)
patrick (developer)
2011-03-18 13:49

wp_gui.ml:let run_and_prove ...
this function is called with an annot_id matching
 | Some (Property.IPDecrease (_,_,Some ca,_)

Note: I performed some commits into src/wp/wpAnnot.ml,
but the problem is still there.
(0001611)
Anne (reporter)
2011-03-18 14:26

I think I found the problem: the [loop variant] property has a [Property.get_kinstr], but we don't want it to be considered as a property of this statement. We want it to be processed with the default behavior of the function (like assert).

- Issue History
Date Modified Username Field Change
2011-02-16 17:25 Anne New Issue
2011-02-16 17:25 Anne Status new => assigned
2011-02-16 17:25 Anne Assigned To => monate
2011-03-18 13:49 patrick Note Added: 0001610
2011-03-18 14:26 Anne Note Added: 0001611
2011-03-18 14:32 svn Checkin
2011-03-18 14:35 Anne Status assigned => resolved
2011-03-18 14:35 Anne Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker