WP computation is looping during variable analysis
ID0001355: This issue was created automatically from Mantis Issue 1355. Further discussion may take place here.
|ID0001355||Frama-C||Plug-in > wp||public||2013-01-31||2014-02-12|
|Priority||normal||Severity||major||Reproducibility||have not tried|
|Product Version||Frama-C Oxygen-20120901||Target Version||-||Fixed in Version||Frama-C Fluorine-20130401|
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.