summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/array_store_all.cpp76
-rw-r--r--test/unit/util/array_store_all_black.h47
2 files changed, 66 insertions, 57 deletions
diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp
index c8e346e48..05710a636 100644
--- a/src/expr/array_store_all.cpp
+++ b/src/expr/array_store_all.cpp
@@ -28,78 +28,72 @@ using namespace std;
namespace CVC4 {
-ArrayStoreAll::ArrayStoreAll(const ArrayStoreAll& other)
- : d_type(new ArrayType(other.getType()))
- , d_expr(new Expr(other.getExpr())) {}
-
-ArrayStoreAll::~ArrayStoreAll() throw() {
- delete d_expr;
- delete d_type;
-}
-
-ArrayStoreAll& ArrayStoreAll::operator=(const ArrayStoreAll& other){
- (*d_type) = other.getType();
- (*d_expr) = other.getExpr();
- return *this;
-}
-
-ArrayStoreAll::ArrayStoreAll(const ArrayType& type, const Expr& expr)
- throw(IllegalArgumentException)
- : d_type(new ArrayType(type))
- , d_expr(new Expr(expr))
-{
- // this check is stronger than the assertion check in the expr manager that ArrayTypes are actually array types
+ArrayStoreAll::ArrayStoreAll(const ArrayType& type,
+ const Expr& expr) throw(IllegalArgumentException)
+ : d_type(NULL), d_expr(NULL) {
+ // this check is stronger than the assertion check in the expr manager that
+ // ArrayTypes are actually array types
// because this check is done in production builds too
PrettyCheckArgument(
- type.isArray(),
- type,
+ type.isArray(), type,
"array store-all constants can only be created for array types, not `%s'",
type.toString().c_str());
PrettyCheckArgument(
- expr.getType().isComparableTo(type.getConstituentType()),
- expr,
+ expr.getType().isComparableTo(type.getConstituentType()), expr,
"expr type `%s' does not match constituent type of array type `%s'",
- expr.getType().toString().c_str(),
- type.toString().c_str());
+ expr.getType().toString().c_str(), type.toString().c_str());
- PrettyCheckArgument(
- expr.isConst(),
- expr,
- "ArrayStoreAll requires a constant expression");
+ PrettyCheckArgument(expr.isConst(), expr,
+ "ArrayStoreAll requires a constant expression");
+
+ // Delay allocation until the checks above have been performed. If these fail,
+ // the memory for d_type and d_expr should not leak. The alternative is catch,
+ // delete and re-throw.
+ d_type = new ArrayType(type);
+ d_expr = new Expr(expr);
}
+ArrayStoreAll::ArrayStoreAll(const ArrayStoreAll& other)
+ : d_type(new ArrayType(other.getType())),
+ d_expr(new Expr(other.getExpr())) {}
-const ArrayType& ArrayStoreAll::getType() const throw() {
- return *d_type;
+ArrayStoreAll::~ArrayStoreAll() throw() {
+ delete d_expr;
+ delete d_type;
}
-const Expr& ArrayStoreAll::getExpr() const throw() {
- return *d_expr;
+ArrayStoreAll& ArrayStoreAll::operator=(const ArrayStoreAll& other) {
+ (*d_type) = other.getType();
+ (*d_expr) = other.getExpr();
+ return *this;
}
+const ArrayType& ArrayStoreAll::getType() const throw() { return *d_type; }
+
+const Expr& ArrayStoreAll::getExpr() const throw() { return *d_expr; }
+
bool ArrayStoreAll::operator==(const ArrayStoreAll& asa) const throw() {
return getType() == asa.getType() && getExpr() == asa.getExpr();
}
-
bool ArrayStoreAll::operator<(const ArrayStoreAll& asa) const throw() {
return (getType() < asa.getType()) ||
- (getType() == asa.getType() && getExpr() < asa.getExpr());
+ (getType() == asa.getType() && getExpr() < asa.getExpr());
}
bool ArrayStoreAll::operator<=(const ArrayStoreAll& asa) const throw() {
return (getType() < asa.getType()) ||
- (getType() == asa.getType() && getExpr() <= asa.getExpr());
+ (getType() == asa.getType() && getExpr() <= asa.getExpr());
}
std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) {
- return out << "__array_store_all__(" << asa.getType() << ", " << asa.getExpr() << ')';
+ return out << "__array_store_all__(" << asa.getType() << ", " << asa.getExpr()
+ << ')';
}
size_t ArrayStoreAllHashFunction::operator()(const ArrayStoreAll& asa) const {
return TypeHashFunction()(asa.getType()) * ExprHashFunction()(asa.getExpr());
}
-
-}/* CVC4 namespace */
+} /* CVC4 namespace */
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback