Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0001355Frama-CPlug-in > wppublic2013-01-31 14:272014-02-12 16:58
ReporterAnne 
Assigned Toyakobowski 
PrioritynormalSeveritymajorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
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.
Relationships
Attached Files

Notes
(0003676)
Anne   
2013-01-31 15:48   
More information : the problem disappear when I use the '-lib-entry' option.
(0003677)
Anne   
2013-01-31 16:06   
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   
2013-03-15 09:37   
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   
2014-02-12 16:58   
Fix committed to stable/neon branch.

Issue History
Date ModifiedUsernameFieldChange
2013-01-31 14:27AnneNew Issue
2013-01-31 14:27AnneStatusnew => assigned
2013-01-31 14:27AnneAssigned To => correnson
2013-01-31 15:48AnneNote Added: 0003676
2013-01-31 16:06AnneNote Added: 0003677
2013-03-15 09:34yakobowskiAssigned Tocorrenson => yakobowski
2013-03-15 09:37yakobowskiNote Added: 0003765
2013-03-15 09:38svn
2013-03-15 09:38svnStatusassigned => resolved
2013-03-15 09:38svnResolutionopen => fixed
2013-04-19 11:05signolesFixed in Version => Frama-C Fluorine
2013-04-19 11:05signolesStatusresolved => closed
2013-12-19 01:11yakobowskiSource_changeset_attached => framac master c4d15783
2014-02-12 16:53yakobowskiSource_changeset_attached => framac stable/neon c4d15783
2014-02-12 16:58yakobowskiNote Added: 0004586
2014-02-12 16:58yakobowskiStatusclosed => resolved