Skip to content

arg/eval and arg/eval-int give wrong results for globals after reanalysis #1018

@FeldrinH

Description

@FeldrinH

Originally reported in #1008.

When runnin arg/eval or arg/eval-int, you can get incorrect results if globals with different vid but the same name are present, even if they are present during different analysis runs.

Reproduction:

// repro.c
int global = 32;

int main() {
    int local = 3;
}
// goblint.json
{
  "files": ["repro.c"]
}

Before reanalysis arg/eval will return ["32"] for global. After reanalysis with reset=true arg/eval will return ["Unknown int([-31,31])"] for global.

Note: The same issue can occur when running analyses with reset=false, but you need to analyze, comment out global, reanalyze, comment in global and reanalyze again to get the issue to happen.

Tested on Goblint version heads/master-0-g52ce96da5

Metadata

Metadata

Assignees

Labels

Type

No type

Projects

No projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions