max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(runtime/object,util/object_ref): missing assertions

Browse source
This commit is contained in:
Sebastian Ullrich 2019-09-03 11:42:38 +02:00
parent 8e47b6396f
commit 4aa4a4d5f1
2 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/runtime/object.h
View file

@ -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); }

1
src/util/object_ref.h
View file

@ -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<object_ref const *>(lean_to_ctor(o)->m_objs)[i];
}