From 124c5da414a019d778bf99be5f8d92cdbe18cbb4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 22 Aug 2019 20:18:59 -0700 Subject: [PATCH] fix(runtime): disable compressed headers and fix bugs --- src/runtime/lean.h | 4 ++-- src/runtime/object.cpp | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/runtime/lean.h b/src/runtime/lean.h index a41fea4f7a..e52b57fef9 100644 --- a/src/runtime/lean.h +++ b/src/runtime/lean.h @@ -16,7 +16,7 @@ Author: Leonardo de Moura #endif #define LEAN_SMALL_ALLOCATOR -#define LEAN_COMPRESSED_OBJECT_HEADER +// #define LEAN_COMPRESSED_OBJECT_HEADER #ifdef __cplusplus #include @@ -1530,7 +1530,7 @@ static inline uint64_t lean_unbox_uint64(b_lean_obj_arg o) { } static inline lean_obj_res lean_box_usize(size_t v) { - lean_obj_res r = lean_alloc_ctor(0, 1, 0); + lean_obj_res r = lean_alloc_ctor(0, 0, sizeof(size_t)); lean_ctor_set_usize(r, 0, v); return r; } diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index 60691e1f73..f66bfbe87c 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -49,7 +49,7 @@ static inline lean_object * get_next(lean_object * o) { LEAN_BYTE(header, 7) = 0; return (lean_object*)(header); #else - return (lean_object*)(o->m_rc); + return (lean_object*)((size_t)(o->m_rc)); #endif } @@ -60,7 +60,7 @@ static inline void set_next(lean_object * o, lean_object * n) { LEAN_BYTE(new_header, 7) = LEAN_BYTE(o->m_header, 7); o->m_header = new_header; #else - *(lean_object*)(o->m_rc) = n; + o->m_rc = (size_t)n; #endif }