WP computation is looping during variable analysis
ID0001355: This issue was created automatically from Mantis Issue 1355. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001355 | Frama-C | Plug-in > wp | public | 2013-01-31 | 2014-02-12 |
| Reporter | Anne | Assigned To | yakobowski | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Oxygen-20120901 | Target Version | - | Fixed in Version | Frama-C Fluorine-20130401 |
Description :
Sorry: I didn't manage to build a small example to reproduce the problem that happen on a large application.
The infinite loop occurs before starting the WP computation itself, but after the [wp:cil2cfg] processing. It seems to be during the analysis which stat with: [wp:var_analysis] [LP+AT] logic parameters and address taken computation
The debug messages while looping are : [wp:var_kind] TheGlobalVariable is a memvar [wp:context] POPK 0: "init_value" [wp:context] PUSH 0: "init_value" [wp:var_kind] TheGlobalVariable is a memvar [wp:context] POPK 0: "init_value" [wp:context] PUSH 0: "init_value" ... etc... (always with the same variable name).
Maybe it is important to say that :
- there are recursive calls in the application;
- the variable is static to one file;
- the type of the variable is a structure. I don't know what else I can say to help, but please ask for more details if you have an idea.