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

fix(kernel): memory corruption bugs

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-17 15:32:27 -08:00
parent 72e1678ad9
commit 53ee205dc6
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/expr.cpp
View file

@ -149,7 +149,7 @@ void expr_app::dealloc(buffer<expr_cell*> & todelete) {
// Expr binders (Lambda, Pi and Sigma)
expr_binder::expr_binder(expr_kind k, name const & n, expr const & t, expr const & b):
expr_composite(k, ::lean::hash(t.hash(), b.hash()), t.has_metavar() || b.has_metavar(),
std::max(get_depth(m_domain), get_depth(m_body)) + 1),
std::max(get_depth(t), get_depth(b)) + 1),
m_name(n),
m_domain(t),
m_body(b) {

2
src/kernel/instantiate.cpp
View file

@ -93,7 +93,7 @@ expr head_beta_reduce(expr const & t) {
expr const * it = &t;
while (true) {
lean_assert(is_app(*it));
expr f = app_fn(*it);
expr const & f = app_fn(*it);
args.push_back(app_arg(*it));
if (is_lambda(f)) {
return apply_beta(f, args.size(), args.data());