Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
caballa opened this issue Jul 3, 2017 · 0 comments
Assignees
Labels
bug domains Related to abstract domains wontfix

Comments

@caballa
Copy link
Contributor

caballa commented Jul 3, 2017

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

@caballa caballa self-assigned this Jul 3, 2017
@caballa caballa added the bug label Jul 3, 2017
@caballa caballa added the domains Related to abstract domains label Aug 24, 2021
@caballa caballa added wontfix boxes Boxes domain and removed boxes Boxes domain labels Jun 17, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug domains Related to abstract domains wontfix
Projects
None yet
Development

No branches or pull requests

1 participant