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

Get Rid of IBoogieVar in AbstractInterpretation #222

Closed
greitsch opened this issue Sep 7, 2017 · 1 comment
Closed

Get Rid of IBoogieVar in AbstractInterpretation #222

greitsch opened this issue Sep 7, 2017 · 1 comment

Comments

@greitsch
Copy link
Member

greitsch commented Sep 7, 2017

Currently, abstract interpretation uses the IBoogieVar interface to identify variables if analyzing ICFGs that stem from Boogie programs. If future RCFGs are used, the type of variables is IProgramVarOrConst. IBoogieVar and IProgramVarOrConst are incompatible types, meaning that it is impossible to easily transform one to another.

In particular, it becomes currently impossible to transform an abstract state based on IBoogieVar into an abstract state using IProgramVarOrConst. If, however, all abstract states were using IProgramVarOrConst, one could use said state in both, RCFGs of the future and "old" RCFGs.

Therefore, all IBoogieVar references should be made compatible to IProgramVarOrConst.

@danieldietsch
Copy link
Member

We added the VARDECL generic to avoid casting -- how do you propose to avoid casting in the future?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants