From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 8 Jun 2020 20:12:52 +0000 (-0700)
Subject: Fix Coverity issues (#4587)
X-Git-Tag: cvc5-1.0.0~3240
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9dcec275dd58b97c4e484ea8a7978fdf7ea88453;p=cvc5.git

Fix Coverity issues (#4587)

This commit fixes the following Coverity issues:

- 1495606: uninitialized field
- 1495605: uninitialized field
- 1488953: uninitialized field
- 1495604: mismatched iterator
---

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<Node, std::map<Node, Node> >::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();
   }