Skip to content

An instance of boxes domain can be in an inconsistent state due to global state #3

@caballa

Description

@caballa

From @caballa on June 25, 2017 21:40

A crab variable can contain a pointer (e.g., crab-llvm stores Value* in a crab variable and seahorn stores Expr). This is very useful when we want to map back crab results to the client. The boxes domain keeps a global map from variables to internal ids. If the destructor of the factory that created the pointer to Value or Expr is called before than the global map is released then it leaves the instance of the boxes domain in an inconsistent state.

Copied from original issue: caballa/crab#17

Metadata

Metadata

Assignees

Labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions