[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