diff --git a/src/runtime/object.h b/src/runtime/object.h index d4dc786380..98b5076de2 100644 --- a/src/runtime/object.h +++ b/src/runtime/object.h @@ -79,7 +79,7 @@ inline unsigned cnstr_num_objs(object * o) { return lean_ctor_num_objs(o); } inline object ** cnstr_obj_cptr(object * o) { return lean_ctor_obj_cptr(o); } inline uint8 * cnstr_scalar_cptr(object * o) { return lean_ctor_scalar_cptr(o); } inline obj_res alloc_cnstr(unsigned tag, unsigned num_objs, unsigned scalar_sz) { return lean_alloc_ctor(tag, num_objs, scalar_sz); } -inline unsigned cnstr_tag(b_obj_arg o) { return lean_ptr_tag(o); } +inline unsigned cnstr_tag(b_obj_arg o) { lean_assert(is_cnstr(o)); return lean_ptr_tag(o); } inline void cnstr_set_tag(b_obj_arg o, unsigned tag) { lean_ctor_set_tag(o, tag); } inline b_obj_res cnstr_get(b_obj_arg o, unsigned i) { return lean_ctor_get(o, i); } inline void cnstr_set(u_obj_arg o, unsigned i, obj_arg v) { lean_ctor_set(o, i, v); } diff --git a/src/util/object_ref.h b/src/util/object_ref.h index 684a2be948..7016690159 100644 --- a/src/util/object_ref.h +++ b/src/util/object_ref.h @@ -129,6 +129,7 @@ inline object_ref mk_cnstr(unsigned tag, object_ref const & o1, object_ref const inline object_ref const & cnstr_get_ref(object * o, unsigned i) { static_assert(sizeof(object_ref) == sizeof(object *), "unexpected object_ref size"); // NOLINT lean_assert(is_cnstr(o)); + lean_assert(i < lean_ctor_num_objs(o)); return reinterpret_cast(lean_to_ctor(o)->m_objs)[i]; }