| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0001355 | Frama-C | Plug-in > wp | public | 2013-01-31 14:27 | 2014-02-12 16:58 | ||||
| Reporter | Anne | ||||||||
| Assigned To | yakobowski | ||||||||
| Priority | normal | Severity | major | Reproducibility | have not tried | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Oxygen-20120901 | ||||||||
| Target Version | Fixed in Version | Frama-C Fluorine-20130401 | |||||||
| Summary | 0001355: WP computation is looping during variable analysis | ||||||||
| Description | Sorry: 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. | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
Anne (reporter) 2013-01-31 15:48 |
More information : the problem disappear when I use the '-lib-entry' option. |
|
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 ?). |
|
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. |
|
yakobowski (manager) 2014-02-12 16:58 |
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 |