Merge pull request #6865 from MathiasVP/fix-if-none

C++/C#/JS/Python: Replace 'if p() then q() else none()' with a conjunction
This commit is contained in:
Mathias Vorreiter Pedersen
2021-10-13 19:47:55 +01:00
committed by GitHub
10 changed files with 36 additions and 44 deletions

View File

@@ -236,10 +236,9 @@ module RangeAnalysis {
) {
if exists(r.getImmediatePredecessor())
then linearDefinitionSum(r.getImmediatePredecessor(), xroot, xsign, yroot, ysign, bias)
else
if exists(r.asExpr().getIntValue())
then none() // do not model constants as sums
else (
else (
not exists(r.asExpr().getIntValue()) and // do not model constants as sums
(
exists(AddExpr add, int bias1, int bias2 | r.asExpr() = add |
// r = r1 + r2
linearDefinition(add.getLeftOperand().flow(), xroot, xsign, bias1) and
@@ -257,6 +256,7 @@ module RangeAnalysis {
linearDefinitionSum(r.asExpr().(NegExpr).getOperand().flow(), xroot, -xsign, yroot, -ysign,
-bias)
)
)
}
/**