michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(kernel/expr): memory leak introduced today

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-16 15:47:30 -07:00
parent 7d76278506
commit e6c52d17a6
2 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/kernel/expr.cpp
View file

@ -117,6 +117,10 @@ void expr_mlocal::dealloc(buffer<expr_cell*> & todelete) {
expr_local::expr_local(name const & n, name const & pp_name, expr const & t):
expr_mlocal(false, n, t),
m_pp_name(pp_name) {}
void expr_local::dealloc(buffer<expr_cell*> & todelete) {
dec_ref(m_type, todelete);
delete(this);
}
// Composite expressions
expr_composite::expr_composite(expr_kind k, unsigned h, bool has_mv, bool has_local, bool has_param_univ, unsigned d, unsigned fv_range):

3
src/kernel/expr.h
View file

@ -188,6 +188,7 @@ public:
/** \brief Metavariables and local constants */
class expr_mlocal : public expr_cell {
protected:
name m_name;
expr m_type;
friend expr_cell;
@ -204,6 +205,8 @@ class expr_local : public expr_mlocal {
// it is only used for pretty printing. This field is ignored
// when comparing expressions.
name m_pp_name;
friend expr_cell;
void dealloc(buffer<expr_cell*> & todelete);
public:
expr_local(name const & n, name const & pp_name, expr const & t);
name const & get_pp_name() const { return m_pp_name; }