From 9dcec275dd58b97c4e484ea8a7978fdf7ea88453 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 8 Jun 2020 13:12:52 -0700 Subject: [PATCH] Fix Coverity issues (#4587) This commit fixes the following Coverity issues: - 1495606: uninitialized field - 1495605: uninitialized field - 1488953: uninitialized field - 1495604: mismatched iterator --- src/api/cvc4cpp.cpp | 6 +++--- src/theory/arith/nl/nl_monomial.cpp | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 88974dc69..325da8cdb 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1119,7 +1119,7 @@ size_t SortHashFunction::operator()(const Sort& s) const /* Op */ /* -------------------------------------------------------------------------- */ -Op::Op() : d_kind(NULL_EXPR), d_expr(new CVC4::Expr()) {} +Op::Op() : d_solver(nullptr), d_kind(NULL_EXPR), d_expr(new CVC4::Expr()) {} Op::Op(const Solver* slv, const Kind k) : d_solver(slv), d_kind(k), d_expr(new CVC4::Expr()) @@ -1628,7 +1628,7 @@ Term::const_iterator::const_iterator(const Solver* slv, } Term::const_iterator::const_iterator(const const_iterator& it) - : d_orig_expr(nullptr) + : d_solver(nullptr), d_orig_expr(nullptr) { if (it.d_orig_expr != nullptr) { @@ -1920,7 +1920,7 @@ std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl) /* DatatypeSelector --------------------------------------------------------- */ -DatatypeSelector::DatatypeSelector() { d_stor = nullptr; } +DatatypeSelector::DatatypeSelector() : d_solver(nullptr), d_stor(nullptr) {} DatatypeSelector::DatatypeSelector(const Solver* slv, const CVC4::DatatypeConstructorArg& stor) diff --git a/src/theory/arith/nl/nl_monomial.cpp b/src/theory/arith/nl/nl_monomial.cpp index e8e7aceba..678a94819 100644 --- a/src/theory/arith/nl/nl_monomial.cpp +++ b/src/theory/arith/nl/nl_monomial.cpp @@ -276,7 +276,7 @@ Node MonomialDb::getContainsDiff(Node a, Node b) const { std::map >::const_iterator it = d_m_contain_mult.find(a); - if (it == d_m_contain_umult.end()) + if (it == d_m_contain_mult.end()) { return Node::null(); } -- 2.30.2