From 79f4eeea62c62526f117ea24780d251596f3ccba Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 22 Aug 2019 20:31:47 -0700 Subject: [PATCH] fix(runtime/lean): incorrect assertion --- src/runtime/compact.cpp | 2 +- src/runtime/lean.h | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/runtime/compact.cpp b/src/runtime/compact.cpp index afbe948ac9..2a2a0ba545 100644 --- a/src/runtime/compact.cpp +++ b/src/runtime/compact.cpp @@ -123,7 +123,7 @@ bool object_compactor::insert_array(object * o) { new_o->m_size = sz; new_o->m_capacity = sz; for (size_t i = 0; i < sz; i++) { - array_set((lean_object*)new_o, i, offsets[i]); + lean_array_set_core((lean_object*)new_o, i, offsets[i]); } save(o, (lean_object*)new_o); return true; diff --git a/src/runtime/lean.h b/src/runtime/lean.h index e52b57fef9..4c05c59357 100644 --- a/src/runtime/lean.h +++ b/src/runtime/lean.h @@ -702,7 +702,9 @@ static inline b_lean_obj_res lean_array_get_core(b_lean_obj_arg o, size_t i) { return lean_to_array(o)->m_data[i]; } static inline void lean_array_set_core(u_lean_obj_arg o, size_t i, lean_obj_arg v) { - assert(lean_is_exclusive(o)); + /* Remark: we use this procedure to update non shared arrays in the heap, + and when copying objects to compact region at compact.cpp */ + assert(!lean_is_heap_object(o) || lean_is_exclusive(o)); assert(i < lean_array_size(o)); lean_to_array(o)->m_data[i] = v; }