25 #include "clang/Analysis/FlowSensitive/Formula.h"
316 /// Ensures that `Expr` is mapped to a `BoolValue` and returns its formula.
317 const Formula &forceBoolValue(Environment &Env, const Expr &Expr) {  in forceBoolValue()
320     return Value->formula();  in forceBoolValue()
324   return Value->formula();  in forceBoolValue()
418 /// `ModelPred` builds a logical formula relating the predicate in
423     const Formula &(*ModelPred)(Environment &Env, const Formula &ExprVal,  in transferValueOrImpl()
424                                 const Formula &HasValueVal)) {  in transferValueOrImpl()
436                        HasValueVal->formula()));  in transferValueOrImpl()
443                              [](Environment &Env, const Formula &ExprVal,  in transferValueOrStringEmptyCall()
444                                 const Formula &HasValueVal) -> const Formula & {  in transferValueOrStringEmptyCall()
461                       [](Environment &Env, const Formula &ExprVal,  in transferValueOrNotEqX()
462                          const Formula &HasValueVal) -> const Formula & {  in transferValueOrNotEqX()
625 const Formula &evaluateEquality(Arena &A, const Formula &EqVal,  in evaluateEquality()
626                                 const Formula &LHS, const Formula &RHS) {  in evaluateEquality()
640   // We rewrite b) as !EqVal => (LHS v RHS), for a more compact formula.  in evaluateEquality()
659       Env.assume(evaluateEquality(A, *CmpValue, LHasVal->formula(),  in transferOptionalAndOptionalCmp()
660                                   RHasVal->formula()));  in transferOptionalAndOptionalCmp()
674         evaluateEquality(A, *CmpValue, HasVal->formula(), A.makeLiteral(true)));  in transferOptionalAndValueCmp()
686     Env.assume(evaluateEquality(A, *CmpValue, HasVal->formula(),  in transferOptionalAndNulloptCmp()
874       if (Env.proves(HasValueVal->formula()))  in diagnoseUnwrapCall()