Selection of [loop variant] properties in GUI
ID0000724: This issue was created automatically from Mantis Issue 724. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000724 | Frama-C | Graphical User Interface | public | 2011-02-16 | 2014-02-12 |
| Reporter | Anne | Assigned To | monate | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
Description :
The [loop variant] properties are not correctly identified when asking to compute WP on them.
Additional Information :
Try 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.