From 3cf5492a8943b71bb4021f1a78cf28cdfafa4289 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 27 Aug 2018 22:41:50 -0500 Subject: [PATCH] Address more coverity warnings (#2394) --- src/theory/datatypes/sygus_simple_sym.cpp | 5 ----- src/theory/quantifiers/candidate_rewrite_database.cpp | 2 +- src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 7 ++----- src/theory/quantifiers/conjecture_generator.h | 1 + src/theory/quantifiers/ematching/candidate_generator.cpp | 5 ++++- src/theory/quantifiers/fmf/bounded_integers.cpp | 5 ++++- src/theory/quantifiers/inst_propagator.cpp | 3 ++- src/theory/quantifiers/sygus/sygus_unif_rl.h | 1 + 8 files changed, 15 insertions(+), 14 deletions(-) diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp index 4aef1231c..a35ab2a03 100644 --- a/src/theory/datatypes/sygus_simple_sym.cpp +++ b/src/theory/datatypes/sygus_simple_sym.cpp @@ -116,7 +116,6 @@ class ReqTrie std::vector argts; if (tdb->canConstructKind(tn, d_req_kind, argts)) { - bool ret = true; for (std::map::iterator it = d_children.begin(); it != d_children.end(); ++it) @@ -134,10 +133,6 @@ class ReqTrie return false; } } - if (!ret) - { - return false; - } } else { diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 3df3717c3..e5df8db8a 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -321,7 +321,7 @@ bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out) CandidateRewriteDatabaseGen::CandidateRewriteDatabaseGen( std::vector& vars, unsigned nsamples) - : d_vars(vars.begin(), vars.end()), d_nsamples(nsamples) + : d_qe(nullptr), d_vars(vars.begin(), vars.end()), d_nsamples(nsamples) { } diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 2a17f1e36..b90d98ca6 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -517,11 +517,8 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) activateInstantiationVariable(pv, i); //get the instantiator object - Instantiator * vinst = NULL; - std::map< Node, Instantiator * >::iterator itin = d_instantiator.find( pv ); - if( itin!=d_instantiator.end() ){ - vinst = itin->second; - } + Assert(d_instantiator.find(pv) != d_instantiator.end()); + Instantiator* vinst = d_instantiator[pv]; Assert( vinst!=NULL ); d_active_instantiators[pv] = vinst; vinst->reset(this, sf, pv, d_effort); diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index a3a0b8795..7d4684200 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -78,6 +78,7 @@ class TermGenerator : d_id(0), d_status(0), d_status_num(0), + d_status_child_num(0), d_match_status(0), d_match_status_child_num(0), d_match_mode(0) diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 6ea6e50b3..3f404c17f 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -34,7 +34,10 @@ bool CandidateGenerator::isLegalCandidate( Node n ){ } CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersEngine* qe, Node pat) - : CandidateGenerator(qe), d_term_iter(-1), d_term_iter_limit(0) + : CandidateGenerator(qe), + d_term_iter(-1), + d_term_iter_limit(0), + d_mode(cand_term_none) { d_op = qe->getTermDatabase()->getMatchOperator( pat ); Assert( !d_op.isNull() ); diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 8d8bf7f50..e28489b1a 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -408,7 +408,10 @@ void BoundedIntegers::checkOwnership(Node f) bool setBoundVar = false; if( it->second==BOUND_INT_RANGE ){ //must have both - if( bound_lit_map[0].find( v )!=bound_lit_map[0].end() && bound_lit_map[1].find( v )!=bound_lit_map[1].end() ){ + std::map& blm0 = bound_lit_map[0]; + std::map& blm1 = bound_lit_map[1]; + if (blm0.find(v) != blm0.end() && blm1.find(v) != blm1.end()) + { setBoundedVar( f, v, BOUND_INT_RANGE ); setBoundVar = true; for( unsigned b=0; b<2; b++ ){ diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp index 392e092b8..15dd35c26 100644 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp @@ -799,7 +799,8 @@ void InstPropagator::propagate( Node a, Node b, bool pol, std::vector< Node >& e } if( pol ){ if( status==EqualityQueryInstProp::STATUS_MERGED_KNOWN ){ - Trace("qip-rlv-propagate") << "Relevant propagation : " << a << ( pol ? " == " : " != " ) << b << std::endl; + Trace("qip-rlv-propagate") + << "Relevant propagation : " << a << " == " << b << std::endl; Assert( d_qy.getEngine()->hasTerm( a ) ); Assert( d_qy.getEngine()->hasTerm( b ) ); Trace("qip-prop-debug") << "...equality between known terms." << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index af6be2e97..c9bdf5691 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -267,6 +267,7 @@ class SygusUnifRl : public SygusUnif class PointSeparator : public LazyTrieEvaluator { public: + PointSeparator() : d_dt(nullptr) {} /** initializes this class */ void initialize(DecisionTreeInfo* dt); /** -- 2.30.2