diff options
author | Tim King <taking@google.com> | 2016-11-07 11:44:52 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-11-07 11:44:52 -0800 |
commit | d9608e29789960cd50704689d39e9a35d01be321 (patch) | |
tree | 1a73c1293d21ef9ba9d0337d9ed276ffe6cea5ae /test/unit | |
parent | 6e61a7ad085774c222afa9ffcd2602b827883556 (diff) |
Changing ArrayStoreAll's constructor to delay allocation until it is done checking error conditions. This prevents a memory leak in exception throwing branches.
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/util/array_store_all_black.h | 47 |
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 */ |