mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 09:26:15 +00:00
Code Activity

fixed memory leak (`mem' remained allocated upon exception thrown in check_args).

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-09-17 13:20:24 +01:00
parent 2e071e89b0
commit d2c9b69eb3
1 changed files with 61 additions and 52 deletions
Download patch file Download diff file Expand all files Collapse all files

113
src/ast/ast.cpp
View file

@ -2002,65 +2002,74 @@ bool ast_manager::coercion_needed(func_decl * decl, unsigned num_args, expr * co
} }
app * ast_manager::mk_app_core(func_decl * decl, unsigned num_args, expr * const * args) { app * ast_manager::mk_app_core(func_decl * decl, unsigned num_args, expr * const * args) {
unsigned sz = app::get_obj_size(num_args); app * r = 0;
void * mem = allocate_node(sz); app * new_node = 0;
app * new_node; unsigned sz = app::get_obj_size(num_args);
app * r; void * mem = allocate_node(sz);
if (m_int_real_coercions && coercion_needed(decl, num_args, args)) {
expr_ref_buffer new_args(*this); try {
if (decl->is_associative()) { if (m_int_real_coercions && coercion_needed(decl, num_args, args)) {
sort * d = decl->get_domain(0); expr_ref_buffer new_args(*this);
for (unsigned i = 0; i < num_args; i++) { if (decl->is_associative()) {
sort * s = get_sort(args[i]); sort * d = decl->get_domain(0);
if (d != s && d->get_family_id() == m_arith_family_id && s->get_family_id() == m_arith_family_id) { for (unsigned i = 0; i < num_args; i++) {
if (d->get_decl_kind() == REAL_SORT) sort * s = get_sort(args[i]);
new_args.push_back(mk_app(m_arith_family_id, OP_TO_REAL, args[i])); if (d != s && d->get_family_id() == m_arith_family_id && s->get_family_id() == m_arith_family_id) {
else if (d->get_decl_kind() == REAL_SORT)
new_args.push_back(mk_app(m_arith_family_id, OP_TO_INT, args[i])); new_args.push_back(mk_app(m_arith_family_id, OP_TO_REAL, args[i]));
} else
else { new_args.push_back(mk_app(m_arith_family_id, OP_TO_INT, args[i]));
new_args.push_back(args[i]); }
else {
new_args.push_back(args[i]);
}
} }
} }
else {
for (unsigned i = 0; i < num_args; i++) {
sort * d = decl->get_domain(i);
sort * s = get_sort(args[i]);
if (d != s && d->get_family_id() == m_arith_family_id && s->get_family_id() == m_arith_family_id) {
if (d->get_decl_kind() == REAL_SORT)
new_args.push_back(mk_app(m_arith_family_id, OP_TO_REAL, args[i]));
else
new_args.push_back(mk_app(m_arith_family_id, OP_TO_INT, args[i]));
}
else {
new_args.push_back(args[i]);
}
}
}
check_args(decl, num_args, new_args.c_ptr());
SASSERT(new_args.size() == num_args);
new_node = new (mem)app(decl, num_args, new_args.c_ptr());
r = register_node(new_node);
} }
else { else {
for (unsigned i = 0; i < num_args; i++) { check_args(decl, num_args, args);
sort * d = decl->get_domain(i); new_node = new (mem)app(decl, num_args, args);
sort * s = get_sort(args[i]); r = register_node(new_node);
if (d != s && d->get_family_id() == m_arith_family_id && s->get_family_id() == m_arith_family_id) { }
if (d->get_decl_kind() == REAL_SORT)
new_args.push_back(mk_app(m_arith_family_id, OP_TO_REAL, args[i])); if (m_trace_stream && r == new_node) {
else *m_trace_stream << "[mk-app] #" << r->get_id() << " ";
new_args.push_back(mk_app(m_arith_family_id, OP_TO_INT, args[i])); if (r->get_num_args() == 0 && r->get_decl()->get_name() == "int") {
} ast_ll_pp(*m_trace_stream, *this, r);
else { }
new_args.push_back(args[i]); else if (is_label_lit(r)) {
} ast_ll_pp(*m_trace_stream, *this, r);
}
else {
*m_trace_stream << r->get_decl()->get_name();
for (unsigned i = 0; i < r->get_num_args(); i++)
*m_trace_stream << " #" << r->get_arg(i)->get_id();
*m_trace_stream << "\n";
} }
} }
check_args(decl, num_args, new_args.c_ptr());
SASSERT(new_args.size() == num_args);
new_node = new (mem) app(decl, num_args, new_args.c_ptr());
r = register_node(new_node);
} }
else { catch (...) {
check_args(decl, num_args, args); deallocate_node(static_cast<ast*>(mem), sz);
new_node = new (mem) app(decl, num_args, args); throw;
r = register_node(new_node);
}
if (m_trace_stream && r == new_node) {
*m_trace_stream << "[mk-app] #" << r->get_id() << " ";
if (r->get_num_args() == 0 && r->get_decl()->get_name() == "int") {
ast_ll_pp(*m_trace_stream, *this, r);
} else if (is_label_lit(r)) {
ast_ll_pp(*m_trace_stream, *this, r);
} else {
*m_trace_stream << r->get_decl()->get_name();
for (unsigned i = 0; i < r->get_num_args(); i++)
*m_trace_stream << " #" << r->get_arg(i)->get_id();
*m_trace_stream << "\n";
}
} }
return r; return r;