maxjhandsome
/
llvm-project
forked from OSchip/llvm-project
1
0
Fork 0
Code Issues Pull Requests Packages Releases Wiki Activity

[analyzer] Delete SMTContext. NFC. 

Summary: There is no reason to have a base class for a context anymore as each SMT object carries a reference to the specific solver context.

Reviewers: NoQ, george.karpenkov, hiraditya

Reviewed By: hiraditya

Subscribers: hiraditya, xazax.hun, szepet, a.sidorin, Szelethus

Differential Revision: https://reviews.llvm.org/D50768

llvm-svn: 340532
This commit is contained in:
Mikhail R. Gadelha 2018-08-23 13:20:18 +00:00
parent b4a7546c5c
commit 2420ee9b91
2 changed files with 2 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

31
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h
View File

@ -1,31 +0,0 @@
//== SMTContext.h -----------------------------------------------*- C++ -*--==//
//
// The LLVM Compiler Infrastructure
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
//
// This file defines a SMT generic Context API, which will be the base class
// for every SMT solver context specific class.
//
//===----------------------------------------------------------------------===//
#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONTEXT_H
#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONTEXT_H
namespace clang {
namespace ento {
/// Generic base class for SMT contexts
class SMTContext {
public:
SMTContext() = default;
virtual ~SMTContext() = default;
};
} // namespace ento
} // namespace clang
#endif

5
clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
View File

@ -11,7 +11,6 @@
#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h"
@ -53,11 +52,11 @@ void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
}
/// Wrapper for Z3 context
class Z3Context : public SMTContext {
class Z3Context {
public:
Z3_context Context;
Z3Context() : SMTContext() {
Z3Context() {
Context = Z3_mk_context_rc(Z3Config().Config);
// The error function is set here because the context is the first object
// created by the backend