summaryrefslogtreecommitdiff
path: root/src/api
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2019-10-08 17:24:49 -0700
committerGitHub <noreply@github.com>2019-10-08 17:24:49 -0700
commit8fa91361af7e891b82f9156e76b7d7e6bb70aa65 (patch)
treeff96cf082751900c84808bee7d4123c7b729ab01 /src/api
parent1b6784fe52f4fb745262842e0406d6dd34053cb2 (diff)
New C++ API: Term: Add missing checks for null. (#3364)
Co-Authored-By: Andres Noetzli <andres.noetzli@gmail.com>
Diffstat (limited to 'src/api')
-rw-r--r--src/api/cvc4cpp.cpp14
1 files changed, 14 insertions, 0 deletions
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback