Fixes related to destructing null (#3231)

diff --git a/src/base/exception.cpp b/src/base/exception.cpp
index c1c174d1dbbad0b2698ff078ff0ab56cf30a602d..44d9b10bc4ae1aefa51a27b234393f221b1e3376 100644 (file)
--- a/src/base/exception.cpp
+++ b/src/base/exception.cpp
@@ -65,9 +65,7 @@ std::string IllegalArgumentException::formatVariadic(const char* format, ...) {
 
   for (int i = 0; i < 2; ++i){
     Assert(n > 0);
-    if(buf != NULL){
-      delete [] buf;
-    }
+    delete[] buf;
     buf = new char[n];
 
     va_list args_copy;

diff --git a/src/theory/arith/cut_log.cpp b/src/theory/arith/cut_log.cpp
index e9df7559daad21bf31a6f5ba39f478ef6793e0ab..43ef971236b03a2108f55095426f36e0208944bc 100644 (file)
--- a/src/theory/arith/cut_log.cpp
+++ b/src/theory/arith/cut_log.cpp
@@ -98,21 +98,19 @@ std::ostream& operator<<(std::ostream& os, const PrimitiveVec& pv){
 }
 
 CutInfo::CutInfo(CutInfoKlass kl, int eid, int o)
-  : d_klass(kl)
-  , d_execOrd(eid)
-  , d_poolOrd(o)
-  , d_cutType(kind::UNDEFINED_KIND)
-  , d_cutRhs()
-  , d_cutVec()
-  , d_mAtCreation(-1)
-  , d_rowId(-1)
-  , d_exactPrecision(NULL)
-  , d_explanation(NULL)
+    : d_klass(kl),
+      d_execOrd(eid),
+      d_poolOrd(o),
+      d_cutType(kind::UNDEFINED_KIND),
+      d_cutRhs(),
+      d_cutVec(),
+      d_mAtCreation(-1),
+      d_rowId(-1),
+      d_exactPrecision(nullptr),
+      d_explanation(nullptr)
 {}
 
 CutInfo::~CutInfo(){
-  if(d_exactPrecision == NULL){ delete d_exactPrecision; }
-  if(d_explanation == NULL){ delete d_explanation; }
 }
 
 int CutInfo::getId() const {
@@ -164,9 +162,7 @@ void CutInfo::setRhs(double r){
   d_cutRhs = r;
 }
 
-bool CutInfo::reconstructed() const{
-  return d_exactPrecision != NULL;
-}
+bool CutInfo::reconstructed() const { return d_exactPrecision != nullptr; }
 
 CutInfoKlass CutInfo::getKlass() const{
   return d_klass;
@@ -190,9 +186,7 @@ int CutInfo::getMAtCreation() const{
 }
 
 /* Returns true if the cut has an explanation. */
-bool CutInfo::proven() const{
-  return d_explanation != NULL;
-}
+bool CutInfo::proven() const { return d_explanation != nullptr; }
 
 bool CutInfo::operator<(const CutInfo& o) const{
   return d_execOrd < o.d_execOrd;
@@ -201,14 +195,17 @@ bool CutInfo::operator<(const CutInfo& o) const{
 
 void CutInfo::setReconstruction(const DenseVector& ep){
   Assert(!reconstructed());
-  d_exactPrecision = new DenseVector(ep);
+  d_exactPrecision.reset(new DenseVector(ep));
 }
 
 void CutInfo::setExplanation(const ConstraintCPVec& ex){
   Assert(reconstructed());
-  if(d_explanation == NULL){
-    d_explanation = new ConstraintCPVec(ex);
-  }else{
+  if (d_explanation == nullptr)
+  {
+    d_explanation.reset(new ConstraintCPVec(ex));
+  }
+  else
+  {
     *d_explanation = ex;
   }
 }
@@ -216,8 +213,9 @@ void CutInfo::setExplanation(const ConstraintCPVec& ex){
 void CutInfo::swapExplanation(ConstraintCPVec& ex){
   Assert(reconstructed());
   Assert(!proven());
-  if(d_explanation == NULL){
-    d_explanation = new ConstraintCPVec();
+  if (d_explanation == nullptr)
+  {
+    d_explanation.reset(new ConstraintCPVec());
   }
   d_explanation->swap(ex);
 }
@@ -229,13 +227,11 @@ const DenseVector& CutInfo::getReconstruction() const {
 
 void CutInfo::clearReconstruction(){
   if(proven()){
-    delete d_explanation;
-    d_explanation = NULL;
+    d_explanation = nullptr;
   }
 
   if(reconstructed()){
-    delete d_exactPrecision;
-    d_exactPrecision = NULL;
+    d_exactPrecision = nullptr;
   }
 
   Assert(!reconstructed());

diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h
index 44553a15b357a339fd44f44bfe1bb804dfdbf640..a5a729f58ce6e93ba3c5a54d43389176ffde6d2c 100644 (file)
--- a/src/theory/arith/cut_log.h
+++ b/src/theory/arith/cut_log.h
@@ -91,11 +91,11 @@ protected:
    * the cut is stored in exact precision in d_exactPrecision.
    * If the cut has not yet been proven, this is null.
    */
-  DenseVector* d_exactPrecision;
+  std::unique_ptr<DenseVector> d_exactPrecision;
 
-  ConstraintCPVec* d_explanation;
+  std::unique_ptr<ConstraintCPVec> d_explanation;
 
-public:
+ public:
   CutInfo(CutInfoKlass kl, int cutid, int ordinal);
 
   virtual ~CutInfo();

diff --git a/src/theory/type_set.cpp b/src/theory/type_set.cpp
index 616245e2b1064af1d74f687571c0051b6c56dcce..0e14f91023deda4b3d9e3a4a05dd6e218c301fd9 100644 (file)
--- a/src/theory/type_set.cpp
+++ b/src/theory/type_set.cpp
@@ -24,18 +24,12 @@ TypeSet::~TypeSet()
   iterator it;
   for (it = d_typeSet.begin(); it != d_typeSet.end(); ++it)
   {
-    if ((*it).second != NULL)
-    {
-      delete (*it).second;
-    }
+    delete (*it).second;
   }
   TypeToTypeEnumMap::iterator it2;
   for (it2 = d_teMap.begin(); it2 != d_teMap.end(); ++it2)
   {
-    if ((*it2).second != NULL)
-    {
-      delete (*it2).second;
-    }
+    delete (*it2).second;
   }
 }