An instance of boxes domain can be in an inconsistent state due to global state
caballa opened this issue · 0 comments
caballa commented
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