From 7ff254480c38b721a506bb0c174bcd8cb34924ef Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 2 Sep 2021 12:04:11 -0700
Subject: [PATCH] EnvObj: Restrict access. (#7121)

This makes all members of EnvObj protected in order to prevent creating
EnvObj instances and call member functions. It further uses protected
inheritance (instead of public) for derived classes in order to disallow
`EnvObj* a = new DerivedObj();`.
---
 src/preprocessing/preprocessing_pass.h | 2 +-
 src/preprocessing/util/ite_utilities.h | 6 +++---
 src/smt/env_obj.h                      | 5 ++---
 3 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h
index e1c3a5100..cc438e5c6 100644
--- a/src/preprocessing/preprocessing_pass.h
+++ b/src/preprocessing/preprocessing_pass.h
@@ -49,7 +49,7 @@ class PreprocessingPassContext;
  */
 enum PreprocessingPassResult { CONFLICT, NO_CONFLICT };
 
-class PreprocessingPass : public EnvObj
+class PreprocessingPass : protected EnvObj
 {
  public:
   /* Preprocesses a list of assertions assertionsToPreprocess */
diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h
index 48408e46e..1d2aa7084 100644
--- a/src/preprocessing/util/ite_utilities.h
+++ b/src/preprocessing/util/ite_utilities.h
@@ -67,7 +67,7 @@ class ContainsTermITEVisitor
   NodeBoolMap d_cache;
 };
 
-class ITEUtilities : public EnvObj
+class ITEUtilities : protected EnvObj
 {
  public:
   ITEUtilities(Env& env);
@@ -164,7 +164,7 @@ class TermITEHeightCounter
  * A routine designed to undo the potentially large blow up
  * due to expansion caused by the ite simplifier.
  */
-class ITECompressor : public EnvObj
+class ITECompressor : protected EnvObj
 {
  public:
   ITECompressor(Env& env, ContainsTermITEVisitor* contains);
@@ -206,7 +206,7 @@ class ITECompressor : public EnvObj
   Statistics d_statistics;
 }; /* class ITECompressor */
 
-class ITESimplifier : public EnvObj
+class ITESimplifier : protected EnvObj
 {
  public:
   ITESimplifier(Env& env, ContainsTermITEVisitor* d_containsVisitor);
diff --git a/src/smt/env_obj.h b/src/smt/env_obj.h
index 69aab7647..bae05874b 100644
--- a/src/smt/env_obj.h
+++ b/src/smt/env_obj.h
@@ -31,12 +31,12 @@ class Options;
 
 class EnvObj
 {
- public:
+ protected:
   /** Constructor. */
   EnvObj(Env& env);
   EnvObj() = delete;
   /** Destructor.  */
-  ~EnvObj() {}
+  virtual ~EnvObj() {}
 
   /**
    * Rewrite a node.
@@ -44,7 +44,6 @@ class EnvObj
    */
   Node rewrite(TNode node);
 
- protected:
   /** The associated environment. */
   Env& d_env;
 };
-- 
2.30.2