martong created this revision.
martong added reviewers: steakhal, ASDenysPetrov, NoQ.
Herald added subscribers: manas, gamesh411, dkrupp, donat.nagy, Szelethus,
mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware, xazax.hun,
whisperity.
Herald added a reviewer: Szelethus.
martong requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
We can reuse the "adjustment" handling logic in the higher level
of the solver by calling `assumeSymRel`.
(Actually, this shows us that there is no point in separating the
`RangeConstraintManager` from the `RangedConstraintManager`, that
separation is in fact artificial. A follow-up NFC patch might
address this.)
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D112296
Files:
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
clang/test/Analysis/constraint-assignor.c
Index: clang/test/Analysis/constraint-assignor.c
===================================================================
--- clang/test/Analysis/constraint-assignor.c
+++ clang/test/Analysis/constraint-assignor.c
@@ -3,9 +3,8 @@
// RUN: -analyzer-checker=debug.ExprInspection \
// RUN: -verify
-// expected-no-diagnostics
-
void clang_analyzer_warnIfReached();
+void clang_analyzer_eval();
void rem_constant_rhs_ne_zero(int x, int y) {
if (x % 3 == 0) // x % 3 != 0 -> x != 0
@@ -67,3 +66,11 @@
if (d % 2 != 0)
return;
}
+
+void remainder_with_adjustment(int x, int y) {
+ if ((x + 1) % 3 == 0) // (x + 1) % 3 != 0 -> x + 1 != 0 -> x != -1
+ return;
+ clang_analyzer_eval(x + 1 != 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x != -1); // expected-warning{{TRUE}}
+ (void)x; // keep the constraints alive.
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1620,7 +1620,7 @@
Builder.getBasicValueFactory().getValue(0, Sym->getType());
// a % b != 0 implies that a != 0.
if (!Constraint.containsZero()) {
- State = RCM.assumeSymNE(State, LHS, Zero, Zero);
+ State = RCM.assumeSymRel(State, LHS, BO_NE, Zero);
if (!State)
return false;
}
Index:
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
===================================================================
---
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
+++
clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
@@ -342,7 +342,6 @@
ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
bool Assumption) override;
-protected:
/// Assume a constraint between a symbolic expression and a concrete integer.
virtual ProgramStateRef assumeSymRel(ProgramStateRef State, SymbolRef Sym,
BinaryOperator::Opcode op,
Index: clang/test/Analysis/constraint-assignor.c
===================================================================
--- clang/test/Analysis/constraint-assignor.c
+++ clang/test/Analysis/constraint-assignor.c
@@ -3,9 +3,8 @@
// RUN: -analyzer-checker=debug.ExprInspection \
// RUN: -verify
-// expected-no-diagnostics
-
void clang_analyzer_warnIfReached();
+void clang_analyzer_eval();
void rem_constant_rhs_ne_zero(int x, int y) {
if (x % 3 == 0) // x % 3 != 0 -> x != 0
@@ -67,3 +66,11 @@
if (d % 2 != 0)
return;
}
+
+void remainder_with_adjustment(int x, int y) {
+ if ((x + 1) % 3 == 0) // (x + 1) % 3 != 0 -> x + 1 != 0 -> x != -1
+ return;
+ clang_analyzer_eval(x + 1 != 0); // expected-warning{{TRUE}}
+ clang_analyzer_eval(x != -1); // expected-warning{{TRUE}}
+ (void)x; // keep the constraints alive.
+}
Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -1620,7 +1620,7 @@
Builder.getBasicValueFactory().getValue(0, Sym->getType());
// a % b != 0 implies that a != 0.
if (!Constraint.containsZero()) {
- State = RCM.assumeSymNE(State, LHS, Zero, Zero);
+ State = RCM.assumeSymRel(State, LHS, BO_NE, Zero);
if (!State)
return false;
}
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
@@ -342,7 +342,6 @@
ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
bool Assumption) override;
-protected:
/// Assume a constraint between a symbolic expression and a concrete integer.
virtual ProgramStateRef assumeSymRel(ProgramStateRef State, SymbolRef Sym,
BinaryOperator::Opcode op,
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
