llvm/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h

//===- Z3CrosscheckVisitor.h - Crosscheck reports with Z3 -------*- C++ -*-===//
//
// 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
//
//===----------------------------------------------------------------------===//
//
//  This file defines the visitor and utilities around it for Z3 report
//  refutation.
//
//===----------------------------------------------------------------------===//

#ifndef LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H
#define LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H

#include "clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h"

namespace clang::ento {

/// The bug visitor will walk all the nodes in a path and collect all the
/// constraints. When it reaches the root node, will create a refutation
/// manager and check if the constraints are satisfiable.
class Z3CrosscheckVisitor final : public BugReporterVisitor { … };

/// The oracle will decide if a report should be accepted or rejected based on
/// the results of the Z3 solver and the statistics of the queries of a report
/// equivalenece class.
class Z3CrosscheckOracle { … };

} // namespace clang::ento

#endif // LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H