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.

Sign up for GitHub

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

Jump to bottom

VPDomain/EqDomain: implement propagations/closure under array axioms #195

Closed
alexandernutz opened this issue Jun 22, 2017 · 1 comment
Closed

VPDomain/EqDomain: implement propagations/closure under array axioms #195

alexandernutz opened this issue Jun 22, 2017 · 1 comment
Assignees
@alexandernutz
Labels
abstract interpretation

Comments

@alexandernutz
Copy link
Member

Currently the EqDomain, runs through, roughly, but is not as "complete" as it could be, i.e., misses some possible propagations.
@alexandernutz alexandernutz self-assigned this Jun 22, 2017
alexandernutz added a commit that referenced this issue Jun 22, 2017
@alexandernutz
changes here and there, towards #195,
e138e4e 
some cleanup
alexandernutz added a commit that referenced this issue Jun 22, 2017
@alexandernutz
#195, more generous array extensionality/congruence propagations -- t…
33feb55 
…aking all nodes, and some subnodes in the current constraint
alexandernutz added a commit that referenced this issue Jun 26, 2017
@alexandernutz
improvement to EqConstraintFactory.propagateIdx(..): now not only the…
4bbb69b 
… topmost, but also inner store functions get idx-axiom propagations, #195
alexandernutz added a commit that referenced this issue Jul 6, 2017
@alexandernutz
fiddle around with propagation at addFunctionEquality(..), #195
7cd3920
@alexandernutz
Copy link
Member Author

We are going for a less eager closure notion than imagined in this issue (using, among others the weak equivalence graph). Thus I'm closing this because it does not apply anymore.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@alexandernutz alexandernutz

Labels
abstract interpretation
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@alexandernutz