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

[BUG] [13:54] Interval's satisfies method #235

Closed
matteboro opened this issue Nov 8, 2022 · 0 comments · Fixed by #237
Closed

[BUG] [13:54] Interval's satisfies method #235

matteboro opened this issue Nov 8, 2022 · 0 comments · Fixed by #237
Assignees
Labels
‼ priority:p1 Priority planning - level 1 🎊 resolution:resolved Bug or feature resolved - might not have been merged to master yet 🔍 scope:analysis Work regarding abstract domains or fixpoint algorithms 🐛 type:bug Something isn't working
Milestone

Comments

@matteboro
Copy link
Contributor

Description
In the satisfiesBinaryExpression method in the Interval domain when calculating the satisfiability of comparison BinaryExpression the method translate the GreaterThan operator in the LessOrEqualThan operator and the GreaterOrEqualThan operator in the
LessThan operator (in both case it switches the left and right operand). The conversion is wrong, it should be:

  • GreaterThan -> LessThan;
  • GreaterOrEqualThan -> LessOrEqualThan;

Reproducibility information
commit hash: 3122841

Expected behavior
If we calculate the the satisfiesBinaryExpression on the GreaterThan operator and on operand left: [0, 1000] and right: [0, 0] the expected output should be Satisfiability.UNKNOWN

Actual behavior
Instead what we see as output is Satisfiability.SATISFIED. That is because the GreaterThan operator is translated in the LessOrEqualThan operator with operand: right: [0, 0] and left: [0, 1000], which, in fact, is always satisfied

@matteboro matteboro added the 🐛 type:bug Something isn't working label Nov 8, 2022
@lucaneg lucaneg added ‼ priority:p1 Priority planning - level 1 🔍 scope:analysis Work regarding abstract domains or fixpoint algorithms labels Nov 8, 2022
@lucaneg lucaneg added this to the 0.1b7 milestone Nov 8, 2022
@lucaneg lucaneg added the 🎊 resolution:resolved Bug or feature resolved - might not have been merged to master yet label Nov 8, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
‼ priority:p1 Priority planning - level 1 🎊 resolution:resolved Bug or feature resolved - might not have been merged to master yet 🔍 scope:analysis Work regarding abstract domains or fixpoint algorithms 🐛 type:bug Something isn't working
Projects
Archived in project
2 participants