Merge pull request #12709 from MathiasVP/disable-rounding-2

C++: Disable floating point rounding in range analysis
This commit is contained in:
Mathias Vorreiter Pedersen
2023-03-30 10:05:47 +01:00
committed by GitHub
3 changed files with 5 additions and 14 deletions

View File

@@ -16,14 +16,5 @@ module FloatDelta implements DeltaSig {
Delta fromInt(int n) { result = n }
bindingset[f]
Delta fromFloat(float f) {
result =
min(float diff, float res |
diff = (res - f) and res = f.ceil()
or
diff = (f - res) and res = f.floor()
|
res order by diff
)
}
Delta fromFloat(float f) { result = f }
}

View File

@@ -29,7 +29,7 @@ private string getDirectionString(boolean d) {
}
bindingset[value]
private string getOffsetString(int value) {
private string getOffsetString(float value) {
if value >= 0 then result = "+" + value.toString() else result = value.toString()
}
@@ -37,7 +37,7 @@ bindingset[s]
string quote(string s) { if s.matches("% %") then result = "\"" + s + "\"" else result = s }
bindingset[delta]
private string getBoundString(SemBound b, int delta) {
private string getBoundString(SemBound b, float delta) {
b instanceof SemZeroBound and result = delta.toString()
or
result =
@@ -51,7 +51,7 @@ private string getBoundString(SemBound b, int delta) {
}
private string getARangeString(SemExpr e) {
exists(SemBound b, int delta, boolean upper |
exists(SemBound b, float delta, boolean upper |
semBounded(e, b, delta, upper, _) and
if semBounded(e, b, delta, upper.booleanNot(), _)
then delta != 0 and result = "==" + getBoundString(b, delta)

View File

@@ -741,7 +741,7 @@ unsigned long mult_rounding() {
range(y); // $ range===1000000003
range(x); // $ range===1000000003
xy = x * y;
range(xy); // $ range===2147483647
range(xy); // $ range===1000000006000000000
return xy; // BUG: upper bound should be >= 1000000006000000009UL
}