[clang] [clang][dataflow] Add `Environment::allows()`. (PR #70046)
Stanislav Gatev via cfe-commits
cfe-commits at lists.llvm.org
Tue Oct 24 08:53:07 PDT 2023
================
@@ -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
----------------
sgatev wrote:
Extra space at the end of \`allows() \`.
https://github.com/llvm/llvm-project/pull/70046
More information about the cfe-commits
mailing list