From: Mathias Preiner Date: Thu, 25 Feb 2021 00:26:44 +0000 (-0800) Subject: Enable -Werror. (#5969) X-Git-Tag: cvc5-1.0.0~2216 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e36aeda0e759c5328ba76412dde8afbecf34970b;p=cvc5.git Enable -Werror. (#5969) --- diff --git a/CMakeLists.txt b/CMakeLists.txt index 3dd282a8d..c32c10f4d 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -234,8 +234,9 @@ include(Config${CMAKE_BUILD_TYPE}) add_check_c_cxx_flag("-O${OPTIMIZATION_LEVEL}") add_check_c_cxx_flag("-Wall") +add_check_c_cxx_flag("-Werror") +add_check_c_cxx_flag("-Wno-unused-private-field") add_check_c_flag("-fexceptions") -add_check_c_cxx_flag("-Wno-deprecated") add_check_cxx_flag("-Wsuggest-override") add_check_cxx_flag("-Wnon-virtual-dtor") add_check_c_cxx_flag("-Wimplicit-fallthrough") diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 10f39cb38..0c94320c3 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -748,7 +748,7 @@ class CVC4ApiExceptionStream * default to noexcept(true) (else this triggers a call to std::terminate). */ ~CVC4ApiExceptionStream() noexcept(false) { - if (!std::uncaught_exception()) + if (std::uncaught_exceptions() == 0) { throw CVC4ApiException(d_stream.str()); } @@ -769,7 +769,7 @@ class CVC4ApiRecoverableExceptionStream * default to noexcept(true) (else this triggers a call to std::terminate). */ ~CVC4ApiRecoverableExceptionStream() noexcept(false) { - if (!std::uncaught_exception()) + if (std::uncaught_exceptions() == 0) { throw CVC4ApiRecoverableException(d_stream.str()); } diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt index dde29110f..211fb5ff8 100644 --- a/src/api/python/CMakeLists.txt +++ b/src/api/python/CMakeLists.txt @@ -48,6 +48,12 @@ add_library(pycvc4 target_link_libraries(pycvc4 cvc4 ${PYTHON_LIBRARIES}) +# Disable -Werror and other warnings for code generated by Cython. +set_target_properties(pycvc4 + PROPERTIES + COMPILE_FLAGS + "-Wno-error -Wno-shadow -Wno-implicit-fallthrough") + python_extension_module(pycvc4) # Installation based on https://bloerg.net/2012/11/10/cmake-and-distutils.html diff --git a/src/expr/node_trie.cpp b/src/expr/node_trie.cpp index 58ad36da9..d2da99509 100644 --- a/src/expr/node_trie.cpp +++ b/src/expr/node_trie.cpp @@ -24,7 +24,7 @@ NodeTemplate NodeTemplateTrie::existsTerm( const NodeTemplateTrie* tnt = this; typename std::map, NodeTemplateTrie>::const_iterator it; - for (const NodeTemplate r : reps) + for (const NodeTemplate& r : reps) { it = tnt->d_data.find(r); if (it == tnt->d_data.end()) @@ -51,7 +51,7 @@ NodeTemplate NodeTemplateTrie::addOrGetTerm( NodeTemplate n, const std::vector>& reps) { NodeTemplateTrie* tnt = this; - for (const NodeTemplate r : reps) + for (const NodeTemplate& r : reps) { tnt = &(tnt->d_data[r]); } diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt index 8e69da34b..2fe92fb45 100644 --- a/src/parser/CMakeLists.txt +++ b/src/parser/CMakeLists.txt @@ -93,7 +93,7 @@ foreach(lang Cvc Smt2 Tptp) # We don't want to enable -Wall for code generated by ANTLR. set_source_files_properties( - ${gen_src_files} PROPERTIES COMPILE_FLAGS -Wno-all) + ${gen_src_files} PROPERTIES COMPILE_FLAGS "-Wno-all -Wno-error") # Add generated source files to the parser source files list(APPEND libcvc4parser_src_files ${gen_src_files}) diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index f5d840a49..4712db91f 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -691,6 +691,9 @@ Node BVToInt::translateWithChildren(Node original, { // Exists is eliminated by the rewriter. Assert(false); +#ifdef NDEBUG + CVC4_FALLTHROUGH; +#endif } default: { diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp index 0e4e21b76..5b7edb3ef 100644 --- a/src/theory/arith/nl/poly_conversion.cpp +++ b/src/theory/arith/nl/poly_conversion.cpp @@ -452,9 +452,11 @@ Node lower_bound_as_node(const Node& var, poly::get_upper(poly::get_isolating_interval(alg))); int sl = poly::sign_at(get_defining_polynomial(alg), poly::get_lower(poly::get_isolating_interval(alg))); +#ifndef NDEBUG int su = poly::sign_at(get_defining_polynomial(alg), poly::get_upper(poly::get_isolating_interval(alg))); Assert(sl != 0 && su != 0 && sl != su); +#endif // open: var <= l or (var < u and sgn(poly(var)) == sl) // !open: var <= l or (var < u and sgn(poly(var)) == sl/0) @@ -506,8 +508,10 @@ Node upper_bound_as_node(const Node& var, poly::get_lower(poly::get_isolating_interval(alg))); Rational u = poly_utils::toRational( poly::get_upper(poly::get_isolating_interval(alg))); +#ifndef NDEBUG int sl = poly::sign_at(get_defining_polynomial(alg), poly::get_lower(poly::get_isolating_interval(alg))); +#endif int su = poly::sign_at(get_defining_polynomial(alg), poly::get_upper(poly::get_isolating_interval(alg))); Assert(sl != 0 && su != 0 && sl != su); diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index f07140d4e..4dd7dcafd 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -936,7 +936,10 @@ void TheoryArrays::checkPair(TNode r1, TNode r2) case EQUALITY_FALSE_AND_PROPAGATED: // Should have been propagated to us Assert(false); - case EQUALITY_FALSE: +#ifdef NDEBUG + CVC4_FALLTHROUGH; +#endif + case EQUALITY_FALSE: CVC4_FALLTHROUGH; case EQUALITY_FALSE_IN_MODEL: // This is unlikely, but I think it could happen Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checkPair called when false in model" << std::endl; diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index 24e821e33..726160d83 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -252,8 +252,10 @@ void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment) else { // AND = FALSE: if all children BUT ONE == TRUE, assign(c = FALSE) - TNode::iterator holdout = find_if_unique( - parent.begin(), parent.end(), not1(IsAssignedTo(*this, true))); + TNode::iterator holdout = + find_if_unique(parent.begin(), parent.end(), [this](TNode x) { + return !isAssignedTo(x, true); + }); if (holdout != parent.end()) { assignAndEnqueue(*holdout, false, prover.andFalse(parent, holdout)); @@ -264,8 +266,10 @@ void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment) if (parentAssignment) { // OR = TRUE: if all children BUT ONE == FALSE, assign(c = TRUE) - TNode::iterator holdout = find_if_unique( - parent.begin(), parent.end(), not1(IsAssignedTo(*this, false))); + TNode::iterator holdout = + find_if_unique(parent.begin(), parent.end(), [this](TNode x) { + return !isAssignedTo(x, false); + }); if (holdout != parent.end()) { assignAndEnqueue(*holdout, true, prover.orTrue(parent, holdout)); @@ -450,8 +454,10 @@ void CircuitPropagator::propagateForward(TNode child, bool childAssignment) if (childAssignment) { TNode::iterator holdout; - holdout = find_if( - parent.begin(), parent.end(), not1(IsAssignedTo(*this, true))); + holdout = find_if(parent.begin(), parent.end(), [this](TNode x) { + return !isAssignedTo(x, true); + }); + if (holdout == parent.end()) { // all children are assigned TRUE // AND ...(x=TRUE)...: if all children now assigned to TRUE, @@ -461,8 +467,10 @@ void CircuitPropagator::propagateForward(TNode child, bool childAssignment) else if (isAssignedTo(parent, false)) { // the AND is FALSE // is the holdout unique ? - TNode::iterator other = find_if( - holdout + 1, parent.end(), not1(IsAssignedTo(*this, true))); + TNode::iterator other = + find_if(holdout + 1, parent.end(), [this](TNode x) { + return !isAssignedTo(x, true); + }); if (other == parent.end()) { // the holdout is unique // AND ...(x=TRUE)...: if all children BUT ONE now assigned to @@ -487,8 +495,9 @@ void CircuitPropagator::propagateForward(TNode child, bool childAssignment) else { TNode::iterator holdout; - holdout = find_if( - parent.begin(), parent.end(), not1(IsAssignedTo(*this, false))); + holdout = find_if(parent.begin(), parent.end(), [this](TNode x) { + return !isAssignedTo(x, false); + }); if (holdout == parent.end()) { // all children are assigned FALSE // OR ...(x=FALSE)...: if all children now assigned to FALSE, @@ -498,8 +507,10 @@ void CircuitPropagator::propagateForward(TNode child, bool childAssignment) else if (isAssignedTo(parent, true)) { // the OR is TRUE // is the holdout unique ? - TNode::iterator other = find_if( - holdout + 1, parent.end(), not1(IsAssignedTo(*this, false))); + TNode::iterator other = + find_if(holdout + 1, parent.end(), [this](TNode x) { + return !isAssignedTo(x, false); + }); if (other == parent.end()) { // the holdout is unique // OR ...(x=FALSE)...: if all children BUT ONE now assigned to diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 3546a4d35..469a01815 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -169,35 +169,6 @@ class CircuitPropagator T& d_data; }; /* class DataClearer */ - /** Predicate for use in STL functions. */ - class IsAssigned : public std::unary_function - { - CircuitPropagator& d_circuit; - - public: - IsAssigned(CircuitPropagator& circuit) : d_circuit(circuit) {} - - bool operator()(TNode in) const { return d_circuit.isAssigned(in); } - }; /* class IsAssigned */ - - /** Predicate for use in STL functions. */ - class IsAssignedTo : public std::unary_function - { - CircuitPropagator& d_circuit; - bool d_value; - - public: - IsAssignedTo(CircuitPropagator& circuit, bool value) - : d_circuit(circuit), d_value(value) - { - } - - bool operator()(TNode in) const - { - return d_circuit.isAssignedTo(in, d_value); - } - }; /* class IsAssignedTo */ - /** * Assignment status of each node. */ diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp index 83662a50f..405dae250 100644 --- a/src/theory/booleans/proof_checker.cpp +++ b/src/theory/booleans/proof_checker.cpp @@ -272,7 +272,7 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, { if (lits[j] == rhsElim) { - rhsElim == Node::null(); + rhsElim = Node::null(); continue; } auto it = lhsElim.find(lits[j]); diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp index 39dd8ed22..6b2f1b7f8 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp @@ -131,7 +131,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, TNode t = tat->getData(); Debug("simple-trigger") << "Actual term is " << t << std::endl; // convert to actual used terms - for (const std::pair& v : d_var_num) + for (const auto& v : d_var_num) { if (v.second >= 0) { diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 2e9093b82..a9ac7d0d2 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -383,7 +383,7 @@ void Skolemize::getSkolemTermVectors( { std::unordered_map, NodeHashFunction>::const_iterator itk; - for (const std::pair& p : d_skolemized) + for (const auto& p : d_skolemized) { Node q = p.first; itk = d_skolem_constants.find(q); diff --git a/src/util/real_algebraic_number_poly_imp.cpp b/src/util/real_algebraic_number_poly_imp.cpp index 674850534..e0a56f610 100644 --- a/src/util/real_algebraic_number_poly_imp.cpp +++ b/src/util/real_algebraic_number_poly_imp.cpp @@ -60,6 +60,7 @@ RealAlgebraicNumber::RealAlgebraicNumber(const std::vector& coefficients, long lower, long upper) { +#ifndef NDEBUG for (long c : coefficients) { Assert(std::numeric_limits::min() <= c @@ -67,6 +68,7 @@ RealAlgebraicNumber::RealAlgebraicNumber(const std::vector& coefficients, << "Coefficients need to fit within 32 bit integers. Please use the " "constructor based on Integer instead."; } +#endif d_value = poly::AlgebraicNumber(poly::UPolynomial(coefficients), poly::DyadicInterval(lower, upper)); } diff --git a/test/unit/theory/logic_info_white.cpp b/test/unit/theory/logic_info_white.cpp index 7ffbd6d2a..5dc8c45cb 100644 --- a/test/unit/theory/logic_info_white.cpp +++ b/test/unit/theory/logic_info_white.cpp @@ -27,8 +27,8 @@ namespace test { class TestTheoryWhiteLogicInfo : public TestInternal { -#warning \ - "This test is of questionable compatiblity with contrib/new-theory. Is the new theory id handled correctly by the Logic info." + // This test is of questionable compatiblity with contrib/new-theory. Is the + // new theory id handled correctly by the Logic info. protected: void eq(const LogicInfo& logic1, const LogicInfo& logic2) const {