seahorn/crab

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

caballa opened this issue · 0 comments

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