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 - 2019 MantisBT Team
Powered by Mantis Bugtracker