Changing ArrayStoreAll's constructor to delay allocation until it is done checking error conditions. This prevents a memory leak in exception throwing branches.

1 files changed, 31 insertions, 16 deletions

diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h
index 6465a6301..981ed418d 100644
--- a/test/unit/util/array_store_all_black.h
+++ b/test/unit/util/array_store_all_black.h
@@ -17,21 +17,19 @@
 #include <cxxtest/TestSuite.h>
 
 #include "expr/array_store_all.h"
+#include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "expr/expr_manager_scope.h"
 #include "expr/type.h"
-#include "expr/expr.h"
 
 using namespace CVC4;
 using namespace std;
 
 class ArrayStoreAllBlack : public CxxTest::TestSuite {
-
   ExprManager* d_em;
   ExprManagerScope* d_scope;
 
-public:
-
+ public:
   void setUp() {
     d_em = new ExprManager();
     d_scope = new ExprManagerScope(*d_em);
@@ -44,25 +42,42 @@ public:
 
   void testStoreAll() {
     Type usort = d_em->mkSort("U");
-    ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->realType()), d_em->mkConst(Rational(9, 2)));
-    ArrayStoreAll(d_em->mkArrayType(d_em->mkSort("U"), usort), d_em->mkConst(UninterpretedConstant(usort, 0)));
-    ArrayStoreAll(d_em->mkArrayType(d_em->mkBitVectorType(8), d_em->realType()), d_em->mkConst(Rational(0)));
-    ArrayStoreAll(d_em->mkArrayType(d_em->mkBitVectorType(8), d_em->integerType()), d_em->mkConst(Rational(0)));
+    ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->realType()),
+                  d_em->mkConst(Rational(9, 2)));
+    ArrayStoreAll(d_em->mkArrayType(d_em->mkSort("U"), usort),
+                  d_em->mkConst(UninterpretedConstant(usort, 0)));
+    ArrayStoreAll(d_em->mkArrayType(d_em->mkBitVectorType(8), d_em->realType()),
+                  d_em->mkConst(Rational(0)));
+    ArrayStoreAll(
+        d_em->mkArrayType(d_em->mkBitVectorType(8), d_em->integerType()),
+        d_em->mkConst(Rational(0)));
   }
 
   void testTypeErrors() {
-    // these two throw an AssertionException in assertions-enabled builds, and an IllegalArgumentException in production builds
-    TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->integerType(), d_em->mkConst(UninterpretedConstant(d_em->mkSort("U"), 0))) );
-    TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->integerType(), d_em->mkConst(Rational(9, 2))) );
+    // these two throw an AssertionException in assertions-enabled builds, and
+    // an IllegalArgumentException in production builds
+    TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll(
+        d_em->integerType(),
+        d_em->mkConst(UninterpretedConstant(d_em->mkSort("U"), 0))));
+    TS_ASSERT_THROWS_ANYTHING(
+        ArrayStoreAll(d_em->integerType(), d_em->mkConst(Rational(9, 2))));
 
-    TS_ASSERT_THROWS( ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->mkSort("U")), d_em->mkConst(Rational(9, 2))), IllegalArgumentException );
+    TS_ASSERT_THROWS(
+        ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->mkSort("U")),
+                      d_em->mkConst(Rational(9, 2))),
+        IllegalArgumentException);
   }
 
   void testConstError() {
     Type usort = d_em->mkSort("U");
-    TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->mkArrayType(d_em->mkSort("U"), usort), d_em->mkVar(usort)) );
-    TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->integerType(), d_em->mkVar("x", d_em->integerType())) );
-    TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->integerType(), d_em->mkExpr(kind::PLUS, d_em->mkConst(Rational(1)), d_em->mkConst(Rational(0)))) );
+    TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll(
+        d_em->mkArrayType(d_em->mkSort("U"), usort), d_em->mkVar(usort)));
+    TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll(
+        d_em->integerType(), d_em->mkVar("x", d_em->integerType())));
+    TS_ASSERT_THROWS_ANYTHING(
+        ArrayStoreAll(d_em->integerType(),
+                      d_em->mkExpr(kind::PLUS, d_em->mkConst(Rational(1)),
+                                   d_em->mkConst(Rational(0)))));
   }
 
-};/* class ArrayStoreAllBlack */
+}; /* class ArrayStoreAllBlack */