diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-09-12 16:41:18 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-09-12 16:41:18 -0700 |
commit | d80588a41753d011202d670dbf7123233b665af9 (patch) | |
tree | 08c4c8bfd24ef153e18f484d1026d8076e8ec0ca /src/api | |
parent | fa79faf9e6ca816e8310f96c95623633e63f7bef (diff) |
New C++ API: Try to fix (false positive) Coverity warnings. (#2454)
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cvc4cpp.cpp | 25 |
1 files changed, 21 insertions, 4 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 24c4ef833..8aed4fb32 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -609,7 +609,16 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> }; namespace { -bool isDefinedKind(Kind k) { return k > UNDEFINED_KIND && k < LAST_KIND; } + +bool isDefinedKind(Kind k) +{ + return k > UNDEFINED_KIND && k < LAST_KIND; +} + +bool isDefinedIntKind(CVC4::Kind k) +{ + return k != CVC4::Kind::UNDEFINED_KIND && k != CVC4::Kind::LAST_KIND; +} Kind intToExtKind(CVC4::Kind k) { @@ -2044,7 +2053,9 @@ Term Solver::mkTerm(Kind kind) const kindToString(kind).c_str()); if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA) { - return d_exprMgr->mkExpr(extToIntKind(kind), std::vector<Expr>()); + CVC4::Kind k = extToIntKind(kind); + Assert(isDefinedIntKind(k)); + return d_exprMgr->mkExpr(k, std::vector<Expr>()); } Assert(kind == PI); return d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI); @@ -2079,7 +2090,9 @@ Term Solver::mkTerm(Kind kind, Term child) const kind, "Invalid kind '%s'", kindToString(kind).c_str()); - return d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr); + CVC4::Kind k = extToIntKind(kind); + Assert(isDefinedIntKind(k)); + return d_exprMgr->mkExpr(k, *child.d_expr); } Term Solver::mkTerm(Kind kind, Term child1, Term child2) const @@ -2104,7 +2117,9 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2) const // n < minArity(kind) || n > maxArity(kind) // else "Exprs with kind %s must have at least %u children and " // "at most %u children (the one under construction has %u)" - return d_exprMgr->mkExpr(extToIntKind(kind), *child1.d_expr, *child2.d_expr); + CVC4::Kind k = extToIntKind(kind); + Assert(isDefinedIntKind(k)); + return d_exprMgr->mkExpr(k, *child1.d_expr, *child2.d_expr); } Term Solver::mkTerm(Kind kind, Term child1, Term child2, Term child3) const @@ -2133,6 +2148,7 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2, Term child3) const kindToString(kind).c_str()); std::vector<Expr> echildren{*child1.d_expr, *child2.d_expr, *child3.d_expr}; CVC4::Kind k = extToIntKind(kind); + Assert(isDefinedIntKind(k)); return kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren) : d_exprMgr->mkExpr(k, echildren); } @@ -2160,6 +2176,7 @@ Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const kindToString(kind).c_str()); std::vector<Expr> echildren = termVectorToExprs(children); CVC4::Kind k = extToIntKind(kind); + Assert(isDefinedIntKind(k)); return kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren) : d_exprMgr->mkExpr(k, echildren); } |