Skip to content

Reluctant incremental analysis does not reach fixpoint and is unsound in some cases #949

@jerhard

Description

@jerhard

The incremental reluctant analysis does not reach the fix-point and produces unsound results on the test case here. Note that the configuration enables exp.earlyglobs, and incremental.reluctant.enabled.

The issue arises due to the fact that the infl set is reset after the call to solve for return node of foo. This way, the information that the return node of foo influences bar is lost. After this call to solve for the return node of foo, the unknowns relating to foo and bar are in stable.

When main is re-evaluted, at the point when g = 4 is evaluated, this destabilizes foo -- but as the influence to bar is not recorded, bar is not re-evaluated. The old, unsound value of bar is thus reused by the analysis.

Metadata

Metadata

Assignees

Type

No type

Projects

No projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions