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
Assigned Tomonate 
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
patrick (developer)
2011-03-18 13:49 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/, but the problem is still there.
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 - 2020 MantisBT Team
Powered by Mantis Bugtracker