2021-02-27 11:19 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000724Frama-CGraphical User Interfacepublic2014-02-12 16:54
Assigned Tomonate 
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




patrick (developer)

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.


Anne (reporter)

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
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
2013-12-19 01:12 Anne Source_changeset_attached => framac master 3eefb616
2014-02-12 16:54 Anne Source_changeset_attached => framac stable/neon 3eefb616
+Issue History