llvm/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp

//===- unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp ----------------===//
//
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
// See https://llvm.org/LICENSE.txt for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
//===----------------------------------------------------------------------===//

#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h"
#include "gtest/gtest.h"

usingnamespaceclang;
usingnamespaceento;

Z3Result;
Z3Decision;

static constexpr Z3Decision AcceptReport = …;
static constexpr Z3Decision RejectReport = …;
static constexpr Z3Decision RejectEQClass = …;

static constexpr std::optional<bool> SAT = …;
static constexpr std::optional<bool> UNSAT = …;
static constexpr std::optional<bool> UNDEF = …;

static unsigned operator""_ms(unsigned long long ms) { … }
static unsigned operator""_step(unsigned long long rlimit) { … }

static const AnalyzerOptions DefaultOpts = …Config;
#define ANALYZER_OPTION_DEPENDS_ON_USER_MODE(TYPE, NAME, CMDFLAG, DESC,        \
                                             SHALLOW_VAL, DEEP_VAL)            \
  ANALYZER_OPTION(TYPE, NAME, CMDFLAG, DESC, DEEP_VAL)
#define ANALYZER_OPTION(TYPE, NAME, CMDFLAG, DESC, DEFAULT_VAL)                \
  Config.NAME = …;

namespace {

class Z3CrosscheckOracleTest : public testing::Test { … };

TEST_F(Z3CrosscheckOracleTest, AcceptsFirstSAT) { … }

TEST_F(Z3CrosscheckOracleTest, AcceptsSAT) { … }

TEST_F(Z3CrosscheckOracleTest, SATWhenItGoesOverTime) { … }

TEST_F(Z3CrosscheckOracleTest, UNSATWhenItGoesOverTime) { … }

TEST_F(Z3CrosscheckOracleTest, RejectsTimeout) { … }

TEST_F(Z3CrosscheckOracleTest, RejectsUNSATs) { … }

// Testing cut heuristics:
// =======================

TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfSpendsTooMuchTotalTime) { … }

TEST_F(Z3CrosscheckOracleTest, SATWhenItSpendsTooMuchTotalTime) { … }

TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfAttemptsManySmallQueries) { … }

TEST_F(Z3CrosscheckOracleTest, SATWhenIfAttemptsManySmallQueries) { … }

TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfExhaustsRLimit) { … }

TEST_F(Z3CrosscheckOracleTest, SATWhenItExhaustsRLimit) { … }

} // namespace