[clang] [clang][nullability] Use `proves()` and `assume()` instead of deprecated synonyms. (PR #70297)
via cfe-commits
cfe-commits at lists.llvm.org
Thu Oct 26 00:23:05 PDT 2023
https://github.com/martinboehme created https://github.com/llvm/llvm-project/pull/70297
None
>From f57ebb921dc5c3289cf19c3075c00fb91119acd6 Mon Sep 17 00:00:00 2001
From: Martin Braenne <mboehme at google.com>
Date: Thu, 26 Oct 2023 07:21:18 +0000
Subject: [PATCH] [clang][nullability] Use `proves()` and `assume()` instead of
deprecated synonyms.
---
.../lib/Analysis/FlowSensitive/HTMLLogger.cpp | 9 +-
.../Models/ChromiumCheckModel.cpp | 2 +-
.../Models/UncheckedOptionalAccessModel.cpp | 22 ++-
.../TypeErasedDataflowAnalysis.cpp | 2 +-
.../FlowSensitive/ChromiumCheckModelTest.cpp | 4 +-
.../FlowSensitive/SignAnalysisTest.cpp | 45 +++---
.../Analysis/FlowSensitive/TransferTest.cpp | 152 +++++++++---------
.../TypeErasedDataflowAnalysisTest.cpp | 74 +++++----
8 files changed, 149 insertions(+), 161 deletions(-)
diff --git a/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp b/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
index 8aef1d6f46089d2..8329367098b1dbb 100644
--- a/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
+++ b/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
@@ -114,11 +114,10 @@ class ModelDumper {
// guaranteed true/false here is valuable and hard to determine by hand.
if (auto *B = llvm::dyn_cast<BoolValue>(&V)) {
JOS.attribute("formula", llvm::to_string(B->formula()));
- JOS.attribute(
- "truth", Env.flowConditionImplies(B->formula()) ? "true"
- : Env.flowConditionImplies(Env.arena().makeNot(B->formula()))
- ? "false"
- : "unknown");
+ JOS.attribute("truth", Env.proves(B->formula()) ? "true"
+ : Env.proves(Env.arena().makeNot(B->formula()))
+ ? "false"
+ : "unknown");
}
}
void dump(const StorageLocation &L) {
diff --git a/clang/lib/Analysis/FlowSensitive/Models/ChromiumCheckModel.cpp b/clang/lib/Analysis/FlowSensitive/Models/ChromiumCheckModel.cpp
index 895f4ff04a172f9..f49087ababc44ce 100644
--- a/clang/lib/Analysis/FlowSensitive/Models/ChromiumCheckModel.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Models/ChromiumCheckModel.cpp
@@ -59,7 +59,7 @@ bool ChromiumCheckModel::transfer(const CFGElement &Element, Environment &Env) {
if (const auto *M = dyn_cast<CXXMethodDecl>(Call->getDirectCallee())) {
if (isCheckLikeMethod(CheckDecls, *M)) {
// Mark this branch as unreachable.
- Env.addToFlowCondition(Env.arena().makeLiteral(false));
+ Env.assume(Env.arena().makeLiteral(false));
return true;
}
}
diff --git a/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp b/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp
index 8bd9a030f50cda0..55d0713639d90da 100644
--- a/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp
@@ -413,7 +413,7 @@ bool isEmptyOptional(const Value &OptionalVal, const Environment &Env) {
auto *HasValueVal =
cast_or_null<BoolValue>(OptionalVal.getProperty("has_value"));
return HasValueVal != nullptr &&
- Env.flowConditionImplies(Env.arena().makeNot(HasValueVal->formula()));
+ Env.proves(Env.arena().makeNot(HasValueVal->formula()));
}
/// Returns true if and only if `OptionalVal` is initialized and known to be
@@ -421,8 +421,7 @@ bool isEmptyOptional(const Value &OptionalVal, const Environment &Env) {
bool isNonEmptyOptional(const Value &OptionalVal, const Environment &Env) {
auto *HasValueVal =
cast_or_null<BoolValue>(OptionalVal.getProperty("has_value"));
- return HasValueVal != nullptr &&
- Env.flowConditionImplies(HasValueVal->formula());
+ return HasValueVal != nullptr && Env.proves(HasValueVal->formula());
}
Value *getValueBehindPossiblePointer(const Expr &E, const Environment &Env) {
@@ -490,8 +489,8 @@ void transferValueOrImpl(
if (HasValueVal == nullptr)
return;
- Env.addToFlowCondition(ModelPred(Env, forceBoolValue(Env, *ValueOrPredExpr),
- HasValueVal->formula()));
+ Env.assume(ModelPred(Env, forceBoolValue(Env, *ValueOrPredExpr),
+ HasValueVal->formula()));
}
void transferValueOrStringEmptyCall(const clang::Expr *ComparisonExpr,
@@ -717,8 +716,8 @@ void transferOptionalAndOptionalCmp(const clang::CXXOperatorCallExpr *CmpExpr,
if (auto *RHasVal = getHasValue(Env, Env.getValue(*CmpExpr->getArg(1)))) {
if (CmpExpr->getOperator() == clang::OO_ExclaimEqual)
CmpValue = &A.makeNot(*CmpValue);
- Env.addToFlowCondition(evaluateEquality(A, *CmpValue, LHasVal->formula(),
- RHasVal->formula()));
+ Env.assume(evaluateEquality(A, *CmpValue, LHasVal->formula(),
+ RHasVal->formula()));
}
}
@@ -729,7 +728,7 @@ void transferOptionalAndValueCmp(const clang::CXXOperatorCallExpr *CmpExpr,
if (auto *HasVal = getHasValue(Env, Env.getValue(*E))) {
if (CmpExpr->getOperator() == clang::OO_ExclaimEqual)
CmpValue = &A.makeNot(*CmpValue);
- Env.addToFlowCondition(
+ Env.assume(
evaluateEquality(A, *CmpValue, HasVal->formula(), A.makeLiteral(true)));
}
}
@@ -917,7 +916,7 @@ llvm::SmallVector<SourceLocation> diagnoseUnwrapCall(const Expr *ObjectExpr,
if (auto *OptionalVal = getValueBehindPossiblePointer(*ObjectExpr, Env)) {
auto *Prop = OptionalVal->getProperty("has_value");
if (auto *HasValueVal = cast_or_null<BoolValue>(Prop)) {
- if (Env.flowConditionImplies(HasValueVal->formula()))
+ if (Env.proves(HasValueVal->formula()))
return {};
}
}
@@ -1004,14 +1003,13 @@ bool UncheckedOptionalAccessModel::merge(QualType Type, const Value &Val1,
bool MustNonEmpty1 = isNonEmptyOptional(Val1, Env1);
bool MustNonEmpty2 = isNonEmptyOptional(Val2, Env2);
if (MustNonEmpty1 && MustNonEmpty2)
- MergedEnv.addToFlowCondition(HasValueVal.formula());
+ MergedEnv.assume(HasValueVal.formula());
else if (
// Only make the costly calls to `isEmptyOptional` if we got "unknown"
// (false) for both calls to `isNonEmptyOptional`.
!MustNonEmpty1 && !MustNonEmpty2 && isEmptyOptional(Val1, Env1) &&
isEmptyOptional(Val2, Env2))
- MergedEnv.addToFlowCondition(
- MergedEnv.arena().makeNot(HasValueVal.formula()));
+ MergedEnv.assume(MergedEnv.arena().makeNot(HasValueVal.formula()));
setHasValue(MergedVal, HasValueVal);
return true;
}
diff --git a/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp b/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp
index 23b062665a687ca..e54fb2a01ddeead 100644
--- a/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp
+++ b/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp
@@ -148,7 +148,7 @@ class TerminatorVisitor
ConditionValue = false;
}
- Env.addToFlowCondition(Val->formula());
+ Env.assume(Val->formula());
return {&Cond, ConditionValue};
}
diff --git a/clang/unittests/Analysis/FlowSensitive/ChromiumCheckModelTest.cpp b/clang/unittests/Analysis/FlowSensitive/ChromiumCheckModelTest.cpp
index 1cb51a9cf37c5c4..a2762046665a2ce 100644
--- a/clang/unittests/Analysis/FlowSensitive/ChromiumCheckModelTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/ChromiumCheckModelTest.cpp
@@ -159,7 +159,7 @@ TEST(ChromiumCheckModelTest, CheckSuccessImpliesConditionHolds) {
auto *FooVal = cast<BoolValue>(Env.getValue(*FooDecl));
- EXPECT_TRUE(Env.flowConditionImplies(FooVal->formula()));
+ EXPECT_TRUE(Env.proves(FooVal->formula()));
};
std::string Code = R"(
@@ -190,7 +190,7 @@ TEST(ChromiumCheckModelTest, UnrelatedCheckIgnored) {
auto *FooVal = cast<BoolValue>(Env.getValue(*FooDecl));
- EXPECT_FALSE(Env.flowConditionImplies(FooVal->formula()));
+ EXPECT_FALSE(Env.proves(FooVal->formula()));
};
std::string Code = R"(
diff --git a/clang/unittests/Analysis/FlowSensitive/SignAnalysisTest.cpp b/clang/unittests/Analysis/FlowSensitive/SignAnalysisTest.cpp
index f8897929a59cf4d..362b0dea58d6b80 100644
--- a/clang/unittests/Analysis/FlowSensitive/SignAnalysisTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/SignAnalysisTest.cpp
@@ -157,44 +157,44 @@ void transferBinary(const BinaryOperator *BO, const MatchFinder::MatchResult &M,
switch (BO->getOpcode()) {
case BO_GT:
// pos > pos
- State.Env.addToFlowCondition(
+ State.Env.assume(
A.makeImplies(*Comp, A.makeImplies(RHSProps.Pos->formula(),
LHSProps.Pos->formula())));
// pos > zero
- State.Env.addToFlowCondition(
+ State.Env.assume(
A.makeImplies(*Comp, A.makeImplies(RHSProps.Zero->formula(),
LHSProps.Pos->formula())));
break;
case BO_LT:
// neg < neg
- State.Env.addToFlowCondition(
+ State.Env.assume(
A.makeImplies(*Comp, A.makeImplies(RHSProps.Neg->formula(),
LHSProps.Neg->formula())));
// neg < zero
- State.Env.addToFlowCondition(
+ State.Env.assume(
A.makeImplies(*Comp, A.makeImplies(RHSProps.Zero->formula(),
LHSProps.Neg->formula())));
break;
case BO_GE:
// pos >= pos
- State.Env.addToFlowCondition(
+ State.Env.assume(
A.makeImplies(*Comp, A.makeImplies(RHSProps.Pos->formula(),
LHSProps.Pos->formula())));
break;
case BO_LE:
// neg <= neg
- State.Env.addToFlowCondition(
+ State.Env.assume(
A.makeImplies(*Comp, A.makeImplies(RHSProps.Neg->formula(),
LHSProps.Neg->formula())));
break;
case BO_EQ:
- State.Env.addToFlowCondition(
+ State.Env.assume(
A.makeImplies(*Comp, A.makeImplies(RHSProps.Neg->formula(),
LHSProps.Neg->formula())));
- State.Env.addToFlowCondition(
+ State.Env.assume(
A.makeImplies(*Comp, A.makeImplies(RHSProps.Zero->formula(),
LHSProps.Zero->formula())));
- State.Env.addToFlowCondition(
+ State.Env.assume(
A.makeImplies(*Comp, A.makeImplies(RHSProps.Pos->formula(),
LHSProps.Pos->formula())));
break;
@@ -215,14 +215,14 @@ void transferUnaryMinus(const UnaryOperator *UO,
return;
// a is pos ==> -a is neg
- State.Env.addToFlowCondition(
+ State.Env.assume(
A.makeImplies(OperandProps.Pos->formula(), UnaryOpProps.Neg->formula()));
// a is neg ==> -a is pos
- State.Env.addToFlowCondition(
+ State.Env.assume(
A.makeImplies(OperandProps.Neg->formula(), UnaryOpProps.Pos->formula()));
// a is zero ==> -a is zero
- State.Env.addToFlowCondition(A.makeImplies(OperandProps.Zero->formula(),
- UnaryOpProps.Zero->formula()));
+ State.Env.assume(A.makeImplies(OperandProps.Zero->formula(),
+ UnaryOpProps.Zero->formula()));
}
void transferUnaryNot(const UnaryOperator *UO,
@@ -235,7 +235,7 @@ void transferUnaryNot(const UnaryOperator *UO,
return;
// a is neg or pos ==> !a is zero
- State.Env.addToFlowCondition(A.makeImplies(
+ State.Env.assume(A.makeImplies(
A.makeOr(OperandProps.Pos->formula(), OperandProps.Neg->formula()),
UnaryOpProps.Zero->formula()));
@@ -243,11 +243,11 @@ void transferUnaryNot(const UnaryOperator *UO,
// put the generic handler, transferExpr maybe?
if (auto *UOBoolVal = dyn_cast<BoolValue>(UnaryOpValue)) {
// !a <==> a is zero
- State.Env.addToFlowCondition(
+ State.Env.assume(
A.makeEquals(UOBoolVal->formula(), OperandProps.Zero->formula()));
// !a <==> !a is not zero
- State.Env.addToFlowCondition(A.makeEquals(
- UOBoolVal->formula(), A.makeNot(UnaryOpProps.Zero->formula())));
+ State.Env.assume(A.makeEquals(UOBoolVal->formula(),
+ A.makeNot(UnaryOpProps.Zero->formula())));
}
}
@@ -391,11 +391,10 @@ BoolValue &mergeBoolValues(BoolValue &Bool1, const Environment &Env1,
// path taken - this simplifies the flow condition tracked in `MergedEnv`.
// Otherwise, information about which path was taken is used to associate
// `MergedBool` with `Bool1` and `Bool2`.
- if (Env1.flowConditionImplies(B1) && Env2.flowConditionImplies(B2)) {
- MergedEnv.addToFlowCondition(MergedBool.formula());
- } else if (Env1.flowConditionImplies(A.makeNot(B1)) &&
- Env2.flowConditionImplies(A.makeNot(B2))) {
- MergedEnv.addToFlowCondition(A.makeNot(MergedBool.formula()));
+ if (Env1.proves(B1) && Env2.proves(B2)) {
+ MergedEnv.assume(MergedBool.formula());
+ } else if (Env1.proves(A.makeNot(B1)) && Env2.proves(A.makeNot(B2))) {
+ MergedEnv.assume(A.makeNot(MergedBool.formula()));
}
return MergedBool;
}
@@ -484,7 +483,7 @@ testing::AssertionResult isPropertyImplied(const Environment &Env,
if (!Prop)
return Result;
auto *BVProp = cast<BoolValue>(Prop);
- if (Env.flowConditionImplies(BVProp->formula()) != Implies)
+ if (Env.proves(BVProp->formula()) != Implies)
return testing::AssertionFailure()
<< Property << " is " << (Implies ? "not" : "") << " implied"
<< ", but should " << (Implies ? "" : "not ") << "be";
diff --git a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
index 0c2106777560ee6..0f9f13df817075e 100644
--- a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
@@ -3795,11 +3795,10 @@ TEST(TransferTest, BooleanEquality) {
ASSERT_THAT(BarDecl, NotNull());
auto &BarValThen = getFormula(*BarDecl, EnvThen);
- EXPECT_TRUE(EnvThen.flowConditionImplies(BarValThen));
+ EXPECT_TRUE(EnvThen.proves(BarValThen));
auto &BarValElse = getFormula(*BarDecl, EnvElse);
- EXPECT_TRUE(
- EnvElse.flowConditionImplies(EnvElse.arena().makeNot(BarValElse)));
+ EXPECT_TRUE(EnvElse.proves(EnvElse.arena().makeNot(BarValElse)));
});
}
@@ -3830,11 +3829,10 @@ TEST(TransferTest, BooleanInequality) {
ASSERT_THAT(BarDecl, NotNull());
auto &BarValThen = getFormula(*BarDecl, EnvThen);
- EXPECT_TRUE(
- EnvThen.flowConditionImplies(EnvThen.arena().makeNot(BarValThen)));
+ EXPECT_TRUE(EnvThen.proves(EnvThen.arena().makeNot(BarValThen)));
auto &BarValElse = getFormula(*BarDecl, EnvElse);
- EXPECT_TRUE(EnvElse.flowConditionImplies(BarValElse));
+ EXPECT_TRUE(EnvElse.proves(BarValElse));
});
}
@@ -3853,7 +3851,7 @@ TEST(TransferTest, IntegerLiteralEquality) {
auto &Equal =
getValueForDecl<BoolValue>(ASTCtx, Env, "equal").formula();
- EXPECT_TRUE(Env.flowConditionImplies(Equal));
+ EXPECT_TRUE(Env.proves(Equal));
});
}
@@ -3890,19 +3888,19 @@ TEST(TransferTest, CorrelatedBranches) {
ASSERT_THAT(BDecl, NotNull());
auto &BVal = getFormula(*BDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(BVal)));
+ EXPECT_TRUE(Env.proves(Env.arena().makeNot(BVal)));
}
{
const Environment &Env = getEnvironmentAtAnnotation(Results, "p1");
auto &CVal = getFormula(*CDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(CVal));
+ EXPECT_TRUE(Env.proves(CVal));
}
{
const Environment &Env = getEnvironmentAtAnnotation(Results, "p2");
auto &CVal = getFormula(*CDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(CVal));
+ EXPECT_TRUE(Env.proves(CVal));
}
});
}
@@ -3934,7 +3932,7 @@ TEST(TransferTest, LoopWithAssignmentConverges) {
ASSERT_THAT(BarDecl, NotNull());
auto &BarVal = getFormula(*BarDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(BarVal)));
+ EXPECT_TRUE(Env.proves(Env.arena().makeNot(BarVal)));
});
}
@@ -3967,12 +3965,11 @@ TEST(TransferTest, LoopWithStagedAssignments) {
auto &BarVal = getFormula(*BarDecl, Env);
auto &ErrVal = getFormula(*ErrDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(BarVal));
+ EXPECT_TRUE(Env.proves(BarVal));
// An unsound analysis, for example only evaluating the loop once, can
// conclude that `Err` is false. So, we test that this conclusion is not
// reached.
- EXPECT_FALSE(
- Env.flowConditionImplies(Env.arena().makeNot(ErrVal)));
+ EXPECT_FALSE(Env.proves(Env.arena().makeNot(ErrVal)));
});
}
@@ -4002,7 +3999,7 @@ TEST(TransferTest, LoopWithReferenceAssignmentConverges) {
ASSERT_THAT(BarDecl, NotNull());
auto &BarVal = getFormula(*BarDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(BarVal)));
+ EXPECT_TRUE(Env.proves(Env.arena().makeNot(BarVal)));
});
}
@@ -4531,11 +4528,10 @@ TEST(TransferTest, IfStmtBranchExtendsFlowCondition) {
ASSERT_THAT(FooDecl, NotNull());
auto &ThenFooVal= getFormula(*FooDecl, ThenEnv);
- EXPECT_TRUE(ThenEnv.flowConditionImplies(ThenFooVal));
+ EXPECT_TRUE(ThenEnv.proves(ThenFooVal));
auto &ElseFooVal = getFormula(*FooDecl, ElseEnv);
- EXPECT_TRUE(
- ElseEnv.flowConditionImplies(ElseEnv.arena().makeNot(ElseFooVal)));
+ EXPECT_TRUE(ElseEnv.proves(ElseEnv.arena().makeNot(ElseFooVal)));
});
}
@@ -4565,11 +4561,11 @@ TEST(TransferTest, WhileStmtBranchExtendsFlowCondition) {
ASSERT_THAT(FooDecl, NotNull());
auto &LoopBodyFooVal = getFormula(*FooDecl, LoopBodyEnv);
- EXPECT_TRUE(LoopBodyEnv.flowConditionImplies(LoopBodyFooVal));
+ EXPECT_TRUE(LoopBodyEnv.proves(LoopBodyFooVal));
auto &AfterLoopFooVal = getFormula(*FooDecl, AfterLoopEnv);
- EXPECT_TRUE(AfterLoopEnv.flowConditionImplies(
- AfterLoopEnv.arena().makeNot(AfterLoopFooVal)));
+ EXPECT_TRUE(
+ AfterLoopEnv.proves(AfterLoopEnv.arena().makeNot(AfterLoopFooVal)));
});
}
@@ -4606,15 +4602,13 @@ TEST(TransferTest, DoWhileStmtBranchExtendsFlowCondition) {
auto &LoopBodyFooVal= getFormula(*FooDecl, LoopBodyEnv);
auto &LoopBodyBarVal = getFormula(*BarDecl, LoopBodyEnv);
- EXPECT_TRUE(LoopBodyEnv.flowConditionImplies(
- A.makeOr(LoopBodyBarVal, LoopBodyFooVal)));
+ EXPECT_TRUE(
+ LoopBodyEnv.proves(A.makeOr(LoopBodyBarVal, LoopBodyFooVal)));
auto &AfterLoopFooVal = getFormula(*FooDecl, AfterLoopEnv);
auto &AfterLoopBarVal = getFormula(*BarDecl, AfterLoopEnv);
- EXPECT_TRUE(
- AfterLoopEnv.flowConditionImplies(A.makeNot(AfterLoopFooVal)));
- EXPECT_TRUE(
- AfterLoopEnv.flowConditionImplies(A.makeNot(AfterLoopBarVal)));
+ EXPECT_TRUE(AfterLoopEnv.proves(A.makeNot(AfterLoopFooVal)));
+ EXPECT_TRUE(AfterLoopEnv.proves(A.makeNot(AfterLoopBarVal)));
});
}
@@ -4644,11 +4638,11 @@ TEST(TransferTest, ForStmtBranchExtendsFlowCondition) {
ASSERT_THAT(FooDecl, NotNull());
auto &LoopBodyFooVal= getFormula(*FooDecl, LoopBodyEnv);
- EXPECT_TRUE(LoopBodyEnv.flowConditionImplies(LoopBodyFooVal));
+ EXPECT_TRUE(LoopBodyEnv.proves(LoopBodyFooVal));
auto &AfterLoopFooVal = getFormula(*FooDecl, AfterLoopEnv);
- EXPECT_TRUE(AfterLoopEnv.flowConditionImplies(
- AfterLoopEnv.arena().makeNot(AfterLoopFooVal)));
+ EXPECT_TRUE(
+ AfterLoopEnv.proves(AfterLoopEnv.arena().makeNot(AfterLoopFooVal)));
});
}
@@ -4673,7 +4667,7 @@ TEST(TransferTest, ForStmtBranchWithoutConditionDoesNotExtendFlowCondition) {
ASSERT_THAT(FooDecl, NotNull());
auto &LoopBodyFooVal= getFormula(*FooDecl, LoopBodyEnv);
- EXPECT_FALSE(LoopBodyEnv.flowConditionImplies(LoopBodyFooVal));
+ EXPECT_FALSE(LoopBodyEnv.proves(LoopBodyFooVal));
});
}
@@ -4699,8 +4693,8 @@ TEST(TransferTest, ContextSensitiveOptionDisabled) {
ASSERT_THAT(FooDecl, NotNull());
auto &FooVal = getFormula(*FooDecl, Env);
- EXPECT_FALSE(Env.flowConditionImplies(FooVal));
- EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
+ EXPECT_FALSE(Env.proves(FooVal));
+ EXPECT_FALSE(Env.proves(Env.arena().makeNot(FooVal)));
},
{BuiltinOptions{/*.ContextSensitiveOpts=*/std::nullopt}});
}
@@ -4838,8 +4832,8 @@ TEST(TransferTest, ContextSensitiveDepthZero) {
ASSERT_THAT(FooDecl, NotNull());
auto &FooVal = getFormula(*FooDecl, Env);
- EXPECT_FALSE(Env.flowConditionImplies(FooVal));
- EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
+ EXPECT_FALSE(Env.proves(FooVal));
+ EXPECT_FALSE(Env.proves(Env.arena().makeNot(FooVal)));
},
{BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/0}}});
}
@@ -4866,7 +4860,7 @@ TEST(TransferTest, ContextSensitiveSetTrue) {
ASSERT_THAT(FooDecl, NotNull());
auto &FooVal = getFormula(*FooDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(FooVal));
+ EXPECT_TRUE(Env.proves(FooVal));
},
{BuiltinOptions{ContextSensitiveOptions{}}});
}
@@ -4893,7 +4887,7 @@ TEST(TransferTest, ContextSensitiveSetFalse) {
ASSERT_THAT(FooDecl, NotNull());
auto &FooVal = getFormula(*FooDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
+ EXPECT_TRUE(Env.proves(Env.arena().makeNot(FooVal)));
},
{BuiltinOptions{ContextSensitiveOptions{}}});
}
@@ -4926,12 +4920,12 @@ TEST(TransferTest, ContextSensitiveSetBothTrueAndFalse) {
ASSERT_THAT(BarDecl, NotNull());
auto &FooVal = getFormula(*FooDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(FooVal));
- EXPECT_FALSE(Env.flowConditionImplies(A.makeNot(FooVal)));
+ EXPECT_TRUE(Env.proves(FooVal));
+ EXPECT_FALSE(Env.proves(A.makeNot(FooVal)));
auto &BarVal = getFormula(*BarDecl, Env);
- EXPECT_FALSE(Env.flowConditionImplies(BarVal));
- EXPECT_TRUE(Env.flowConditionImplies(A.makeNot(BarVal)));
+ EXPECT_FALSE(Env.proves(BarVal));
+ EXPECT_TRUE(Env.proves(A.makeNot(BarVal)));
},
{BuiltinOptions{ContextSensitiveOptions{}}});
}
@@ -4959,8 +4953,8 @@ TEST(TransferTest, ContextSensitiveSetTwoLayersDepthOne) {
ASSERT_THAT(FooDecl, NotNull());
auto &FooVal = getFormula(*FooDecl, Env);
- EXPECT_FALSE(Env.flowConditionImplies(FooVal));
- EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
+ EXPECT_FALSE(Env.proves(FooVal));
+ EXPECT_FALSE(Env.proves(Env.arena().makeNot(FooVal)));
},
{BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/1}}});
}
@@ -4988,7 +4982,7 @@ TEST(TransferTest, ContextSensitiveSetTwoLayersDepthTwo) {
ASSERT_THAT(FooDecl, NotNull());
auto &FooVal = getFormula(*FooDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(FooVal));
+ EXPECT_TRUE(Env.proves(FooVal));
},
{BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/2}}});
}
@@ -5017,8 +5011,8 @@ TEST(TransferTest, ContextSensitiveSetThreeLayersDepthTwo) {
ASSERT_THAT(FooDecl, NotNull());
auto &FooVal = getFormula(*FooDecl, Env);
- EXPECT_FALSE(Env.flowConditionImplies(FooVal));
- EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
+ EXPECT_FALSE(Env.proves(FooVal));
+ EXPECT_FALSE(Env.proves(Env.arena().makeNot(FooVal)));
},
{BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/2}}});
}
@@ -5047,7 +5041,7 @@ TEST(TransferTest, ContextSensitiveSetThreeLayersDepthThree) {
ASSERT_THAT(FooDecl, NotNull());
auto &FooVal = getFormula(*FooDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(FooVal));
+ EXPECT_TRUE(Env.proves(FooVal));
},
{BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/3}}});
}
@@ -5090,8 +5084,8 @@ TEST(TransferTest, ContextSensitiveMutualRecursion) {
auto &FooVal = getFormula(*FooDecl, Env);
// ... but it also can't prove anything here.
- EXPECT_FALSE(Env.flowConditionImplies(FooVal));
- EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
+ EXPECT_FALSE(Env.proves(FooVal));
+ EXPECT_FALSE(Env.proves(Env.arena().makeNot(FooVal)));
},
{BuiltinOptions{ContextSensitiveOptions{/*.Depth=*/4}}});
}
@@ -5124,12 +5118,12 @@ TEST(TransferTest, ContextSensitiveSetMultipleLines) {
ASSERT_THAT(BarDecl, NotNull());
auto &FooVal = getFormula(*FooDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(FooVal));
- EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
+ EXPECT_TRUE(Env.proves(FooVal));
+ EXPECT_FALSE(Env.proves(Env.arena().makeNot(FooVal)));
auto &BarVal = getFormula(*BarDecl, Env);
- EXPECT_FALSE(Env.flowConditionImplies(BarVal));
- EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(BarVal)));
+ EXPECT_FALSE(Env.proves(BarVal));
+ EXPECT_TRUE(Env.proves(Env.arena().makeNot(BarVal)));
},
{BuiltinOptions{ContextSensitiveOptions{}}});
}
@@ -5166,12 +5160,12 @@ TEST(TransferTest, ContextSensitiveSetMultipleBlocks) {
ASSERT_THAT(BazDecl, NotNull());
auto &BarVal = getFormula(*BarDecl, Env);
- EXPECT_FALSE(Env.flowConditionImplies(BarVal));
- EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(BarVal)));
+ EXPECT_FALSE(Env.proves(BarVal));
+ EXPECT_TRUE(Env.proves(Env.arena().makeNot(BarVal)));
auto &BazVal = getFormula(*BazDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(BazVal));
- EXPECT_FALSE(Env.flowConditionImplies(Env.arena().makeNot(BazVal)));
+ EXPECT_TRUE(Env.proves(BazVal));
+ EXPECT_FALSE(Env.proves(Env.arena().makeNot(BazVal)));
},
{BuiltinOptions{ContextSensitiveOptions{}}});
}
@@ -5215,7 +5209,7 @@ TEST(TransferTest, ContextSensitiveReturnTrue) {
ASSERT_THAT(FooDecl, NotNull());
auto &FooVal = getFormula(*FooDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(FooVal));
+ EXPECT_TRUE(Env.proves(FooVal));
},
{BuiltinOptions{ContextSensitiveOptions{}}});
}
@@ -5240,7 +5234,7 @@ TEST(TransferTest, ContextSensitiveReturnFalse) {
ASSERT_THAT(FooDecl, NotNull());
auto &FooVal = getFormula(*FooDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(Env.arena().makeNot(FooVal)));
+ EXPECT_TRUE(Env.proves(Env.arena().makeNot(FooVal)));
},
{BuiltinOptions{ContextSensitiveOptions{}}});
}
@@ -5268,7 +5262,7 @@ TEST(TransferTest, ContextSensitiveReturnArg) {
ASSERT_THAT(BazDecl, NotNull());
auto &BazVal = getFormula(*BazDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(BazVal));
+ EXPECT_TRUE(Env.proves(BazVal));
},
{BuiltinOptions{ContextSensitiveOptions{}}});
}
@@ -5316,7 +5310,7 @@ TEST(TransferTest, ContextSensitiveMethodLiteral) {
ASSERT_THAT(FooDecl, NotNull());
auto &FooVal = getFormula(*FooDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(FooVal));
+ EXPECT_TRUE(Env.proves(FooVal));
},
{BuiltinOptions{ContextSensitiveOptions{}}});
}
@@ -5348,7 +5342,7 @@ TEST(TransferTest, ContextSensitiveMethodGetter) {
ASSERT_THAT(FooDecl, NotNull());
auto &FooVal = getFormula(*FooDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(FooVal));
+ EXPECT_TRUE(Env.proves(FooVal));
},
{BuiltinOptions{ContextSensitiveOptions{}}});
}
@@ -5380,7 +5374,7 @@ TEST(TransferTest, ContextSensitiveMethodSetter) {
ASSERT_THAT(FooDecl, NotNull());
auto &FooVal = getFormula(*FooDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(FooVal));
+ EXPECT_TRUE(Env.proves(FooVal));
},
{BuiltinOptions{ContextSensitiveOptions{}}});
}
@@ -5414,7 +5408,7 @@ TEST(TransferTest, ContextSensitiveMethodGetterAndSetter) {
ASSERT_THAT(FooDecl, NotNull());
auto &FooVal = getFormula(*FooDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(FooVal));
+ EXPECT_TRUE(Env.proves(FooVal));
},
{BuiltinOptions{ContextSensitiveOptions{}}});
}
@@ -5449,7 +5443,7 @@ TEST(TransferTest, ContextSensitiveMethodTwoLayersVoid) {
ASSERT_THAT(FooDecl, NotNull());
auto &FooVal = getFormula(*FooDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(FooVal));
+ EXPECT_TRUE(Env.proves(FooVal));
},
{BuiltinOptions{ContextSensitiveOptions{}}});
}
@@ -5483,7 +5477,7 @@ TEST(TransferTest, ContextSensitiveMethodTwoLayersReturn) {
ASSERT_THAT(FooDecl, NotNull());
auto &FooVal = getFormula(*FooDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(FooVal));
+ EXPECT_TRUE(Env.proves(FooVal));
},
{BuiltinOptions{ContextSensitiveOptions{}}});
}
@@ -5514,7 +5508,7 @@ TEST(TransferTest, ContextSensitiveConstructorBody) {
ASSERT_THAT(FooDecl, NotNull());
auto &FooVal = getFormula(*FooDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(FooVal));
+ EXPECT_TRUE(Env.proves(FooVal));
},
{BuiltinOptions{ContextSensitiveOptions{}}});
}
@@ -5545,7 +5539,7 @@ TEST(TransferTest, ContextSensitiveConstructorInitializer) {
ASSERT_THAT(FooDecl, NotNull());
auto &FooVal = getFormula(*FooDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(FooVal));
+ EXPECT_TRUE(Env.proves(FooVal));
},
{BuiltinOptions{ContextSensitiveOptions{}}});
}
@@ -5576,7 +5570,7 @@ TEST(TransferTest, ContextSensitiveConstructorDefault) {
ASSERT_THAT(FooDecl, NotNull());
auto &FooVal = getFormula(*FooDecl, Env);
- EXPECT_TRUE(Env.flowConditionImplies(FooVal));
+ EXPECT_TRUE(Env.proves(FooVal));
},
{BuiltinOptions{ContextSensitiveOptions{}}});
}
@@ -5656,7 +5650,7 @@ TEST(TransferTest, ChainedLogicalOps) {
ASTContext &ASTCtx) {
const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
auto &B = getValueForDecl<BoolValue>(ASTCtx, Env, "b").formula();
- EXPECT_TRUE(Env.flowConditionImplies(B));
+ EXPECT_TRUE(Env.proves(B));
});
}
@@ -5701,30 +5695,30 @@ TEST(TransferTest, NoReturnFunctionInsideShortCircuitedBooleanOp) {
auto &A = Env.arena();
// Check that [[p]] is reachable with a non-false flow condition.
- EXPECT_FALSE(Env.flowConditionImplies(A.makeLiteral(false)));
+ EXPECT_FALSE(Env.proves(A.makeLiteral(false)));
auto &B1 = getValueForDecl<BoolValue>(ASTCtx, Env, "b1").formula();
- EXPECT_TRUE(Env.flowConditionImplies(A.makeNot(B1)));
+ EXPECT_TRUE(Env.proves(A.makeNot(B1)));
auto &NoreturnOnRhsOfAnd =
getValueForDecl<BoolValue>(ASTCtx, Env, "NoreturnOnRhsOfAnd").formula();
- EXPECT_TRUE(Env.flowConditionImplies(A.makeNot(NoreturnOnRhsOfAnd)));
+ EXPECT_TRUE(Env.proves(A.makeNot(NoreturnOnRhsOfAnd)));
auto &B2 = getValueForDecl<BoolValue>(ASTCtx, Env, "b2").formula();
- EXPECT_TRUE(Env.flowConditionImplies(B2));
+ EXPECT_TRUE(Env.proves(B2));
auto &NoreturnOnRhsOfOr =
getValueForDecl<BoolValue>(ASTCtx, Env, "NoreturnOnRhsOfOr")
.formula();
- EXPECT_TRUE(Env.flowConditionImplies(NoreturnOnRhsOfOr));
+ EXPECT_TRUE(Env.proves(NoreturnOnRhsOfOr));
auto &NoreturnOnLhsMakesAndUnreachable = getValueForDecl<BoolValue>(
ASTCtx, Env, "NoreturnOnLhsMakesAndUnreachable").formula();
- EXPECT_TRUE(Env.flowConditionImplies(NoreturnOnLhsMakesAndUnreachable));
+ EXPECT_TRUE(Env.proves(NoreturnOnLhsMakesAndUnreachable));
auto &NoreturnOnLhsMakesOrUnreachable = getValueForDecl<BoolValue>(
ASTCtx, Env, "NoreturnOnLhsMakesOrUnreachable").formula();
- EXPECT_TRUE(Env.flowConditionImplies(NoreturnOnLhsMakesOrUnreachable));
+ EXPECT_TRUE(Env.proves(NoreturnOnLhsMakesOrUnreachable));
});
}
@@ -5944,7 +5938,7 @@ TEST(TransferTest, AnonymousStruct) {
S->getChild(*cast<ValueDecl>(IndirectField->chain().front())));
auto *B = cast<BoolValue>(getFieldValue(&AnonStruct, *BDecl, Env));
- ASSERT_TRUE(Env.flowConditionImplies(B->formula()));
+ ASSERT_TRUE(Env.proves(B->formula()));
});
}
@@ -5975,7 +5969,7 @@ TEST(TransferTest, AnonymousStructWithInitializer) {
*cast<ValueDecl>(IndirectField->chain().front())));
auto *B = cast<BoolValue>(getFieldValue(&AnonStruct, *BDecl, Env));
- ASSERT_TRUE(Env.flowConditionImplies(B->formula()));
+ ASSERT_TRUE(Env.proves(B->formula()));
});
}
diff --git a/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp b/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
index 8422f3804db5494..e33bea47137ad73 100644
--- a/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
@@ -450,8 +450,7 @@ class SpecialBoolAnalysis final
if (IsSet2 == nullptr)
return ComparisonResult::Different;
- return Env1.flowConditionImplies(IsSet1->formula()) ==
- Env2.flowConditionImplies(IsSet2->formula())
+ return Env1.proves(IsSet1->formula()) == Env2.proves(IsSet2->formula())
? ComparisonResult::Same
: ComparisonResult::Different;
}
@@ -475,9 +474,8 @@ class SpecialBoolAnalysis final
auto &IsSet = MergedEnv.makeAtomicBoolValue();
MergedVal.setProperty("is_set", IsSet);
- if (Env1.flowConditionImplies(IsSet1->formula()) &&
- Env2.flowConditionImplies(IsSet2->formula()))
- MergedEnv.addToFlowCondition(IsSet.formula());
+ if (Env1.proves(IsSet1->formula()) && Env2.proves(IsSet2->formula()))
+ MergedEnv.assume(IsSet.formula());
return true;
}
@@ -544,10 +542,10 @@ TEST_F(JoinFlowConditionsTest, JoinDistinctButProvablyEquivalentValues) {
->formula();
};
- EXPECT_FALSE(Env1.flowConditionImplies(GetFoo(Env1)));
- EXPECT_TRUE(Env2.flowConditionImplies(GetFoo(Env2)));
- EXPECT_TRUE(Env3.flowConditionImplies(GetFoo(Env3)));
- EXPECT_TRUE(Env4.flowConditionImplies(GetFoo(Env4)));
+ EXPECT_FALSE(Env1.proves(GetFoo(Env1)));
+ EXPECT_TRUE(Env2.proves(GetFoo(Env2)));
+ EXPECT_TRUE(Env3.proves(GetFoo(Env3)));
+ EXPECT_TRUE(Env4.proves(GetFoo(Env4)));
});
}
@@ -849,11 +847,11 @@ TEST_F(FlowConditionTest, IfStmtSingleVar) {
const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula();
- EXPECT_TRUE(Env1.flowConditionImplies(FooVal1));
+ EXPECT_TRUE(Env1.proves(FooVal1));
const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula();
- EXPECT_FALSE(Env2.flowConditionImplies(FooVal2));
+ EXPECT_FALSE(Env2.proves(FooVal2));
});
}
@@ -880,11 +878,11 @@ TEST_F(FlowConditionTest, IfStmtSingleNegatedVar) {
const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula();
- EXPECT_FALSE(Env1.flowConditionImplies(FooVal1));
+ EXPECT_FALSE(Env1.proves(FooVal1));
const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula();
- EXPECT_TRUE(Env2.flowConditionImplies(FooVal2));
+ EXPECT_TRUE(Env2.proves(FooVal2));
});
}
@@ -908,7 +906,7 @@ TEST_F(FlowConditionTest, WhileStmt) {
const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
auto &FooVal = cast<BoolValue>(Env.getValue(*FooDecl))->formula();
- EXPECT_TRUE(Env.flowConditionImplies(FooVal));
+ EXPECT_TRUE(Env.proves(FooVal));
});
}
@@ -931,7 +929,7 @@ TEST_F(FlowConditionTest, WhileStmtWithAssignmentInCondition) {
ASTContext &ASTCtx) {
const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
auto &FooVal = getValueForDecl<BoolValue>(ASTCtx, Env, "Foo").formula();
- EXPECT_TRUE(Env.flowConditionImplies(FooVal));
+ EXPECT_TRUE(Env.proves(FooVal));
});
}
@@ -961,14 +959,14 @@ TEST_F(FlowConditionTest, Conjunction) {
const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula();
auto &BarVal1 = cast<BoolValue>(Env1.getValue(*BarDecl))->formula();
- EXPECT_TRUE(Env1.flowConditionImplies(FooVal1));
- EXPECT_TRUE(Env1.flowConditionImplies(BarVal1));
+ EXPECT_TRUE(Env1.proves(FooVal1));
+ EXPECT_TRUE(Env1.proves(BarVal1));
const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula();
auto &BarVal2 = cast<BoolValue>(Env2.getValue(*BarDecl))->formula();
- EXPECT_FALSE(Env2.flowConditionImplies(FooVal2));
- EXPECT_FALSE(Env2.flowConditionImplies(BarVal2));
+ EXPECT_FALSE(Env2.proves(FooVal2));
+ EXPECT_FALSE(Env2.proves(BarVal2));
});
}
@@ -998,14 +996,14 @@ TEST_F(FlowConditionTest, Disjunction) {
const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula();
auto &BarVal1 = cast<BoolValue>(Env1.getValue(*BarDecl))->formula();
- EXPECT_FALSE(Env1.flowConditionImplies(FooVal1));
- EXPECT_FALSE(Env1.flowConditionImplies(BarVal1));
+ EXPECT_FALSE(Env1.proves(FooVal1));
+ EXPECT_FALSE(Env1.proves(BarVal1));
const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula();
auto &BarVal2 = cast<BoolValue>(Env2.getValue(*BarDecl))->formula();
- EXPECT_FALSE(Env2.flowConditionImplies(FooVal2));
- EXPECT_FALSE(Env2.flowConditionImplies(BarVal2));
+ EXPECT_FALSE(Env2.proves(FooVal2));
+ EXPECT_FALSE(Env2.proves(BarVal2));
});
}
@@ -1035,14 +1033,14 @@ TEST_F(FlowConditionTest, NegatedConjunction) {
const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula();
auto &BarVal1 = cast<BoolValue>(Env1.getValue(*BarDecl))->formula();
- EXPECT_FALSE(Env1.flowConditionImplies(FooVal1));
- EXPECT_FALSE(Env1.flowConditionImplies(BarVal1));
+ EXPECT_FALSE(Env1.proves(FooVal1));
+ EXPECT_FALSE(Env1.proves(BarVal1));
const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula();
auto &BarVal2 = cast<BoolValue>(Env2.getValue(*BarDecl))->formula();
- EXPECT_TRUE(Env2.flowConditionImplies(FooVal2));
- EXPECT_TRUE(Env2.flowConditionImplies(BarVal2));
+ EXPECT_TRUE(Env2.proves(FooVal2));
+ EXPECT_TRUE(Env2.proves(BarVal2));
});
}
@@ -1072,14 +1070,14 @@ TEST_F(FlowConditionTest, DeMorgan) {
const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula();
auto &BarVal1 = cast<BoolValue>(Env1.getValue(*BarDecl))->formula();
- EXPECT_TRUE(Env1.flowConditionImplies(FooVal1));
- EXPECT_TRUE(Env1.flowConditionImplies(BarVal1));
+ EXPECT_TRUE(Env1.proves(FooVal1));
+ EXPECT_TRUE(Env1.proves(BarVal1));
const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula();
auto &BarVal2 = cast<BoolValue>(Env2.getValue(*BarDecl))->formula();
- EXPECT_FALSE(Env2.flowConditionImplies(FooVal2));
- EXPECT_FALSE(Env2.flowConditionImplies(BarVal2));
+ EXPECT_FALSE(Env2.proves(FooVal2));
+ EXPECT_FALSE(Env2.proves(BarVal2));
});
}
@@ -1108,7 +1106,7 @@ TEST_F(FlowConditionTest, Join) {
const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
auto &FooVal = cast<BoolValue>(Env.getValue(*FooDecl))->formula();
- EXPECT_TRUE(Env.flowConditionImplies(FooVal));
+ EXPECT_TRUE(Env.proves(FooVal));
});
}
@@ -1142,7 +1140,7 @@ TEST_F(FlowConditionTest, OpaqueFlowConditionMergesToOpaqueBool) {
auto &BarVal = cast<BoolValue>(Env.getValue(*BarDecl))->formula();
- EXPECT_FALSE(Env.flowConditionImplies(BarVal));
+ EXPECT_FALSE(Env.proves(BarVal));
});
}
@@ -1183,7 +1181,7 @@ TEST_F(FlowConditionTest, OpaqueFieldFlowConditionMergesToOpaqueBool) {
auto &BarVal = cast<BoolValue>(Env.getValue(*BarDecl))->formula();
- EXPECT_FALSE(Env.flowConditionImplies(BarVal));
+ EXPECT_FALSE(Env.proves(BarVal));
});
}
@@ -1217,7 +1215,7 @@ TEST_F(FlowConditionTest, OpaqueFlowConditionInsideBranchMergesToOpaqueBool) {
auto &BarVal = cast<BoolValue>(Env.getValue(*BarDecl))->formula();
- EXPECT_FALSE(Env.flowConditionImplies(BarVal));
+ EXPECT_FALSE(Env.proves(BarVal));
});
}
@@ -1245,11 +1243,11 @@ TEST_F(FlowConditionTest, PointerToBoolImplicitCast) {
const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
auto &FooVal1 = cast<BoolValue>(Env1.getValue(*FooDecl))->formula();
- EXPECT_TRUE(Env1.flowConditionImplies(FooVal1));
+ EXPECT_TRUE(Env1.proves(FooVal1));
const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
auto &FooVal2 = cast<BoolValue>(Env2.getValue(*FooDecl))->formula();
- EXPECT_FALSE(Env2.flowConditionImplies(FooVal2));
+ EXPECT_FALSE(Env2.proves(FooVal2));
});
}
@@ -1585,7 +1583,7 @@ TEST_F(TopTest, TopUsedInBothBranchesWithoutPrecisionLoss) {
auto *BarVal = dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl));
ASSERT_THAT(BarVal, NotNull());
- EXPECT_TRUE(Env.flowConditionImplies(
+ EXPECT_TRUE(Env.proves(
Env.arena().makeEquals(FooVal->formula(), BarVal->formula())));
});
}
More information about the cfe-commits
mailing list