================
@@ -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>()) {
+ // The symbol folds to a concrete integer. If the assumption contradicts it
+ // the path is infeasible and must be pruned; otherwise a
self-contradictory
+ // state would stay feasible and could crash checkers downstream.
+ if (!isConcreteFeasible(*CI->getValue(), Assumption))
+ return nullptr;
+ // When the fold is consistent we deliberately do NOT return early: we fall
----------------
necto wrote:
it is used as contextual synonym to "feasible".
rephrased in
57b0790fdd4e [NFC] Trim extra comments
https://github.com/llvm/llvm-project/pull/210912
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
