From 8fa91361af7e891b82f9156e76b7d7e6bb70aa65 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 8 Oct 2019 17:24:49 -0700 Subject: [PATCH] New C++ API: Term: Add missing checks for null. (#3364) Co-Authored-By: Andres Noetzli --- src/api/cvc4cpp.cpp | 14 ++++++++++++++ test/unit/api/term_black.h | 14 ++++++++++++++ 2 files changed, 28 insertions(+) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 3ea0fcb01..d1112a9dc 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1072,6 +1072,7 @@ bool Term::isParameterized() const Term Term::notTerm() const { + CVC4_API_CHECK_NOT_NULL; try { Term res = d_expr->notExpr(); @@ -1086,6 +1087,8 @@ Term Term::notTerm() const Term Term::andTerm(const Term& t) const { + CVC4_API_CHECK_NOT_NULL; + CVC4_API_ARG_CHECK_NOT_NULL(t); try { Term res = d_expr->andExpr(*t.d_expr); @@ -1100,6 +1103,8 @@ Term Term::andTerm(const Term& t) const Term Term::orTerm(const Term& t) const { + CVC4_API_CHECK_NOT_NULL; + CVC4_API_ARG_CHECK_NOT_NULL(t); try { Term res = d_expr->orExpr(*t.d_expr); @@ -1114,6 +1119,8 @@ Term Term::orTerm(const Term& t) const Term Term::xorTerm(const Term& t) const { + CVC4_API_CHECK_NOT_NULL; + CVC4_API_ARG_CHECK_NOT_NULL(t); try { Term res = d_expr->xorExpr(*t.d_expr); @@ -1128,6 +1135,8 @@ Term Term::xorTerm(const Term& t) const Term Term::eqTerm(const Term& t) const { + CVC4_API_CHECK_NOT_NULL; + CVC4_API_ARG_CHECK_NOT_NULL(t); try { Term res = d_expr->eqExpr(*t.d_expr); @@ -1142,6 +1151,8 @@ Term Term::eqTerm(const Term& t) const Term Term::impTerm(const Term& t) const { + CVC4_API_CHECK_NOT_NULL; + CVC4_API_ARG_CHECK_NOT_NULL(t); try { Term res = d_expr->impExpr(*t.d_expr); @@ -1156,6 +1167,9 @@ Term Term::impTerm(const Term& t) const Term Term::iteTerm(const Term& then_t, const Term& else_t) const { + CVC4_API_CHECK_NOT_NULL; + CVC4_API_ARG_CHECK_NOT_NULL(then_t); + CVC4_API_ARG_CHECK_NOT_NULL(else_t); try { Term res = d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr); diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h index 945944467..c5300dbfe 100644 --- a/test/unit/api/term_black.h +++ b/test/unit/api/term_black.h @@ -168,6 +168,7 @@ void TermBlack::testNotTerm() Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort); Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); + TS_ASSERT_THROWS(Term().notTerm(), CVC4ApiException&); Term b = d_solver.mkTrue(); TS_ASSERT_THROWS_NOTHING(b.notTerm()); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); @@ -205,6 +206,8 @@ void TermBlack::testAndTerm() Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); + TS_ASSERT_THROWS(Term().andTerm(b), CVC4ApiException&); + TS_ASSERT_THROWS(b.andTerm(Term()), CVC4ApiException&); TS_ASSERT_THROWS_NOTHING(b.andTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); TS_ASSERT_THROWS(x.andTerm(b), CVC4ApiException&); @@ -269,6 +272,8 @@ void TermBlack::testOrTerm() Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); + TS_ASSERT_THROWS(Term().orTerm(b), CVC4ApiException&); + TS_ASSERT_THROWS(b.orTerm(Term()), CVC4ApiException&); TS_ASSERT_THROWS_NOTHING(b.orTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); TS_ASSERT_THROWS(x.orTerm(b), CVC4ApiException&); @@ -333,6 +338,8 @@ void TermBlack::testXorTerm() Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); + TS_ASSERT_THROWS(Term().xorTerm(b), CVC4ApiException&); + TS_ASSERT_THROWS(b.xorTerm(Term()), CVC4ApiException&); TS_ASSERT_THROWS_NOTHING(b.xorTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); TS_ASSERT_THROWS(x.xorTerm(b), CVC4ApiException&); @@ -397,6 +404,8 @@ void TermBlack::testEqTerm() Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); + TS_ASSERT_THROWS(Term().eqTerm(b), CVC4ApiException&); + TS_ASSERT_THROWS(b.eqTerm(Term()), CVC4ApiException&); TS_ASSERT_THROWS_NOTHING(b.eqTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); TS_ASSERT_THROWS(x.eqTerm(b), CVC4ApiException&); @@ -461,6 +470,8 @@ void TermBlack::testImpTerm() Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); + TS_ASSERT_THROWS(Term().impTerm(b), CVC4ApiException&); + TS_ASSERT_THROWS(b.impTerm(Term()), CVC4ApiException&); TS_ASSERT_THROWS_NOTHING(b.impTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); TS_ASSERT_THROWS(x.impTerm(b), CVC4ApiException&); @@ -525,6 +536,9 @@ void TermBlack::testIteTerm() Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort); Term b = d_solver.mkTrue(); + TS_ASSERT_THROWS(Term().iteTerm(b, b), CVC4ApiException&); + TS_ASSERT_THROWS(b.iteTerm(Term(), b), CVC4ApiException&); + TS_ASSERT_THROWS(b.iteTerm(b, Term()), CVC4ApiException&); TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); TS_ASSERT_THROWS_NOTHING(b.iteTerm(x, x)); -- 2.30.2