[analyzer][Z3][NFC] Use GTEST_SKIP instead of hacks
Since @bkramer bumped gtest to 1.10.0 I think it's a good time to clean up some of my hacks. Reviewed By: Szelethus Differential Revision: https://reviews.llvm.org/D102643
This commit is contained in:
parent
7eb85cdb10
commit
3febf0b507
|
@ -19,13 +19,6 @@
|
||||||
#include "llvm/Config/llvm-config.h"
|
#include "llvm/Config/llvm-config.h"
|
||||||
#include "gtest/gtest.h"
|
#include "gtest/gtest.h"
|
||||||
|
|
||||||
// FIXME: Use GTEST_SKIP() instead if GTest is updated to version 1.10.0
|
|
||||||
#ifdef LLVM_WITH_Z3
|
|
||||||
#define SKIP_WITHOUT_Z3
|
|
||||||
#else
|
|
||||||
#define SKIP_WITHOUT_Z3 return
|
|
||||||
#endif
|
|
||||||
|
|
||||||
namespace clang {
|
namespace clang {
|
||||||
namespace ento {
|
namespace ento {
|
||||||
namespace {
|
namespace {
|
||||||
|
@ -101,6 +94,15 @@ void addFalsePositiveGenerator(AnalysisASTConsumer &AnalysisConsumer,
|
||||||
});
|
});
|
||||||
}
|
}
|
||||||
|
|
||||||
|
class FalsePositiveRefutationBRVisitorTestBase : public testing::Test {
|
||||||
|
public:
|
||||||
|
void SetUp() override {
|
||||||
|
#ifndef LLVM_WITH_Z3
|
||||||
|
GTEST_SKIP() << "Requires the LLVM_ENABLE_Z3_SOLVER cmake option.";
|
||||||
|
#endif
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
// C++20 use constexpr below.
|
// C++20 use constexpr below.
|
||||||
const std::vector<std::string> LazyAssumeArgs{
|
const std::vector<std::string> LazyAssumeArgs{
|
||||||
"-Xclang", "-analyzer-config", "-Xclang", "eagerly-assume=false"};
|
"-Xclang", "-analyzer-config", "-Xclang", "eagerly-assume=false"};
|
||||||
|
@ -108,8 +110,7 @@ const std::vector<std::string> LazyAssumeAndCrossCheckArgs{
|
||||||
"-Xclang", "-analyzer-config", "-Xclang", "eagerly-assume=false",
|
"-Xclang", "-analyzer-config", "-Xclang", "eagerly-assume=false",
|
||||||
"-Xclang", "-analyzer-config", "-Xclang", "crosscheck-with-z3=true"};
|
"-Xclang", "-analyzer-config", "-Xclang", "crosscheck-with-z3=true"};
|
||||||
|
|
||||||
TEST(FalsePositiveRefutationBRVisitor, UnSatInTheMiddleNoReport) {
|
TEST_F(FalsePositiveRefutationBRVisitorTestBase, UnSatInTheMiddleNoReport) {
|
||||||
SKIP_WITHOUT_Z3;
|
|
||||||
constexpr auto Code = R"(
|
constexpr auto Code = R"(
|
||||||
void reachedWithContradiction();
|
void reachedWithContradiction();
|
||||||
void reachedWithNoContradiction();
|
void reachedWithNoContradiction();
|
||||||
|
@ -139,8 +140,8 @@ TEST(FalsePositiveRefutationBRVisitor, UnSatInTheMiddleNoReport) {
|
||||||
"test.FalsePositiveGenerator:REACHED_WITH_CONTRADICTION\n");
|
"test.FalsePositiveGenerator:REACHED_WITH_CONTRADICTION\n");
|
||||||
}
|
}
|
||||||
|
|
||||||
TEST(FalsePositiveRefutationBRVisitor, UnSatAtErrorNodeWithNewSymbolNoReport) {
|
TEST_F(FalsePositiveRefutationBRVisitorTestBase,
|
||||||
SKIP_WITHOUT_Z3;
|
UnSatAtErrorNodeWithNewSymbolNoReport) {
|
||||||
constexpr auto Code = R"(
|
constexpr auto Code = R"(
|
||||||
void reportIfCanBeTrue(bool);
|
void reportIfCanBeTrue(bool);
|
||||||
void reachedWithNoContradiction();
|
void reachedWithNoContradiction();
|
||||||
|
@ -170,9 +171,8 @@ TEST(FalsePositiveRefutationBRVisitor, UnSatAtErrorNodeWithNewSymbolNoReport) {
|
||||||
"test.FalsePositiveGenerator:CAN_BE_TRUE\n");
|
"test.FalsePositiveGenerator:CAN_BE_TRUE\n");
|
||||||
}
|
}
|
||||||
|
|
||||||
TEST(FalsePositiveRefutationBRVisitor,
|
TEST_F(FalsePositiveRefutationBRVisitorTestBase,
|
||||||
UnSatAtErrorNodeDueToRefinedConstraintNoReport) {
|
UnSatAtErrorNodeDueToRefinedConstraintNoReport) {
|
||||||
SKIP_WITHOUT_Z3;
|
|
||||||
constexpr auto Code = R"(
|
constexpr auto Code = R"(
|
||||||
void reportIfCanBeTrue(bool);
|
void reportIfCanBeTrue(bool);
|
||||||
void reachedWithNoContradiction();
|
void reachedWithNoContradiction();
|
||||||
|
|
Loading…
Reference in New Issue