From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 9 Oct 2019 00:24:49 +0000 (-0700)
Subject: New C++ API: Term: Add missing checks for null. (#3364)
X-Git-Tag: cvc5-1.0.0~3902
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8fa91361af7e891b82f9156e76b7d7e6bb70aa65;p=cvc5.git

New C++ API: Term: Add missing checks for null. (#3364)

Co-Authored-By: Andres Noetzli <andres.noetzli@gmail.com>
---

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));