2021-03-02 03:09 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001355Frama-CPlug-in > wppublic2014-02-12 16:58
Assigned Toyakobowski 
PrioritynormalSeveritymajorReproducibilityhave not tried
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001355: WP computation is looping during variable analysis
DescriptionSorry: 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.
TagsNo tags attached.
Attached Files




Anne (reporter)

More information : the problem disappear when I use the '-lib-entry' option.


Anne (reporter)

Sorry : it is not looping, it is just veeeeery long.

Maybe progress messages (like x/N) would help if it is possible to know N (the number of variables to process ?).


yakobowski (manager)

Without a reproducible test case, this kind of bug report is almost impossible to fix on our side. Some datastructures have been optimized, this might fix the problem.


yakobowski (manager)

Fix committed to stable/neon branch.

-Issue History
Date Modified Username Field Change
2013-01-31 14:27 Anne New Issue
2013-01-31 14:27 Anne Status new => assigned
2013-01-31 14:27 Anne Assigned To => correnson
2013-01-31 15:48 Anne Note Added: 0003676
2013-01-31 16:06 Anne Note Added: 0003677
2013-03-15 09:34 yakobowski Assigned To correnson => yakobowski
2013-03-15 09:37 yakobowski Note Added: 0003765
2013-03-15 09:38 svn
2013-03-15 09:38 svn Status assigned => resolved
2013-03-15 09:38 svn Resolution open => fixed
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed
2013-12-19 01:11 yakobowski Source_changeset_attached => framac master c4d15783
2014-02-12 16:53 yakobowski Source_changeset_attached => framac stable/neon c4d15783
2014-02-12 16:58 yakobowski Note Added: 0004586
2014-02-12 16:58 yakobowski Status closed => resolved
+Issue History