mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-27 06:13:35 +00:00
Code Activity

Merge pull request #8898 from Z3Prover/copilot/address-actionable-issues-discussion

Browse source 
Fix actionable null pointer dereferences and uninitialized variables from static analysis
This commit is contained in:
Nikolaj Bjorner 2026-03-09 10:45:47 -07:00 • committed by GitHub
commit 4b377ae713
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
6 changed files with 27 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/euf/euf_mam.cpp
View file

@ -1402,6 +1402,7 @@ namespace euf {
// to check it again.
get_check_mark(reg) == NOT_CHECKED &&
is_ground(m_registers[reg]) &&
instr->m_enode != nullptr &&
get_pat_lbl_hash(reg) == instr->m_enode->get_lbl_hash();
}

24
src/ast/sls/sls_euf_plugin.cpp
View file

@ -289,25 +289,33 @@ namespace sls {
b = g.find(to_app(e)->get_arg(1));
}
if (lit.sign() && m.is_eq(e)) {
if (a->get_root() == b->get_root()) {
if (a && b && a->get_root() == b->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not disequal " << lit << " " << mk_pp(e, m) << "\n");
ctx.display(verbose_stream());
UNREACHABLE();
}
}
else if (!lit.sign() && m.is_eq(e)) {
if (a->get_root() != b->get_root()) {
if (a && b && a->get_root() != b->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not equal " << lit << " " << mk_pp(e, m) << "\n");
//UNREACHABLE();
}
}
else if (to_app(e)->get_family_id() != basic_family_id && lit.sign() && g.find(e)->get_root() != g.find(m.mk_false())->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not alse " << lit << " " << mk_pp(e, m) << "\n");
//UNREACHABLE();
else if (to_app(e)->get_family_id() != basic_family_id && lit.sign()) {
auto* ne = g.find(e);
auto* nf = g.find(m.mk_false());
if (ne && nf && ne->get_root() != nf->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not false " << lit << " " << mk_pp(e, m) << "\n");
//UNREACHABLE();
}
}
else if (to_app(e)->get_family_id() != basic_family_id && !lit.sign() && g.find(e)->get_root() != g.find(m.mk_true())->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not true " << lit << " " << mk_pp(e, m) << "\n");
//UNREACHABLE();
else if (to_app(e)->get_family_id() != basic_family_id && !lit.sign()) {
auto* ne = g.find(e);
auto* nt = g.find(m.mk_true());
if (ne && nt && ne->get_root() != nt->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not true " << lit << " " << mk_pp(e, m) << "\n");
//UNREACHABLE();
}
}
}

6
src/math/realclosure/realclosure.cpp
View file

@ -3458,6 +3458,8 @@ namespace realclosure {
if (sc) sc = sc->prev();
i--;
}
if (!sc)
return 0;
return ext->sdt()->qs()[sc->qidx()].size();
}
@ -3474,6 +3476,8 @@ namespace realclosure {
if (sc) sc = sc->prev();
i--;
}
if (!sc)
return 0;
const polynomial & q = ext->sdt()->qs()[sc->qidx()];
return q.size();
}
@ -3491,6 +3495,8 @@ namespace realclosure {
if (sc) sc = sc->prev();
i--;
}
if (!sc)
return numeral();
const polynomial & q = ext->sdt()->qs()[sc->qidx()];
if (j >= q.size())
return numeral();

1
src/muz/rel/udoc_relation.cpp
View file

@ -54,6 +54,7 @@ namespace datalog {
col = column_idx(orig[i]);
limit = col + column_num_bits(orig[i]);
} else {
SASSERT(other);
unsigned idx = orig[i] - get_num_cols();
col = get_num_bits() + other->column_idx(idx);
limit = col + other->column_num_bits(idx);

4
src/muz/spacer/spacer_context.cpp
View file

@ -3330,7 +3330,7 @@ bool context::is_reachable(pob &n)
model_ref mdl;
// used in case n is reachable
bool is_concrete;
bool is_concrete = false;
const datalog::rule * r = nullptr;
// denotes which predecessor's (along r) reach facts are used
bool_vector reach_pred_used;
@ -3521,7 +3521,7 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
model_ref model;
// used in case n is reachable
bool is_concrete;
bool is_concrete = false;
const datalog::rule * r = nullptr;
// denotes which predecessor's (along r) reach facts are used
bool_vector reach_pred_used;

1
src/smt/mam.cpp
View file

@ -1360,6 +1360,7 @@ namespace {
// to check it again.
get_check_mark(reg) == NOT_CHECKED &&
is_ground(m_registers[reg]) &&
instr->m_enode != nullptr &&
get_pat_lbl_hash(reg) == instr->m_enode->get_lbl_hash();
}