Add missing overrides in unit tests (#2362)

diff --git a/test/unit/base/map_util_black.h b/test/unit/base/map_util_black.h
index 6d2d2bbc72f69c63f9a547c3e9f797f9b87c61d7..39567d6ac827f9b137c8e6e9a17e2184bfb86010 100644 (file)
--- a/test/unit/base/map_util_black.h
+++ b/test/unit/base/map_util_black.h
@@ -38,8 +38,8 @@ using std::string;
 class MapUtilBlack : public CxxTest::TestSuite
 {
  public:
-  void setUp() {}
-  void tearDown() {}
+  void setUp() override {}
+  void tearDown() override {}
 
   // Returns a map containing {"key"->"value", "other"->"entry"}.
   static const std::map<string, string>& DefaultMap()

diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h
index 7545fa808dd22f975885939ef397c894740275a6..8a31f70ca631c0976339262a09d6ba80e38b178a 100644 (file)
--- a/test/unit/context/cdlist_black.h
+++ b/test/unit/context/cdlist_black.h
@@ -40,9 +40,9 @@ class CDListBlack : public CxxTest::TestSuite {
   Context* d_context;
 
  public:
-  void setUp() { d_context = new Context(); }
+  void setUp() override { d_context = new Context(); }
 
-  void tearDown() { delete d_context; }
+  void tearDown() override { delete d_context; }
 
   // test at different sizes.  this triggers grow() behavior differently.
   // grow() was completely broken in revision 256

diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h
index 8cc1b73c2e2667c9adc105b73d80725308d7aad2..2d2b3f409d6306bd080957230cfb2a38da635865 100644 (file)
--- a/test/unit/context/cdmap_black.h
+++ b/test/unit/context/cdmap_black.h
@@ -31,14 +31,15 @@ class CDMapBlack : public CxxTest::TestSuite {
   Context* d_context;
 
  public:
-  void setUp() {
+  void setUp() override
+  {
     d_context = new Context;
     // Debug.on("context");
     // Debug.on("gc");
     // Debug.on("pushpop");
   }
 
-  void tearDown() { delete d_context; }
+  void tearDown() override { delete d_context; }
 
   // Returns the elements in a CDHashMap.
   static std::map<int, int> GetElements(const CDHashMap<int, int>& map) {

diff --git a/test/unit/context/cdmap_white.h b/test/unit/context/cdmap_white.h
index 232eb55a856b37984f3940a705f5de9be7e20fae..0f111cd6119db8f1a5288a86860dfeb911d5f078 100644 (file)
--- a/test/unit/context/cdmap_white.h
+++ b/test/unit/context/cdmap_white.h
@@ -27,17 +27,13 @@ class CDMapWhite : public CxxTest::TestSuite {
 
   Context* d_context;
 
-public:
+ public:
+  void setUp() override { d_context = new Context; }
 
-  void setUp() {
-    d_context = new Context;
-  }
-
-  void tearDown() {
-    delete d_context;
-  }
+  void tearDown() override { delete d_context; }
 
-  void testUnreachableSaveAndRestore() {
+  void testUnreachableSaveAndRestore()
+  {
     CDHashMap<int, int> map(d_context);
 
     TS_ASSERT_THROWS_NOTHING(map.makeCurrent());

diff --git a/test/unit/context/cdo_black.h b/test/unit/context/cdo_black.h
index f5666173d81b967ba55e61bcbfc5b396ec3e1a12..2838ae32201a8c2492e56b016fb27329b0559b59 100644 (file)
--- a/test/unit/context/cdo_black.h
+++ b/test/unit/context/cdo_black.h
@@ -33,17 +33,13 @@ private:
 
   Context* d_context;
 
-public:
+ public:
+  void setUp() override { d_context = new Context; }
 
-  void setUp() {
-    d_context = new Context;
-  }
-
-  void tearDown() {
-    delete d_context;
-  }
+  void tearDown() override { delete d_context; }
 
-  void testIntCDO() {
+  void testIntCDO()
+  {
     // Test that push/pop maintains the original value
     CDO<int> a1(d_context);
     a1 = 5;

diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h
index 63b60edc936f3c479d0dd31ba1efa2c53eb36f6a..b4be4197c8a91e6f57840f01beab18dddb5e489f 100644 (file)
--- a/test/unit/context/context_black.h
+++ b/test/unit/context/context_black.h
@@ -36,12 +36,10 @@ struct MyContextNotifyObj : public ContextNotifyObj {
     ContextNotifyObj(context, pre),
     nCalls(0) {
   }
-  
-  virtual ~MyContextNotifyObj() {}
 
-  void contextNotifyPop() {
-    ++nCalls;
-  }
+  ~MyContextNotifyObj() override {}
+
+  void contextNotifyPop() override { ++nCalls; }
 };
 
 class MyContextObj : public ContextObj {
@@ -75,18 +73,15 @@ public:
     nSaves(0) {
   }
 
-  virtual ~MyContextObj() {
-    destroy();
-  }
+  ~MyContextObj() override { destroy(); }
 
-  ContextObj* save(ContextMemoryManager* pcmm) {
+  ContextObj* save(ContextMemoryManager* pcmm) override
+  {
     ++nSaves;
     return new(pcmm) MyContextObj(*this);
   }
 
-  void restore(ContextObj* contextObj) {
-    nCalls = notify.nCalls;
-  }
+  void restore(ContextObj* contextObj) override { nCalls = notify.nCalls; }
 
   void makeCurrent() {
     ContextObj::makeCurrent();
@@ -99,17 +94,13 @@ private:
 
   Context* d_context;
 
-public:
+ public:
+  void setUp() override { d_context = new Context; }
 
-  void setUp() {
-    d_context = new Context;
-  }
-
-  void tearDown() {
-    delete d_context;
-  }
+  void tearDown() override { delete d_context; }
 
-  void testContextPushPop() {
+  void testContextPushPop()
+  {
     // Test what happens when the context is popped below 0
     // the interface doesn't declare any exceptions
     d_context->push();

diff --git a/test/unit/context/context_mm_black.h b/test/unit/context/context_mm_black.h
index ed64b5eac009e1c8bbd3e1f58e2d3cf69c00cf82..beace137ee5b7073b5435f3fa790a4c91169d6ab 100644 (file)
--- a/test/unit/context/context_mm_black.h
+++ b/test/unit/context/context_mm_black.h
@@ -33,13 +33,11 @@ private:
 
   ContextMemoryManager* d_cmm;
 
-public:
+ public:
+  void setUp() override { d_cmm = new ContextMemoryManager(); }
 
-  void setUp() {
-    d_cmm = new ContextMemoryManager();
-  }
-
-  void testPushPop() {
+  void testPushPop()
+  {
 #ifdef CVC4_DEBUG_CONTEXT_MEMORY_MANAGER
 #warning "Using the debug context memory manager, omitting unit tests"
 #else
@@ -96,7 +94,5 @@ public:
 #endif /* __CVC4__CONTEXT__CONTEXT_MM_H */
   }
 
-  void tearDown() {
-    delete d_cmm;
-  }
+  void tearDown() override { delete d_cmm; }
 };

diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h
index 64e6e184b145c748532739b907b5eb9f24a40a22..2c1ef8e71e60f89995a10f3e53851ecee8529f6e 100644 (file)
--- a/test/unit/context/context_white.h
+++ b/test/unit/context/context_white.h
@@ -29,18 +29,14 @@ private:
 
   Context* d_context;
 
-public:
+ public:
+  void setUp() override { d_context = new Context; }
 
-  void setUp() {
-    d_context = new Context;
-  }
-
-  void tearDown() {
-    delete d_context;
-  }
+  void tearDown() override { delete d_context; }
 
-  void testContextSimple() {
-    Scope *s = d_context->getTopScope();
+  void testContextSimple()
+  {
+    Scope* s = d_context->getTopScope();
 
     TS_ASSERT(s == d_context->getBottomScope());
     TS_ASSERT(d_context->getLevel() == 0);

diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index afc99ef322a2f57d6c1c9147a737da7bf357f8ab..58defe07dfd4f5a7d8a5ff094afdda02a0420530 100644 (file)
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -42,16 +42,17 @@ private:
   SmtEngine* d_smtEngine;
   SmtScope* d_scope;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_exprManager = new ExprManager();
     d_nodeManager = NodeManager::fromExprManager(d_exprManager);
     d_smtEngine = new SmtEngine(d_exprManager);
     d_scope = new SmtScope(d_smtEngine);
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_scope;
     delete d_smtEngine;
     delete d_exprManager;

diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index a169855e2c1a63634290b8e4f5719f3bb1af0ca8..847cbf9296e51730a684b50e0c4d186ed816da1d 100644 (file)
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -61,9 +61,9 @@ class AttributeWhite : public CxxTest::TestSuite {
   TypeNode* d_booleanType;
   SmtEngine* d_smtEngine;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
     d_smtEngine = new SmtEngine(d_em);
@@ -71,7 +71,8 @@ public:
     d_booleanType = new TypeNode(d_nm->booleanType());
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_booleanType;
     delete d_scope;
     delete d_smtEngine;

diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h
index a131aa140e8fe5188bb6bfee6783316f9671eac7..9c604aa52f8b9ad50634238e00d1758020d95e18 100644 (file)
--- a/test/unit/expr/expr_manager_public.h
+++ b/test/unit/expr/expr_manager_public.h
@@ -61,19 +61,19 @@ private:
     return vars;
   }
 
+ public:
+  void setUp() override { d_exprManager = new ExprManager; }
 
-public:
-  void setUp() {
-    d_exprManager = new ExprManager;
-  }
-
-
-  void tearDown() {
-    try {
+  void tearDown() override
+  {
+    try
+    {
       delete d_exprManager;
-    } catch(Exception e) {
+    }
+    catch (Exception e)
+    {
       cerr << "Exception during tearDown():" << endl << e;
-      throw ;
+      throw;
     }
   }
 

diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index 4354c5b6ae1cee69f1c254b6a902211f98d8ff98..d8774db820fed3c44a284480924d5e40634f64c1 100644 (file)
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -50,12 +50,12 @@ private:
   Expr* r1;
   Expr* r2;
 
-public:
-
-  void setUp() {
-    try {
-
-      char *argv[2];
+ public:
+  void setUp() override
+  {
+    try
+    {
+      char* argv[2];
       argv[0] = strdup("");
       argv[1] = strdup("--output-language=ast");
       Options::parseOptions(&opts, 2, argv);
@@ -64,12 +64,13 @@ public:
 
       d_em = new ExprManager(opts);
 
-      a_bool = new Expr(d_em->mkVar("a",d_em->booleanType()));
+      a_bool = new Expr(d_em->mkVar("a", d_em->booleanType()));
       b_bool = new Expr(d_em->mkVar("b", d_em->booleanType()));
       c_bool_and = new Expr(d_em->mkExpr(AND, *a_bool, *b_bool));
       and_op = new Expr(d_em->mkConst(AND));
       plus_op = new Expr(d_em->mkConst(PLUS));
-      fun_type = new Type(d_em->mkFunctionType(d_em->booleanType(), d_em->booleanType()));
+      fun_type = new Type(
+          d_em->mkFunctionType(d_em->booleanType(), d_em->booleanType()));
       fun_op = new Expr(d_em->mkVar("f", *fun_type));
       d_apply_fun_bool = new Expr(d_em->mkExpr(APPLY_UF, *fun_op, *a_bool));
       null = new Expr();
@@ -78,13 +79,16 @@ public:
       i2 = new Expr(d_em->mkConst(Rational(23)));
       r1 = new Expr(d_em->mkConst(Rational(1, 5)));
       r2 = new Expr(d_em->mkConst(Rational("0")));
-    } catch(Exception e) {
+    }
+    catch (Exception e)
+    {
       cerr << "Exception during setUp():" << endl << e;
       throw;
     }
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     try {
       delete r2;
       delete r1;

diff --git a/test/unit/expr/kind_black.h b/test/unit/expr/kind_black.h
index 5ac503b0e3f04e070a8871aa64ab6b58ed989e36..900f5dac694b9b1268601f48b603211d844263e3 100644 (file)
--- a/test/unit/expr/kind_black.h
+++ b/test/unit/expr/kind_black.h
@@ -34,13 +34,15 @@ class KindBlack : public CxxTest::TestSuite {
   //easier to define in setup
   int beyond;
   Kind unknown;
-public:
-  void setUp() {
+
+ public:
+  void setUp() override
+  {
     undefined = UNDEFINED_KIND;
     null = NULL_EXPR;
     last = LAST_KIND;
-    beyond = ((int) LAST_KIND) + 1;
-    unknown = (Kind) beyond;
+    beyond = ((int)LAST_KIND) + 1;
+    unknown = (Kind)beyond;
   }
 
   

diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index fb468c896afcc56b09930e2daa9d1084d96cbde3..461d59498b28d1c5b3f671d60fb7db8c3c8a6564 100644 (file)
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -56,7 +56,8 @@ class NodeBlack : public CxxTest::TestSuite {
   TypeNode* d_realType;
 
  public:
-  void setUp() {
+  void setUp() override
+  {
     char* argv[2];
     argv[0] = strdup("");
     argv[1] = strdup("--output-language=ast");
@@ -70,7 +71,8 @@ class NodeBlack : public CxxTest::TestSuite {
     d_realType = new TypeNode(d_nodeManager->realType());
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_realType;
     delete d_booleanType;
     delete d_scope;

diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index b8e9d92f6ff2a5efb750ef2d180df5f6bca08bd8..f4fbbb5d9c0756c7d49660c329d072ff5c31e9f9 100644 (file)
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -40,9 +40,9 @@ private:
   TypeNode* d_integerType;
   TypeNode* d_realType;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_nm = new NodeManager(NULL);
     d_scope = new NodeManagerScope(d_nm);
 
@@ -52,7 +52,8 @@ public:
     d_realType = new TypeNode(d_nm->realType());
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_integerType;
     delete d_booleanType;
     delete d_realType;

diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index 68c94c176022ff60c263fbe39940e3f00164c617..5da55916b387842da08c83c661c84238d3f02757 100644 (file)
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -34,14 +34,15 @@ class NodeManagerBlack : public CxxTest::TestSuite {
   NodeManager* d_nodeManager;
   NodeManagerScope* d_scope;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_nodeManager = new NodeManager(NULL);
     d_scope = new NodeManagerScope(d_nodeManager);
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_scope;
     delete d_nodeManager;
   }

diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h
index e2b8cbf1cf22f10dc22de67c2c37171ce3bc2685..016ea7793f6c8cce6f88f46df285cb75f5cbe67f 100644 (file)
--- a/test/unit/expr/node_manager_white.h
+++ b/test/unit/expr/node_manager_white.h
@@ -30,14 +30,15 @@ class NodeManagerWhite : public CxxTest::TestSuite {
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_nm = new NodeManager(NULL);
     d_scope = new NodeManagerScope(d_nm);
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_scope;
     delete d_nm;
   }

diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h
index bab7e2b0c4125a79640d485826c75aeef9b4c108..cfc4a6b7a2df465389eca9fa5b93741db41cd9e3 100644 (file)
--- a/test/unit/expr/node_self_iterator_black.h
+++ b/test/unit/expr/node_self_iterator_black.h
@@ -33,16 +33,17 @@ private:
   TypeNode* d_booleanType;
   TypeNode* d_realType;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_nodeManager = new NodeManager(NULL);
     d_scope = new NodeManagerScope(d_nodeManager);
     d_booleanType = new TypeNode(d_nodeManager->booleanType());
     d_realType = new TypeNode(d_nodeManager->realType());
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_booleanType;
     delete d_scope;
     delete d_nodeManager;

diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index d2d6a265d42af8628a254c898518d9d000321b3f..09d015e42b7b96fe55e1294a122821dbca2b2b1e 100644 (file)
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -34,14 +34,15 @@ class NodeWhite : public CxxTest::TestSuite {
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_nm = new NodeManager(NULL);
     d_scope = new NodeManagerScope(d_nm);
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_scope;
     delete d_nm;
   }

diff --git a/test/unit/expr/symbol_table_black.h b/test/unit/expr/symbol_table_black.h
index 33b5d73c9e005ff69dfa85efa3d9f831e742543e..2f6f88c27080c7940a247412538ff888c925cdb8 100644 (file)
--- a/test/unit/expr/symbol_table_black.h
+++ b/test/unit/expr/symbol_table_black.h
@@ -37,18 +37,22 @@ private:
 
   ExprManager* d_exprManager;
 
-public:
-
-  void setUp() {
-    try {
+ public:
+  void setUp() override
+  {
+    try
+    {
       d_exprManager = new ExprManager;
-    } catch(Exception e) {
+    }
+    catch (Exception e)
+    {
       cerr << "Exception during setUp():" << endl << e;
       throw;
     }
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     try {
       delete d_exprManager;
     } catch(Exception e) {

diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h
index ff05df5da939437735fefc87e927ee9477e1d54e..51cb6a8819a6e8ea3943f6912a68b8ad0d50ad0c 100644 (file)
--- a/test/unit/expr/type_cardinality_public.h
+++ b/test/unit/expr/type_cardinality_public.h
@@ -32,20 +32,20 @@ using namespace std;
 class TypeCardinalityPublic : public CxxTest::TestSuite {
   ExprManager* d_em;
 
-public:
-
-  void setUp() {
-    d_em = new ExprManager();
-  }
-
-  void tearDown() {
-    delete d_em;
-  }
-
-  void testTheBasics() {
-    TS_ASSERT( d_em->booleanType().getCardinality().compare(2) == Cardinality::EQUAL );
-    TS_ASSERT( d_em->integerType().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL );
-    TS_ASSERT( d_em->realType().getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL );
+ public:
+  void setUp() override { d_em = new ExprManager(); }
+
+  void tearDown() override { delete d_em; }
+
+  void testTheBasics()
+  {
+    TS_ASSERT(d_em->booleanType().getCardinality().compare(2)
+              == Cardinality::EQUAL);
+    TS_ASSERT(
+        d_em->integerType().getCardinality().compare(Cardinality::INTEGERS)
+        == Cardinality::EQUAL);
+    TS_ASSERT(d_em->realType().getCardinality().compare(Cardinality::REALS)
+              == Cardinality::EQUAL);
   }
 
   void testArrays() {

diff --git a/test/unit/expr/type_node_white.h b/test/unit/expr/type_node_white.h
index 45a48ea99930359bb563410b86d1e21144fbe493..32b5ca7cb0c5447eeb7716b1bff29745ba8413a9 100644 (file)
--- a/test/unit/expr/type_node_white.h
+++ b/test/unit/expr/type_node_white.h
@@ -37,16 +37,17 @@ class TypeNodeWhite : public CxxTest::TestSuite {
   NodeManagerScope* d_scope;
   SmtEngine* d_smt;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_em = new ExprManager();
     d_nm = d_em->getNodeManager();
     d_smt = new SmtEngine(d_em);
     d_scope = new NodeManagerScope(d_nm);
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_scope;
     delete d_smt;
     delete d_em;

diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h
index 44b3660c9b11b71a7d43446d3e60b7501da38779..cf76bb05a525b9484ca6d9a0d8929f097a211c5c 100644 (file)
--- a/test/unit/main/interactive_shell_black.h
+++ b/test/unit/main/interactive_shell_black.h
@@ -35,7 +35,7 @@ using namespace std;
 class InteractiveShellBlack : public CxxTest::TestSuite
 {
  public:
-  void setUp()
+  void setUp() override
   {
     d_sin = new stringstream;
     d_sout = new stringstream;
@@ -45,7 +45,8 @@ class InteractiveShellBlack : public CxxTest::TestSuite
     d_solver.reset(new api::Solver(&d_options));
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_sin;
     delete d_sout;
   }

diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index e7548708e9a035bf03529e955d28215d41ca9a22..58ed12a60b1a77ca4c7885fb9d54d139b0a2fa96 100644 (file)
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -217,13 +217,9 @@ class Cvc4ParserTest : public CxxTest::TestSuite, public ParserBlack {
 public:
   Cvc4ParserTest() : ParserBlack(LANG_CVC4) { }
 
-  void setUp() {
-    super::setUp();
-  }
+  void setUp() override { super::setUp(); }
 
-  void tearDown() {
-    super::tearDown();
-  }
+  void tearDown() override { super::tearDown(); }
 
   void testGoodCvc4Inputs() {
     tryGoodInput(""); // empty string is OK
@@ -307,13 +303,9 @@ class Smt1ParserTest : public CxxTest::TestSuite, public ParserBlack {
 public:
   Smt1ParserTest() : ParserBlack(LANG_SMTLIB_V1) { }
 
-  void setUp() {
-    super::setUp();
-  }
+  void setUp() override { super::setUp(); }
 
-  void tearDown() {
-    super::tearDown();
-  }
+  void tearDown() override { super::tearDown(); }
 
   void testGoodSmt1Inputs() {
     tryGoodInput(""); // empty string is OK
@@ -376,15 +368,12 @@ class Smt2ParserTest : public CxxTest::TestSuite, public ParserBlack {
 public:
   Smt2ParserTest() : ParserBlack(LANG_SMTLIB_V2) { }
 
-  void setUp() {
-    super::setUp();
-  }
+  void setUp() override { super::setUp(); }
 
-  void tearDown() {
-    super::tearDown();
-  }
+  void tearDown() override { super::tearDown(); }
 
-  virtual void setupContext(Parser& parser) {
+  void setupContext(Parser& parser) override
+  {
     if(dynamic_cast<Smt2*>(&parser) != NULL){
       dynamic_cast<Smt2*>(&parser)->addTheory(Smt2::THEORY_CORE);
     }

diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h
index 45baf177f8aebde893450157646c76f555a8e387..d83d2681b261b54025d88e983f80b94769545410 100644 (file)
--- a/test/unit/parser/parser_builder_black.h
+++ b/test/unit/parser/parser_builder_black.h
@@ -38,9 +38,9 @@ using namespace std;
 class ParserBuilderBlack : public CxxTest::TestSuite
 {
  public:
-  void setUp() { d_solver.reset(new api::Solver()); }
+  void setUp() override { d_solver.reset(new api::Solver()); }
 
-  void tearDown() {}
+  void tearDown() override {}
 
   void testEmptyFileInput()
   {

diff --git a/test/unit/preprocessing/pass_bv_gauss_white.h b/test/unit/preprocessing/pass_bv_gauss_white.h
index 7d7ee1a3a024edf515723700b616eb9884bfbd79..f238ba8be71ad4fafaeaa8136817f7d2a706cc5a 100644 (file)
--- a/test/unit/preprocessing/pass_bv_gauss_white.h
+++ b/test/unit/preprocessing/pass_bv_gauss_white.h
@@ -177,7 +177,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
  public:
   TheoryBVGaussWhite() {}
 
-  void setUp()
+  void setUp() override
   {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
@@ -251,7 +251,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     d_z_mul_nine = d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_nine);
   }
 
-  void tearDown()
+  void tearDown() override
   {
     (void)d_scope;
     d_p = Node::null();

diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index be69a7a1d8cabc82255581d4c0f0b27c8bee7129..7e04bb7c5e735cf6bb5881da5a8ecc80f2c55dab 100644 (file)
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -49,31 +49,34 @@ class FakeSatSolver : public SatSolver {
  public:
   FakeSatSolver() : d_nextVar(0), d_addClauseCalled(false) {}
 
-  SatVariable newVar(bool theoryAtom, bool preRegister, bool canErase) {
+  SatVariable newVar(bool theoryAtom, bool preRegister, bool canErase) override
+  {
     return d_nextVar++;
   }
 
-  SatVariable trueVar() { return d_nextVar++; }
+  SatVariable trueVar() override { return d_nextVar++; }
 
-  SatVariable falseVar() { return d_nextVar++; }
+  SatVariable falseVar() override { return d_nextVar++; }
 
-  ClauseId addClause(SatClause& c, bool lemma) {
+  ClauseId addClause(SatClause& c, bool lemma) override
+  {
     d_addClauseCalled = true;
     return ClauseIdUndef;
   }
 
-  ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) {
+  ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override
+  {
     d_addClauseCalled = true;
     return ClauseIdUndef;
   }
 
-  bool nativeXor() { return false; }
+  bool nativeXor() override { return false; }
 
   void reset() { d_addClauseCalled = false; }
 
   unsigned int addClauseCalled() { return d_addClauseCalled; }
 
-  unsigned getAssertionLevel() const { return 0; }
+  unsigned getAssertionLevel() const override { return 0; }
 
   bool isDecision(Node) const { return false; }
 
@@ -83,19 +86,22 @@ class FakeSatSolver : public SatSolver {
 
   bool spendResource() { return false; }
 
-  void interrupt() {}
+  void interrupt() override {}
 
-  SatValue solve() { return SAT_VALUE_UNKNOWN; }
+  SatValue solve() override { return SAT_VALUE_UNKNOWN; }
 
-  SatValue solve(long unsigned int& resource) { return SAT_VALUE_UNKNOWN; }
+  SatValue solve(long unsigned int& resource) override
+  {
+    return SAT_VALUE_UNKNOWN;
+  }
 
-  SatValue value(SatLiteral l) { return SAT_VALUE_UNKNOWN; }
+  SatValue value(SatLiteral l) override { return SAT_VALUE_UNKNOWN; }
 
-  SatValue modelValue(SatLiteral l) { return SAT_VALUE_UNKNOWN; }
+  SatValue modelValue(SatLiteral l) override { return SAT_VALUE_UNKNOWN; }
 
   bool properExplanation(SatLiteral lit, SatLiteral expl) const { return true; }
 
-  bool ok() const { return true; }
+  bool ok() const override { return true; }
 
 }; /* class FakeSatSolver */
 
@@ -122,7 +128,8 @@ class CnfStreamWhite : public CxxTest::TestSuite {
   SmtScope* d_scope;
   SmtEngine* d_smt;
 
-  void setUp() {
+  void setUp() override
+  {
     d_exprManager = new ExprManager();
     d_smt = new SmtEngine(d_exprManager);
     d_smt->d_logic.lock();
@@ -138,7 +145,8 @@ class CnfStreamWhite : public CxxTest::TestSuite {
         d_satSolver, d_cnfRegistrar, d_cnfContext, d_smt->channels());
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_cnfStream;
     delete d_cnfContext;
     delete d_cnfRegistrar;

diff --git a/test/unit/theory/evaluator_white.h b/test/unit/theory/evaluator_white.h
index 4416ee00a8a6cf46388a0dfc8fb4032013b19b3b..10cb15f6fc53e95442a42b5e3d655719cb9a8e1c 100644 (file)
--- a/test/unit/theory/evaluator_white.h
+++ b/test/unit/theory/evaluator_white.h
@@ -43,7 +43,7 @@ class TheoryEvaluatorWhite : public CxxTest::TestSuite
  public:
   TheoryEvaluatorWhite() {}
 
-  void setUp()
+  void setUp() override
   {
     Options opts;
     opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
@@ -53,7 +53,7 @@ class TheoryEvaluatorWhite : public CxxTest::TestSuite
     d_scope = new SmtScope(d_smt);
   }
 
-  void tearDown()
+  void tearDown() override
   {
     delete d_scope;
     delete d_smt;

diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index 2cb1243d58788102d3add88b311277a08782718b..7661c08b567c031e50d16e0b8e8a80db46682091 100644 (file)
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -97,7 +97,8 @@ public:
     }
   }
 
-  void setUp() {
+  void setUp() override
+  {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
     d_smt = new SmtEngine(d_em);
@@ -125,7 +126,8 @@ public:
 
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_intType;
     delete d_realType;
     delete d_booleanType;

diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 487c6a434e76411c749620005f5ac502a597efd2..569d7e30b7c08ee292a95ca33ac47d2b0cd38e63 100644 (file)
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -44,9 +44,9 @@ private:
   NodeManager* d_nm;
   SmtScope* d_scope;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_em = new ExprManager();
     d_smt = new SmtEngine(d_em);
     d_scope = new SmtScope(d_smt);
@@ -54,7 +54,8 @@ public:
     d_nm = NodeManager::fromExprManager(d_em);
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_scope;
     delete d_smt;
     delete d_em;

diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h
index c830e7813526c2193d998333b1c5003f96162695..bc5b36a0b01d7a4bbe47a7c84f8aa5a6dda984e0 100644 (file)
--- a/test/unit/theory/theory_bv_white.h
+++ b/test/unit/theory/theory_bv_white.h
@@ -52,14 +52,16 @@ public:
 
   TheoryBVWhite() {}
 
-  void setUp() {
+  void setUp() override
+  {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
     d_smt = new SmtEngine(d_em);
     d_scope = new SmtScope(d_smt);
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_scope;
     delete d_smt;
     delete d_em;

diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h
index 4c96f6cb92e007c890e20dcc7ecdac7a69011793..018744bd1661fe734a5f18270beb163c3554a81b 100644 (file)
--- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h
+++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h
@@ -38,8 +38,8 @@ using namespace CVC4::smt;
 class BvInstantiatorWhite : public CxxTest::TestSuite
 {
  public:
-  void setUp();
-  void tearDown();
+  void setUp() override;
+  void tearDown() override;
 
   void testGetPvCoeff();
   void testNormalizePvMult();

diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index fc073b5a40c54dc4d71f0edc4c91aafeef1d4d4e..67dc205419a8ad974399d37a21af4903a52fe545 100644 (file)
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -39,7 +39,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
  public:
   TheoryStringsRewriterWhite() {}
 
-  void setUp()
+  void setUp() override
   {
     Options opts;
     opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
@@ -49,7 +49,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     d_scope = new SmtScope(d_smt);
   }
 
-  void tearDown()
+  void tearDown() override
   {
     delete d_scope;
     delete d_smt;

diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index 0fbf9c1d6900e4122699f14eca2222424be6014e..c8265a755aa1afd3a034b636c06957db2ebd6066 100644 (file)
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -122,20 +122,19 @@ public:
     return done();
   }
 
-  void check(Effort e) {
+  void check(Effort e) override
+  {
     while(!done()) {
       getWrapper();
     }
   }
 
-  void presolve() {
-    Unimplemented();
-  }
-  void preRegisterTerm(TNode n) {}
-  void propagate(Effort level) {}
-  Node explain(TNode n) { return Node::null(); }
+  void presolve() override { Unimplemented(); }
+  void preRegisterTerm(TNode n) override {}
+  void propagate(Effort level) override {}
+  Node explain(TNode n) override { return Node::null(); }
   Node getValue(TNode n) { return Node::null(); }
-  string identify() const { return "DummyTheory"; }
+  string identify() const override { return "DummyTheory"; }
 };/* class DummyTheory */
 
 class TheoryBlack : public CxxTest::TestSuite {
@@ -155,9 +154,9 @@ class TheoryBlack : public CxxTest::TestSuite {
   Node atom0;
   Node atom1;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
     d_smt = new SmtEngine(d_em);
@@ -173,14 +172,15 @@ public:
     d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN] = NULL;
     d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN] = NULL;
 
-    d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL),
-                              *d_logicInfo);
+    d_dummy = new DummyTheory(
+        d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo);
     d_outputChannel.clear();
     atom0 = d_nm->mkConst(true);
     atom1 = d_nm->mkConst(false);
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     atom1 = Node::null();
     atom0 = Node::null();
     delete d_dummy;

diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h
index 03b1a2a95069080886ec93eb0597d253639d0ab2..b68941843ac566e07557458a289360d8698ed969 100644 (file)
--- a/test/unit/theory/type_enumerator_white.h
+++ b/test/unit/theory/type_enumerator_white.h
@@ -38,15 +38,16 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite {
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
     d_scope = new NodeManagerScope(d_nm);
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_scope;
     delete d_em;
   }

diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h
index 49a0b995ac7b6bbd7852806cc60a385277142671..c668e8c8fd015e33440c2dec78d69135a247032c 100644 (file)
--- a/test/unit/util/array_store_all_black.h
+++ b/test/unit/util/array_store_all_black.h
@@ -30,12 +30,14 @@ class ArrayStoreAllBlack : public CxxTest::TestSuite {
   ExprManagerScope* d_scope;
 
  public:
-  void setUp() {
+  void setUp() override
+  {
     d_em = new ExprManager();
     d_scope = new ExprManagerScope(*d_em);
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_scope;
     delete d_em;
   }

diff --git a/test/unit/util/binary_heap_black.h b/test/unit/util/binary_heap_black.h
index 904b78b4b1e4b7fd79471d7f9648c395864debea..ce7e854d8dc59eb06dc1c7497f9ee3a00622cfaa 100644 (file)
--- a/test/unit/util/binary_heap_black.h
+++ b/test/unit/util/binary_heap_black.h
@@ -25,20 +25,18 @@ using namespace CVC4;
 using namespace std;
 
 class BinaryHeapBlack : public CxxTest::TestSuite {
-public:
+ public:
+  void setUp() override {}
 
-  void setUp() {
-  }
-
-  void tearDown() {
-  }
+  void tearDown() override {}
 
   /**
    * Test a a series of simple heaps (push a few then pop all then do others).
    * Done as a series to test if the heap structure falls into a bad state
    * after prolonged use.
    */
-  void testHeapSeries() {
+  void testHeapSeries()
+  {
     BinaryHeap<int> heap;
 
     // First test a heap of 1 element

diff --git a/test/unit/util/bitvector_black.h b/test/unit/util/bitvector_black.h
index 04fdc4044d9c7bff2dcdbc5599c36c8bf637a325..c75368196da7e0f40ff209374bab96fee8d89c31 100644 (file)
--- a/test/unit/util/bitvector_black.h
+++ b/test/unit/util/bitvector_black.h
@@ -26,7 +26,7 @@ class BitVectorBlack : public CxxTest::TestSuite {
 
 
 public:
- void setUp()
+ void setUp() override
  {
    zero = BitVector(4);
    one = zero.setBit(0);

diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h
index 7e69e4efeb51e3fbb12ff669c7669466ef71434e..c2086c415f7671c074b8a1c1ee5767c468b8a9d9 100644 (file)
--- a/test/unit/util/datatype_black.h
+++ b/test/unit/util/datatype_black.h
@@ -31,16 +31,17 @@ class DatatypeBlack : public CxxTest::TestSuite {
   ExprManager* d_em;
   ExprManagerScope* d_scope;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_em = new ExprManager();
     d_scope = new ExprManagerScope(*d_em);
     Debug.on("datatypes");
     Debug.on("groundterms");
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_scope;
     delete d_em;
   }

diff --git a/test/unit/util/exception_black.h b/test/unit/util/exception_black.h
index 0eb4b004012818faebf0a14df24b2083bead0fe0..ba17d28da2df93aeb66ec131f6e5a47c61195608 100644 (file)
--- a/test/unit/util/exception_black.h
+++ b/test/unit/util/exception_black.h
@@ -25,16 +25,14 @@ using namespace CVC4;
 using namespace std;
 
 class ExceptionBlack : public CxxTest::TestSuite {
-public:
+ public:
+  void setUp() override {}
 
-  void setUp() {
-  }
-
-  void tearDown() {
-  }
+  void tearDown() override {}
 
   // CVC4::Exception is a simple class, just test it all at once.
-  void testExceptions() {
+  void testExceptions()
+  {
     Exception e1;
     Exception e2(string("foo!"));
     Exception e3("bar!");

diff --git a/test/unit/util/listener_black.h b/test/unit/util/listener_black.h
index 014970b77498ec1424584f1d6c2250a87a3220bc..7296de060a231d0c2dd9ef2168037288dffa78e3 100644 (file)
--- a/test/unit/util/listener_black.h
+++ b/test/unit/util/listener_black.h
@@ -30,9 +30,9 @@ class ListenerBlack : public CxxTest::TestSuite {
    public:
     EventListener(std::multiset<std::string>& events, std::string name)
         : d_events(events), d_name(name) {}
-    ~EventListener(){}
+    ~EventListener() override {}
 
-    virtual void notify() { d_events.insert(d_name); }
+    void notify() override { d_events.insert(d_name); }
 
    private:
     std::multiset<std::string>& d_events;
@@ -45,13 +45,9 @@ public:
     return std::multiset<std::string>(arr, arr + len);
   }
 
-  void setUp() {
-    d_events.clear();
-  }
+  void setUp() override { d_events.clear(); }
 
-  void tearDown() {
-    d_events.clear();
-  }
+  void tearDown() override { d_events.clear(); }
 
   void testEmptyCollection() {
     // Makes an new collection and tests that it is empty.

diff --git a/test/unit/util/output_black.h b/test/unit/util/output_black.h
index c8833ced588b0d957785003e3071a07cf0fcbfdb..cea30f360bf10175a0d2cf96d89f097eebf67b2c 100644 (file)
--- a/test/unit/util/output_black.h
+++ b/test/unit/util/output_black.h
@@ -33,9 +33,9 @@ class OutputBlack : public CxxTest::TestSuite {
   stringstream d_messageStream;
   stringstream d_warningStream;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     DebugChannel.setStream(&d_debugStream);
     TraceChannel.setStream(&d_traceStream);
     NoticeChannel.setStream(&d_noticeStream);
@@ -51,8 +51,7 @@ public:
     d_warningStream.str("");
   }
 
-  void tearDown() {
-  }
+  void tearDown() override {}
 
   void testOutput() {
     Debug.on("foo");