Fix warnings and enable -Wnon-virtual-dtor warning (#2079)

This commit fixes warnings for an unused variable, comparison of two
different types and add virtual destructors to classes that were
previously missing them. It also enables the -Wnon-virtual-dtor warning
which warns about any class definition with virtual methods that does
not have a virtual destructor (except if the destructor is protected).
This flag is supported by both clang and GCC and not enabled by default.

diff --git a/configure.ac b/configure.ac
index 81e3f1fdc5684c8cfff64f81ca32d87f5a28a591..48ef9c7f8a4d72069722319ed79c9a29a591f3bf 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -988,6 +988,7 @@ CVC4_CXX_OPTION([-Wno-parentheses], [WNO_PARENTHESES])
 CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED])
 CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE])
 CVC4_CXX_OPTION([-Wsuggest-override], [W_SUGGEST_OVERRIDE])
+CVC4_CXX_OPTION([-Wnon-virtual-dtor], [W_NON_VIRTUAL_DTOR])
 CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING])
 AC_SUBST([WERROR])
 AC_SUBST([WNO_CONVERSION_NULL])
@@ -996,9 +997,11 @@ AC_SUBST([WNO_PARENTHESES])
 AC_SUBST([WNO_UNINITIALIZED])
 AC_SUBST([WNO_UNUSED_VARIABLE])
 AC_SUBST([W_SUGGEST_OVERRIDE])
+AC_SUBST([W_NON_VIRTUAL_DTOR])
 AC_SUBST([FNO_STRICT_ALIASING])
 
 CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }${W_SUGGEST_OVERRIDE}"
+CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }${W_NON_VIRTUAL_DTOR}"
 
 # On Mac, we have to fix the visibility of standard library symbols.
 # Otherwise, exported template instantiations---even though explicitly

diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index f0c1d548812bbc9d0e1d691081ee4d6991c43dc2..938e0f2a64536a8f025f322efe1c01b1f793f6da 100644 (file)
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -667,7 +667,7 @@ Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsign
   }
 
   if (signature.getNumChildren() == 0) {
-    Assert(signature.getKind() != kind::metakind::VARIABLE);
+    Assert(signature.getMetaKind() != kind::metakind::VARIABLE);
     seen[signature] = signature;
     return signature;
   }

diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp
index 00e527abad243a7a8ac87dd8e7d4d4427e363336..27f36cbf3824451a5ed7191cb9b0d66ee5447edb 100644 (file)
--- a/src/theory/quantifiers/dynamic_rewrite.cpp
+++ b/src/theory/quantifiers/dynamic_rewrite.cpp
@@ -24,8 +24,7 @@ namespace theory {
 namespace quantifiers {
 
 DynamicRewriter::DynamicRewriter(const std::string& name, QuantifiersEngine* qe)
-    : d_qe(qe),
-      d_equalityEngine(qe->getUserContext(), "DynamicRewriter::" + name, true),
+    : d_equalityEngine(qe->getUserContext(), "DynamicRewriter::" + name, true),
       d_rewrites(qe->getUserContext())
 {
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);

diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h
index 56f59147072085d1f28b43c06c2db66689a92cb7..9d80ebe5769ef115a9df93090b4d6e0ab39f5de8 100644 (file)
--- a/src/theory/quantifiers/dynamic_rewrite.h
+++ b/src/theory/quantifiers/dynamic_rewrite.h
@@ -65,8 +65,6 @@ class DynamicRewriter
   bool areEqual(Node a, Node b);
 
  private:
-  /** pointer to the quantifiers engine */
-  QuantifiersEngine* d_qe;
   /** index over argument types to function skolems
    *
    * The purpose of this trie is to associate a class of interpreted operator

diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index 856219b7364aa24c0d508d957db6552a329a6e91..6330bbd30d323042bcbd94d6cd18ab25551a679f 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -42,7 +42,7 @@ class Cegis : public SygusModule
 {
  public:
   Cegis(QuantifiersEngine* qe, CegConjecture* p);
-  ~Cegis() {}
+  ~Cegis() override {}
   /** initialize */
   virtual bool initialize(Node n,
                           const std::vector<Node>& candidates,

diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index ec338a8b2bbe29c5c88c161882b0490b1e6cde89..c0f860975d58564255af874e0546f4e96061406a 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -200,7 +200,7 @@ class CegisUnif : public Cegis
 {
  public:
   CegisUnif(QuantifiersEngine* qe, CegConjecture* p);
-  ~CegisUnif();
+  ~CegisUnif() override;
   /** Retrieves enumerators for constructing solutions
    *
    * Non-unification candidates have themselves as enumerators, while for

diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index b01f8e1d051c41c6719e3c806e4c88f64e2ba267..fb2821e205d0f9680029cc95b374a2a3e1ce7f03 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -49,7 +49,7 @@ class SygusModule
 {
  public:
   SygusModule(QuantifiersEngine* qe, CegConjecture* p);
-  ~SygusModule() {}
+  virtual ~SygusModule() {}
   /** initialize
    *
    * n is the "base instantiation" of the deep-embedding version of the

diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h
index cbce5e70c4c3e4de84a75d7395167e85612144dc..db0ff4afb4c9ca577769ed98d9150229ecc7fd6b 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h
@@ -93,6 +93,8 @@ std::ostream& operator<<(std::ostream& os, StrategyType st);
 class UnifContext
 {
  public:
+  virtual ~UnifContext() {}
+
   /** Get the current role
    *
    * In a particular context when constructing solutions in synthesis by

diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index 5e0a24dd222a7d7f997753f023dbdf3251c9de0c..1b4d3aedd97a1070427464bfd1dce69580d14388 100644 (file)
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -278,6 +278,8 @@ class SygusSampler : public LazyTrieEvaluator
 class NotifyMatch
 {
  public:
+  virtual ~NotifyMatch() {}
+
   /**
    * A notification that s is equal to n * { vars -> subs }. This function
    * should return false if we do not wish to be notified of further matches.