Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add and fix a few general compiler warnings. #5628

Merged
merged 10 commits into from
Oct 29, 2021
21 changes: 21 additions & 0 deletions cmake/compiler_warnings.cmake
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,27 @@ set(CLANG_WARNINGS_AS_ERRORS
"-Werror=delete-non-virtual-dtor"
# https://clang.llvm.org/docs/DiagnosticsReference.html#woverloaded-virtual
"-Werror=overloaded-virtual"
# warn the user if a class with virtual functions has a
# non-virtual destructor. This helps catch hard to
# track down memory errors
"-Werror=non-virtual-dtor"
# warn if a null dereference is detected
"-Werror=null-dereference"
# warn for potential performance problem casts
# "-Werror=cast-align"
# warn if float is implicit promoted to double
# "-Werror=double-promotion"
"-Werror=no-unreachable-code-return"
# warn the user if a variable declaration shadows one from a parent context
# "-Werror=shadow"
# warn for c-style casts
# "-Werror=old-style-cast"
# warn on sign conversions
# "-Werror=sign-conversion"
# warn on type conversions that may lose data
# "-Werror=conversion"
# warn on anything being unused
# "-Werror=unused"
)

################################################################################
Expand Down
2 changes: 2 additions & 0 deletions examples/c++/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,8 @@ add_executable(cpp_example example.cpp)
target_include_directories(cpp_example PRIVATE ${Z3_CXX_INCLUDE_DIRS})
target_link_libraries(cpp_example PRIVATE ${Z3_LIBRARIES})

target_compile_options(cpp_example PRIVATE ${Z3_COMPONENT_CXX_FLAGS})

if (CMAKE_SYSTEM_NAME MATCHES "[Ww]indows")
# On Windows we need to copy the Z3 libraries
# into the same directory as the executable
Expand Down
2 changes: 2 additions & 0 deletions src/api/c++/z3++.h
Original file line number Diff line number Diff line change
Expand Up @@ -3940,6 +3940,8 @@ namespace z3 {
virtual void push() = 0;
virtual void pop(unsigned num_scopes) = 0;

virtual ~user_propagator_base() = default;

/**
\brief user_propagators created using \c fresh() are created during
search and their lifetimes are restricted to search time. They should
Expand Down
1 change: 1 addition & 0 deletions src/ast/ast.h
Original file line number Diff line number Diff line change
Expand Up @@ -1399,6 +1399,7 @@ inline bool has_labels(expr const * n) {
class some_value_proc {
public:
virtual expr * operator()(sort * s) = 0;
virtual ~some_value_proc() = default;
};

// -----------------------------------
Expand Down
1 change: 1 addition & 0 deletions src/ast/ast_smt_pp.h
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,7 @@ class ast_smt_pp {
public:
virtual bool operator()(func_decl* d) const { return false; }
virtual bool operator()(sort* s) const { return false; }
virtual ~is_declared() = default;
};
private:
ast_manager& m_manager;
Expand Down
2 changes: 1 addition & 1 deletion src/ast/fpa/fpa2bv_converter.h
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ class fpa2bv_converter {
public:

fpa2bv_converter(ast_manager & m);
~fpa2bv_converter();
virtual ~fpa2bv_converter();

fpa_util & fu() { return m_util; }
bv_util & bu() { return m_bv_util; }
Expand Down
1 change: 1 addition & 0 deletions src/ast/is_variable_test.h
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ Revision History:

class is_variable_proc {
public:
virtual ~is_variable_proc() = default;
virtual bool operator()(const expr* e) const = 0;
};

Expand Down
1 change: 1 addition & 0 deletions src/ast/normal_forms/name_exprs.h
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ Module Name:

class expr_predicate {
public:
virtual ~expr_predicate() = default;
virtual bool operator()(expr * t) = 0;
};

Expand Down
2 changes: 2 additions & 0 deletions src/ast/num_occurs.h
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,8 @@ class num_occurs {
m_ignore_quantifiers(ignore_quantifiers) {
}

virtual ~num_occurs() = default;

void validate();
virtual void reset() { m_num_occurs.reset(); }

Expand Down
1 change: 1 addition & 0 deletions src/ast/recfun_decl_plugin.h
Original file line number Diff line number Diff line change
Expand Up @@ -93,6 +93,7 @@ namespace recfun {
// closure for computing whether a `rhs` expression is immediate
struct is_immediate_pred {
virtual bool operator()(expr * rhs) = 0;
virtual ~is_immediate_pred() = default;
};

class def {
Expand Down
1 change: 1 addition & 0 deletions src/ast/rewriter/push_app_ite.h
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,7 @@ struct push_app_ite_cfg : public default_rewriter_cfg {
virtual bool is_target(func_decl * decl, unsigned num_args, expr * const * args);
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr);
push_app_ite_cfg(ast_manager& m): m(m), m_conservative(true) {}
virtual ~push_app_ite_cfg() = default;
void set_conservative(bool c) { m_conservative = c; }
bool rewrite_patterns() const { return false; }
};
Expand Down
1 change: 1 addition & 0 deletions src/ast/rewriter/seq_eq_solver.h
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ namespace seq {

class eq_solver_context {
public:
virtual ~eq_solver_context() = default;
virtual void add_consequence(bool uses_dep, expr_ref_vector const& clause) = 0;
virtual void add_solution(expr* var, expr* term) = 0;
virtual expr* expr2rep(expr* e) = 0;
Expand Down
7 changes: 3 additions & 4 deletions src/ast/rewriter/seq_rewriter.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -3046,7 +3046,6 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
auto nothing = [&]() { return expr_ref(re().mk_empty(r->get_sort()), m()); };
auto epsilon = [&]() { return expr_ref(re().mk_epsilon(seq_sort), m()); };
auto dotstar = [&]() { return expr_ref(re().mk_full_seq(r->get_sort()), m()); };
auto dotplus = [&]() { return expr_ref(re().mk_plus(re().mk_full_char(r->get_sort())), m()); };
unsigned lo = 0, hi = 0;
if (re().is_empty(r) || re().is_epsilon(r))
// D(e,[]) = D(e,()) = []
Expand Down Expand Up @@ -3182,7 +3181,7 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
else if (re().is_loop(r, r1, lo))
result = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), re().mk_loop(r1, lo - 1));
else if (re().is_loop(r, r1, lo, hi)) {
if (lo == 0 && hi == 0 || hi < lo)
if ((lo == 0 && hi == 0) || hi < lo)
result = nothing();
else
result = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), re().mk_loop(r1, (lo == 0 ? 0 : lo - 1), hi - 1));
Expand Down Expand Up @@ -3260,7 +3259,7 @@ expr_ref seq_rewriter::mk_antimirov_deriv_concat(expr* d, expr* r) {
}

expr_ref seq_rewriter::mk_antimirov_deriv_negate(expr* d) {
sort* seq_sort = nullptr, * ele_sort = nullptr;
sort* seq_sort = nullptr;
VERIFY(m_util.is_re(d, seq_sort));
auto nothing = [&]() { return expr_ref(re().mk_empty(d->get_sort()), m()); };
auto epsilon = [&]() { return expr_ref(re().mk_epsilon(seq_sort), m()); };
Expand Down Expand Up @@ -3404,7 +3403,7 @@ expr_ref seq_rewriter::simplify_path(expr* path) {
result = simplify_path(t);
else if (m().is_true(t))
result = simplify_path(h);
else if (m().is_eq(h, lhs, rhs) || m().is_not(h, h1) && m().is_eq(h1, lhs, rhs))
else if (m().is_eq(h, lhs, rhs) || (m().is_not(h, h1) && m().is_eq(h1, lhs, rhs)))
elim_condition(lhs, result);
}
return result;
Expand Down
1 change: 1 addition & 0 deletions src/math/hilbert/heap_trie.h
Original file line number Diff line number Diff line change
Expand Up @@ -270,6 +270,7 @@ class heap_trie {
class check_value {
public:
virtual bool operator()(Value const& v) = 0;
virtual ~check_value() = default;
};

bool find_le(Key const* keys, check_value& check) {
Expand Down
1 change: 1 addition & 0 deletions src/math/lp/column_namer.h
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ Revision History:
namespace lp {
class column_namer {
public:
virtual ~column_namer() = default;
virtual std::string get_variable_name(unsigned j) const = 0;
template <typename T>
std::ostream & print_row(const row_strip<T> & row, std::ostream & out) const {
Expand Down
2 changes: 2 additions & 0 deletions src/math/lp/factorization.h
Original file line number Diff line number Diff line change
Expand Up @@ -120,6 +120,8 @@ struct factorization_factory {
m_vars(vars), m_monic(m) {
}

virtual ~factorization_factory() = default;

bool_vector get_mask() const {
// we keep the last element always in the first factor to avoid
// repeating a pair twice, that is why m_mask is shorter by one then m_vars
Expand Down
1 change: 1 addition & 0 deletions src/math/lp/lp_settings.h
Original file line number Diff line number Diff line change
Expand Up @@ -99,6 +99,7 @@ template <typename X> bool is_epsilon_small(const X & v, const double& eps);

class lp_resource_limit {
public:
virtual ~lp_resource_limit() = default;
virtual bool get_cancel_flag() = 0;
};

Expand Down
3 changes: 3 additions & 0 deletions src/math/polynomial/polynomial.h
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,7 @@ namespace polynomial {
template<typename ValManager, typename Value = typename ValManager::numeral>
class var2value {
public:
virtual ~var2value() = default;
virtual ValManager & m() const = 0;
virtual bool contains(var x) const = 0;
virtual Value const & operator()(var x) const = 0;
Expand Down Expand Up @@ -100,6 +101,7 @@ namespace polynomial {

struct display_var_proc {
virtual std::ostream& operator()(std::ostream & out, var x) const { return out << "x" << x; }
virtual ~display_var_proc() = default;
};

class polynomial;
Expand Down Expand Up @@ -228,6 +230,7 @@ namespace polynomial {
del_eh * m_next;
public:
del_eh():m_next(nullptr) {}
virtual ~del_eh() = default;
virtual void operator()(polynomial * p) = 0;
};

Expand Down
2 changes: 2 additions & 0 deletions src/math/polynomial/upolynomial_factorization_int.h
Original file line number Diff line number Diff line change
Expand Up @@ -175,6 +175,8 @@ namespace upolynomial {
m_current_size = 0;
}

virtual ~factorization_combination_iterator_base() = default;

/**
\brief Returns the factors we are enumerating through.
*/
Expand Down
1 change: 1 addition & 0 deletions src/math/realclosure/realclosure.h
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ namespace realclosure {

class mk_interval {
public:
virtual ~mk_interval() = default;
virtual void operator()(unsigned k, mpqi_manager & im, mpqi_manager::interval & r) = 0;
};

Expand Down
1 change: 1 addition & 0 deletions src/math/subpaving/subpaving_types.h
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@ class power : public std::pair<var, unsigned> {
};

struct display_var_proc {
virtual ~display_var_proc() = default;
virtual void operator()(std::ostream & out, var x) const { out << "x" << x; }
};

Expand Down
1 change: 0 additions & 1 deletion src/model/model_evaluator.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -162,7 +162,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
result_pr = nullptr;
family_id fid = f->get_family_id();
bool _is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
func_decl* g = nullptr;
br_status st = BR_FAILED;
#if 0
struct pp {
Expand Down
1 change: 1 addition & 0 deletions src/muz/base/dl_engine_base.h
Original file line number Diff line number Diff line change
Expand Up @@ -122,6 +122,7 @@ namespace datalog {

class register_engine_base {
public:
virtual ~register_engine_base() = default;
virtual engine_base* mk_engine(DL_ENGINE engine_type) = 0;
virtual void set_context(context* ctx) = 0;
};
Expand Down
1 change: 1 addition & 0 deletions src/nlsat/nlsat_solver.h
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ namespace nlsat {

class display_assumption_proc {
public:
virtual ~display_assumption_proc() = default;
virtual std::ostream& operator()(std::ostream& out, assumption a) const = 0;
};

Expand Down
1 change: 1 addition & 0 deletions src/opt/opt_context.h
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,7 @@ namespace opt {

class maxsat_context {
public:
virtual ~maxsat_context() = default;
virtual generic_model_converter& fm() = 0; // converter that removes fresh names introduced by simplification.
virtual bool sat_enabled() const = 0; // is using th SAT solver core enabled?
virtual solver& get_solver() = 0; // retrieve solver object (SAT or SMT solver)
Expand Down
1 change: 1 addition & 0 deletions src/opt/opt_pareto.h
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ namespace opt {

class pareto_callback {
public:
virtual ~pareto_callback() = default;
virtual unsigned num_objectives() = 0;
virtual expr_ref mk_gt(unsigned i, model_ref& model) = 0;
virtual expr_ref mk_ge(unsigned i, model_ref& model) = 0;
Expand Down
1 change: 1 addition & 0 deletions src/qe/nlarith_util.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -989,6 +989,7 @@ namespace nlarith {
imp& m_imp;
public:
isubst(imp& i) : m_imp(i) {}
virtual ~isubst() = default;
virtual void mk_lt(poly const& p, app_ref& r) = 0;
virtual void mk_eq(poly const& p, app_ref& r) = 0;
virtual void mk_le(poly const& p, app_ref& r) {
Expand Down
1 change: 1 addition & 0 deletions src/qe/qe.h
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ namespace qe {

class i_nnf_atom {
public:
virtual ~i_nnf_atom() = default;
virtual void operator()(expr* e, bool pol, expr_ref& result) = 0;
};

Expand Down
1 change: 1 addition & 0 deletions src/sat/sat_extension.h
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@ namespace sat {
class literal_occs_fun {
public:
virtual double operator()(literal l) = 0;
virtual ~literal_occs_fun() = default;
};


Expand Down
1 change: 0 additions & 1 deletion src/sat/sat_solver.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1893,7 +1893,6 @@ namespace sat {
void solver::init_ext_assumptions() {
if (m_ext && m_ext->tracking_assumptions()) {
m_ext_assumption_set.reset();
unsigned trail_size = m_trail.size();
if (!inconsistent())
m_ext->add_assumptions(m_ext_assumption_set);
}
Expand Down
2 changes: 1 addition & 1 deletion src/sat/smt/array_model.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,7 @@ namespace array {

bool solver::must_have_different_model_values(theory_var v1, theory_var v2) {
euf::enode* else1 = nullptr, * else2 = nullptr;
euf::enode* n1 = var2enode(v1), *n2 = var2enode(v2);
euf::enode* n1 = var2enode(v1);
expr* e1 = n1->get_expr();
if (!a.is_array(e1))
return true;
Expand Down
3 changes: 3 additions & 0 deletions src/sat/smt/pb_constraint.h
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,9 @@ namespace pb {
constraint(tag_t t, unsigned id, literal l, unsigned sz, size_t osz, unsigned k):
m_tag(t), m_lit(l), m_size(sz), m_obj_size(osz), m_id(id), m_k(k) {
}

virtual ~constraint() = default;

sat::ext_constraint_idx cindex() const { return sat::constraint_base::mem2base(this); }
void deallocate(small_object_allocator& a) { a.deallocate(obj_size(), sat::constraint_base::mem2base_ptr(this)); }
unsigned id() const { return m_id; }
Expand Down
1 change: 1 addition & 0 deletions src/sat/smt/pb_solver_interface.h
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@ namespace pb {

class solver_interface {
public:
virtual ~solver_interface() = default;
virtual lbool value(bool_var v) const = 0;
virtual lbool value(literal lit) const = 0;
virtual bool is_false(literal lit) const = 0;
Expand Down
1 change: 0 additions & 1 deletion src/smt/mam.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2091,7 +2091,6 @@ namespace {
enode * n = m_registers[j2->m_reg]->get_root();
if (n->get_num_parents() == 0)
return nullptr;
unsigned num_args = n->get_num_args();
enode_vector * v = mk_enode_vector();
enode_vector::const_iterator it1 = n->begin_parents();
enode_vector::const_iterator end1 = n->end_parents();
Expand Down
1 change: 1 addition & 0 deletions src/smt/smt_model_finder.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,7 @@ namespace smt {

class evaluator {
public:
virtual ~evaluator() = default;
virtual expr* eval(expr* n, bool model_completion) = 0;
};

Expand Down
1 change: 1 addition & 0 deletions src/smt/theory_opt.h
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ namespace smt {
class theory_opt {
public:
typedef inf_eps_rational<inf_rational> inf_eps;
virtual ~theory_opt() = default;
virtual inf_eps value(theory_var) = 0;
virtual inf_eps maximize(theory_var v, expr_ref& blocker, bool& has_shared) = 0;
virtual theory_var add_objective(app* term) = 0;
Expand Down
1 change: 1 addition & 0 deletions src/solver/assertions/asserted_formulas.h
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,7 @@ class asserted_formulas {
char const* m_id;
public:
simplify_fmls(asserted_formulas& af, char const* id): af(af), m(af.m), m_id(id) {}
virtual ~simplify_fmls() = default;
char const* id() const { return m_id; }
virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) = 0;
virtual bool should_apply() const { return true;}
Expand Down
1 change: 1 addition & 0 deletions src/solver/solver.h
Original file line number Diff line number Diff line change
Expand Up @@ -241,6 +241,7 @@ class solver : public check_sat_result {

class propagate_callback {
public:
virtual ~propagate_callback() = default;
virtual void propagate_cb(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr* conseq) = 0;
};
class context_obj {
Expand Down
2 changes: 2 additions & 0 deletions src/tactic/fd_solver/smtfd_solver.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -509,6 +509,8 @@ namespace smtfd {
m_context.add_plugin(this);
}

virtual ~theory_plugin() = default;

table& ast2table(ast* f, sort* s) {
unsigned idx = 0;
if (!m_ast2table.find(f, s, idx)) {
Expand Down