Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
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.
Attached Files

- Relationships

-  Notes
(0003676)
Anne (reporter)
2013-01-31 15:48

More information : the problem disappear when I use the '-lib-entry' option.
(0003677)
Anne (reporter)
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 (manager)
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 (manager)
2014-02-12 16:58

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 Checkin
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
2014-02-12 16:58 yakobowski Note Added: 0004586
2014-02-12 16:58 yakobowski Status closed => resolved


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker