[clang] [clang][dataflow] Factor out built-in boolean model into an explicit module. (PR #82950)

via cfe-commits cfe-commits at lists.llvm.org
Tue Mar 12 03:41:22 PDT 2024


================
@@ -1059,9 +1066,16 @@ void Environment::assume(const Formula &F) {
   DACtx->addFlowConditionConstraint(FlowConditionToken, F);
 }
 
+#if 0
 bool Environment::proves(const Formula &F) const {
   return DACtx->flowConditionImplies(FlowConditionToken, F);
 }
+#else
+bool Environment::proves(const Formula &F) const {
+  auto V = simple_bool_model::getLiteralValue(F, *this);
+  return V.has_value() && *V;
----------------
martinboehme wrote:

```suggestion
  return V.value_or(false);
```

https://github.com/llvm/llvm-project/pull/82950


More information about the cfe-commits mailing list