Skip to content

Commit 619266d

Browse files
committed
C++: Fix floating point imprecision.
1 parent ce0f2b1 commit 619266d

File tree

2 files changed

+11
-2
lines changed

2 files changed

+11
-2
lines changed

cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisStage.qll

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -936,6 +936,15 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
936936
bounded(cast.getOperand(), b, delta, upper, fromBackEdge, origdelta, reason)
937937
}
938938

939+
/**
940+
* Computes a normal form of `x` where -0.0 has changed to +0.0. This can be
941+
* needed on the lesser side of a floating-point comparison or on both sides of
942+
* a floating point equality because QL does not follow IEEE in floating-point
943+
* comparisons but instead defines -0.0 to be less than and distinct from 0.0.
944+
*/
945+
bindingset[x]
946+
private float normalizeFloatUp(float x) { result = x + 0.0 }
947+
939948
/**
940949
* Holds if `b + delta` is a valid bound for `e`.
941950
* - `upper = true` : `e <= b + delta`
@@ -1025,7 +1034,7 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
10251034
e.(SemNegateExpr).getOperand() = mid and
10261035
b instanceof SemZeroBound and
10271036
bounded(mid, b, d, upper.booleanNot(), fromBackEdge, origdelta, reason) and
1028-
f = -D::toFloat(d) and
1037+
f = normalizeFloatUp(-D::toFloat(d)) and
10291038
delta = D::fromFloat(f) and
10301039
if semPositive(e) then f >= 0 else any()
10311040
)

cpp/ql/test/library-tests/ir/range-analysis/SimpleRangeAnalysis_tests.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -271,7 +271,7 @@ int test_unary(int a) {
271271
int b = +a;
272272
range(b); // $ range=<=0 range=>=-7
273273
int c = -a;
274-
range(c); // $ range=<=7 MISSING: range=>=0
274+
range(c); // $ range=<=7 range=>=0
275275
range(b+c); // $ range="<=- ...+0" range=">=+ ...:a+0" range=>=-7 range=<=7
276276
total += b+c;
277277
range(total);

0 commit comments

Comments
 (0)