mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-24 17:40:35 +00:00
Code Activity

Fix clang warnings about casting away const. (#9933)

Browse source 
This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings.

This PR adds
```
"-Wcast-qual"
```
to the set of warnings enabled in the build.  This gives warnings like:
```
/Users/daviddetlefs/z3/src/ast/ast.cpp:2897:38: warning: cast from 'app *const *' to 'expr **' drops const qualifier [-Wcast-qual]
```
I fixed these by inserting consts. In some cases, a "const_cast<T>(...)"
was necessary.
This commit is contained in:
davedets 2026-06-23 18:57:46 -07:00 • committed by GitHub
parent cd2915ff3c
commit 0adbcaf0d5
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 14 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

1
cmake/compiler_warnings.cmake
View file

@ -24,6 +24,7 @@ set(CLANG_ONLY_WARNINGS
"-Wsuggest-override"
"-Winconsistent-missing-override"
"-Wno-missing-field-initializers"
"-Wcast-qual"
)
set(MSVC_WARNINGS "/W3")

2
src/api/z3_replayer.cpp
View file

@ -621,7 +621,7 @@ struct z3_replayer::imp {
Z3_symbol get_symbol(unsigned pos) const {
check_arg(pos, SYMBOL);
return (Z3_symbol)m_args[pos].m_sym;
return (Z3_symbol)const_cast<void*>(m_args[pos].m_sym);
}
void * get_obj(unsigned pos) const {

20
src/ast/ast.cpp
View file

@ -2894,7 +2894,7 @@ proof * ast_manager::mk_transitivity(unsigned num_proofs, proof * const * proofs
}
});
ptr_buffer<expr> args;
args.append(num_proofs, (expr**) proofs);
args.append(num_proofs, (expr* const *) proofs);
args.push_back(mk_eq(n1,n2));
return mk_app(basic_family_id, PR_TRANSITIVITY_STAR, args.size(), args.data());
}
@ -2903,7 +2903,7 @@ proof * ast_manager::mk_monotonicity(func_decl * R, app * f1, app * f2, unsigned
SASSERT(f1->get_num_args() == f2->get_num_args());
SASSERT(f1->get_decl() == f2->get_decl());
ptr_buffer<expr> args;
args.append(num_proofs, (expr**) proofs);
args.append(num_proofs, (expr* const *) proofs);
args.push_back(mk_app(R, f1, f2));
proof* p = mk_app(basic_family_id, PR_MONOTONICITY, args.size(), args.data());
return p;
@ -2965,7 +2965,7 @@ proof * ast_manager::mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, pr
if (proofs_disabled())
return nullptr;
ptr_buffer<expr> args;
args.append(num_proofs, (expr**) proofs);
args.append(num_proofs, (expr* const *) proofs);
args.push_back(mk_eq(s, t));
return mk_app(basic_family_id, PR_REWRITE_STAR, args.size(), args.data());
}
@ -3055,7 +3055,7 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
}
if (!found_complement) {
args.append(num_proofs, (expr**)proofs);
args.append(num_proofs, (expr* const *)proofs);
CTRACE(mk_unit_resolution_bug, !is_or(f1), tout << mk_ll_pp(f1, *this) << "\n";
for (unsigned i = 1; i < num_proofs; ++i)
tout << mk_pp(proofs[i], *this) << "\n";
@ -3125,7 +3125,7 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
tout << mk_pp(new_fact, *this) << "\n";);
ptr_buffer<expr> args;
args.append(num_proofs, (expr**) proofs);
args.append(num_proofs, (expr* const *) proofs);
args.push_back(new_fact);
#ifdef Z3DEBUG
expr * f1 = get_fact(proofs[0]);
@ -3191,7 +3191,7 @@ proof * ast_manager::mk_apply_defs(expr * n, expr * def, unsigned num_proofs, pr
if (proofs_disabled())
return nullptr;
ptr_buffer<expr> args;
args.append(num_proofs, (expr**) proofs);
args.append(num_proofs, (expr* const *) proofs);
args.push_back(mk_oeq(n, def));
return mk_app(basic_family_id, PR_APPLY_DEF, args.size(), args.data());
}
@ -3225,7 +3225,7 @@ proof * ast_manager::mk_nnf_pos(expr * s, expr * t, unsigned num_proofs, proof *
return nullptr;
check_nnf_proof_parents(num_proofs, proofs);
ptr_buffer<expr> args;
args.append(num_proofs, (expr**) proofs);
args.append(num_proofs, (expr* const *) proofs);
args.push_back(mk_oeq(s, t));
return mk_app(basic_family_id, PR_NNF_POS, args.size(), args.data());
}
@ -3235,7 +3235,7 @@ proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof *
return nullptr;
check_nnf_proof_parents(num_proofs, proofs);
ptr_buffer<expr> args;
args.append(num_proofs, (expr**) proofs);
args.append(num_proofs, (expr* const *) proofs);
args.push_back(mk_oeq(mk_not(s), t));
return mk_app(basic_family_id, PR_NNF_NEG, args.size(), args.data());
}
@ -3305,7 +3305,7 @@ proof * ast_manager::mk_redundant_del(expr* e) {
proof * ast_manager::mk_clause_trail(unsigned n, expr* const* ps) {
ptr_buffer<expr> args;
args.append(n, (expr**) ps);
args.append(n, (expr* const *) ps);
return mk_app(basic_family_id, PR_CLAUSE_TRAIL, 0, nullptr, args.size(), args.data());
}
@ -3323,7 +3323,7 @@ proof * ast_manager::mk_th_lemma(
for (unsigned i = 0; i < num_params; ++i)
parameters.push_back(params[i]);
ptr_buffer<expr> args;
args.append(num_proofs, (expr**) proofs);
args.append(num_proofs, (expr* const *) proofs);
args.push_back(fact);
return mk_app(basic_family_id, PR_TH_LEMMA, parameters.size(), parameters.data(), args.size(), args.data());
}

4
src/ast/ast_pp_dot.cpp
View file

@ -68,8 +68,8 @@ private:
inline ast_manager & m() const { return m_manager; }
// label for an expression
std::string label_of_expr(const expr * e) const {
expr_ref er((expr*)e, m());
std::string label_of_expr(const expr *e) const {
expr_ref er(const_cast<expr *>(e), m());
std::ostringstream out;
out << er << std::flush;
return escape_dot(out.str());