================
@@ -546,12 +546,29 @@ class Environment {
Atom getFlowConditionToken() const { return FlowConditionToken; }
/// Record a fact that must be true if this point in the program is reached.
- void addToFlowCondition(const Formula &);
+ void assume(const Formula &);
+
+ /// Deprecated synonym for `assume()`.
+ void addToFlowCondition(const Formula &F) { assume(F); }
/// Returns true if the formula is always true when this point is reached.
- /// Returns false if the formula may be false, or if the flow condition isn't
- /// sufficiently precise to prove that it is true.
- bool flowConditionImplies(const Formula &) const;
+ /// Returns false if the formula may be false (or the flow condition isn't
+ /// sufficiently precise to prove that it is true) or if the solver times
out.
+ ///
+ /// Note that there is an asymmetry between this function and `allows()` in
+ /// that they both return false if the solver times out. The assumption is
+ /// that if `proves()` or `allows() ` returns true, this will result in a
----------------
martinboehme wrote:
Done.
https://github.com/llvm/llvm-project/pull/70046
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
