================
@@ -20,10 +20,47 @@ namespace ento {
RangedConstraintManager::~RangedConstraintManager() {}
+// Is `Assumption` (i.e. "the condition is non-zero") consistent with a symbol
+// that simplified to the concrete integer `V`? Mirrors the nonloc::ConcreteInt
+// handling in SimpleConstraintManager::assumeAux.
+static bool isConcreteFeasible(const llvm::APSInt &V, bool Assumption) {
+ return (V != 0) ? Assumption : !Assumption;
+}
+
ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
SymbolRef Sym,
bool Assumption) {
- Sym = simplify(State, Sym);
+ SVal SimplifiedVal = simplifyToSVal(State, Sym);
+ // Note: a loc::ConcreteInt is not possible here. This callsite is only ever
+ // reached with non-loc-typed symbols (SimpleConstraintManager::assumeAux's
+ // nonloc::SymbolVal case and assumeSymRel's comparison-to-zero rewrite), and
+ // simplifyToSVal() -> makeSymbolVal() only produces a Loc for pointer-typed
+ // symbols -- so the fold can only ever be a nonloc::ConcreteInt.
+ if (auto CI = SimplifiedVal.getAs<nonloc::ConcreteInt>()) {
----------------
necto wrote:
2bdd388e286c [NFC] Use SVal::getAsInteger()
https://github.com/llvm/llvm-project/pull/210912
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
