0001355: WP computation is looping during variable analysis

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

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

Platform

OS Version

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

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