3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00

Fix memory leaks

Signed-off-by: Alex Horn <t-alexh@microsoft.com>
This commit is contained in:
Alex Horn 2015-06-11 08:59:57 +01:00
parent bd57994f78
commit 565c0f785f
4 changed files with 11 additions and 1 deletions

View file

@ -518,6 +518,7 @@ namespace datalog {
relation_manager & manager = t.get_manager();
table_join_fn * join_fn = manager.mk_join_fn(t, t, m_group_by_cols, m_group_by_cols);
table_base * join_table = (*join_fn)(t, t);
dealloc(join_fn);
table_base::iterator join_table_it = join_table->begin();
table_base::iterator join_table_end = join_table->end();
@ -545,6 +546,8 @@ namespace datalog {
table_transformer_fn * project_fn = manager.mk_project_fn(*join_table, cols);
table_base * gt_table = (*project_fn)(*join_table);
dealloc(project_fn);
join_table->deallocate();
for (unsigned k = 0; k < cols.size(); ++k) {
cols[k] = k;
@ -555,6 +558,7 @@ namespace datalog {
table_base * result = t.clone();
table_intersection_filter_fn * diff_fn = manager.mk_filter_by_negation_fn(*result, *gt_table, cols, cols);
(*diff_fn)(*result, *gt_table);
dealloc(diff_fn);
gt_table->deallocate();
return result;
}

View file

@ -916,6 +916,7 @@ namespace datalog {
const relation_signature & r_sig = s.get_signature();
table_min_fn * fn = r_manager.mk_min_fn(source_t, m_group_by_cols, m_min_col);
table_base * target_t = (*fn)(source_t);
dealloc(fn);
TRACE("dl",
tout << "% ";

View file

@ -354,7 +354,9 @@ namespace datalog {
return product_relation_plugin::get_plugin(*this).mk_empty(s);
}
/**
The newly created object takes ownership of the \c table object.
*/
relation_base * relation_manager::mk_table_relation(const relation_signature & s, table_base * table) {
SASSERT(s.size()==table->get_signature().size());
return get_table_relation_plugin(table->get_plugin()).mk_from_table(s, table);

View file

@ -63,6 +63,9 @@ namespace datalog {
return alloc(table_relation, *this, s, t);
}
/**
The newly created object takes ownership of the \c t object.
*/
relation_base * table_relation_plugin::mk_from_table(const relation_signature & s, table_base * t) {
if (&t->get_plugin() == &m_table_plugin)
return alloc(table_relation, *this, s, t);