Skip to content

Principled fix for Apron-Domain Top #1380

Open
@michael-schwarz

Description

@michael-schwarz

As discussed here

https://github.com/goblint/analyzer/pull/1354/files/05bd808ad40aea8555f53f1d235f257d26d67988#r1498877891

and in the GobCon.

A separate T is to be introduced that conceptually ranges over the entire environment. I gave it a shot today, but turns out it is a major rewrite that I don't have time for before wrapping up my thesis.
Among other things, it and also entails carefully thinking about where variable values are only forgotten as opposed to removed from the environment.

Creating this separate issue for the principled fix allows merging #1354 which is not the grand unified fix but a step in the right direction (and away from a setup which we know to be unsound) which also allows for experiments in a setting that is not unsound.

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugcleanupRefactoring, clean-uprelationalRelational analyses (Apron, affeq, lin2var)

    Type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions