/// Construct a ConstraintVal indicating the constraint is underconstrained.
ConditionTruthVal() {}
+ /// \return Stored value, assuming that the value is known.
+ /// Crashes otherwise.
+ bool getValue() const {
+ return *Val;
+ }
+
/// Return true if the constraint is perfectly constrained to 'true'.
bool isConstrainedTrue() const {
return Val.hasValue() && Val.getValue();
assumeInclusiveRange(DefinedOrUnknownSVal Val, const llvm::APSInt &From,
const llvm::APSInt &To) const;
+ /// \brief Check if the given SVal is not constrained to zero and is not
+ /// a zero constant.
+ ConditionTruthVal isNonNull(SVal V) const;
+
/// \brief Check if the given SVal is constrained to zero or is a zero
/// constant.
ConditionTruthVal isNull(SVal V) const;
+ /// \return Whether values \p Lhs and \p Rhs are equal.
+ ConditionTruthVal areEqual(SVal Lhs, SVal Rhs) const;
+
/// Utility method for getting regions.
const VarRegion* getRegion(const VarDecl *D, const LocationContext *LC) const;
namespace ento {
+class ConditionTruthVal;
+
class SValBuilder {
virtual void anchor();
protected:
SVal evalBinOp(ProgramStateRef state, BinaryOperator::Opcode op,
SVal lhs, SVal rhs, QualType type);
-
+
+ /// \return Whether values in \p lhs and \p rhs are equal at \p state.
+ ConditionTruthVal areEqual(ProgramStateRef state, SVal lhs, SVal rhs);
+
+ SVal evalEQ(ProgramStateRef state, SVal lhs, SVal rhs);
+
DefinedOrUnknownSVal evalEQ(ProgramStateRef state, DefinedOrUnknownSVal lhs,
DefinedOrUnknownSVal rhs);
return CM.assume(this, inBound.castAs<DefinedSVal>(), Assumption);
}
+ConditionTruthVal ProgramState::isNonNull(SVal V) const {
+ ConditionTruthVal IsNull = isNull(V);
+ if (IsNull.isUnderconstrained())
+ return IsNull;
+ return ConditionTruthVal(!IsNull.getValue());
+}
+
+ConditionTruthVal ProgramState::areEqual(SVal Lhs, SVal Rhs) const {
+ return stateMgr->getSValBuilder().areEqual(this, Lhs, Rhs);
+}
+
ConditionTruthVal ProgramState::isNull(SVal V) const {
if (V.isZeroConstant())
return true;
type);
}
+ConditionTruthVal SValBuilder::areEqual(ProgramStateRef state, SVal lhs,
+ SVal rhs) {
+ return state->isNonNull(evalEQ(state, lhs, rhs));
+}
+
+SVal SValBuilder::evalEQ(ProgramStateRef state, SVal lhs, SVal rhs) {
+ return evalBinOp(state, BO_EQ, lhs, rhs, getConditionType());
+}
+
DefinedOrUnknownSVal SValBuilder::evalEQ(ProgramStateRef state,
DefinedOrUnknownSVal lhs,
DefinedOrUnknownSVal rhs) {
- return evalBinOp(state, BO_EQ, lhs, rhs, getConditionType())
+ return evalEQ(state, static_cast<SVal>(lhs), static_cast<SVal>(rhs))
.castAs<DefinedOrUnknownSVal>();
}