From 2e5702d31eacee493af6de49239e58239fc77d08 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 May 2017 10:02:10 -0700 Subject: [PATCH] fix(library/parray): it is unsafe to return reference A reroot operation performed by another thread may invalidate the reference. --- src/library/parray.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/library/parray.h b/src/library/parray.h index 72e1152a99..764251a60e 100644 --- a/src/library/parray.h +++ b/src/library/parray.h @@ -246,7 +246,7 @@ class parray { dec_ref(last); } - static T const & read_aux(cell * c, size_t i) { + static T read_aux(cell * c, size_t i) { if (c->kind() != Root) reroot(c); lean_assert(c->kind() == Root); @@ -254,7 +254,7 @@ class parray { return c->m_values[i]; } - static T const & read(cell * c, size_t i) { + static T read(cell * c, size_t i) { if (get_rc(c) == 1 && c->kind() == Root) { lean_assert(i < c->size()); return c->m_values[i]; @@ -454,7 +454,7 @@ public: return size(m_cell); } - T const & operator[](size_t i) const { + T operator[](size_t i) const { return read(m_cell, i); }