summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2014-05-15 23:33:55 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2014-05-20 16:14:08 -0400
commita0960d8b5bc0897191444b7bcffece8136630917 (patch)
tree78b11cc03ad75869f78ed70287f6bf707e0ccc45
parent76f8e7c5d64d142110b6ed1ecab1d5d345af77c3 (diff)
Fix compiler warning (missing virtual dtor)
-rw-r--r--src/prop/registrar.h1
-rw-r--r--src/theory/theory_registrar.h2
-rw-r--r--src/util/regexp.cpp2
3 files changed, 3 insertions, 2 deletions
diff --git a/src/prop/registrar.h b/src/prop/registrar.h
index 4fe04f062..b6dd021ab 100644
--- a/src/prop/registrar.h
+++ b/src/prop/registrar.h
@@ -28,6 +28,7 @@ namespace prop {
class Registrar {
public:
+ virtual ~Registrar() {}
virtual void preRegister(Node n) = 0;
};/* class Registrar */
diff --git a/src/theory/theory_registrar.h b/src/theory/theory_registrar.h
index 691c1147b..d8389bece 100644
--- a/src/theory/theory_registrar.h
+++ b/src/theory/theory_registrar.h
@@ -29,7 +29,7 @@
namespace CVC4 {
namespace theory {
-class TheoryRegistrar: public prop::Registrar {
+class TheoryRegistrar : public prop::Registrar {
private:
TheoryEngine* d_theoryEngine;
diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index 3f0bc46fd..cbc0b843b 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -156,4 +156,4 @@ std::ostream& operator<<(std::ostream& out, const RegExp& s) {
return out << "regexp(" << s.getType() << ')';
}
-}/* CVC4 namespace */ \ No newline at end of file
+}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback