2021-01-24 22:28 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001355Frama-CPlug-in > wppublic2014-02-12 16:58
ReporterAnne 
Assigned Toyakobowski 
PrioritynormalSeveritymajorReproducibilityhave not tried
StatusclosedResolutionfixed 
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

-Relationships
+Relationships

-Notes

~0003676

Anne (reporter)

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

~0003677

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 ?).

~0003765

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.

~0004586

yakobowski (manager)

Fix committed to stable/neon branch.
+Notes

-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