Compare commits

...

1 Commits

Author SHA1 Message Date
Leonardo de Moura
97a26b2cdf fix: sharecommon
This PR fixes a bug in the `sharecommon` module, which was returning
incorrect results for objects that had already been processed by
`sharecommon`. See the new test for an example that triggered the bug.
2024-12-18 18:30:43 -08:00
2 changed files with 15 additions and 1 deletions

View File

@@ -233,7 +233,10 @@ public:
obj_res operator()(obj_arg a) {
if (push_child(a)) {
return m_state.pack(a);
object * r = m_children.back();
lean_inc(r);
lean_dec(a);
return m_state.pack(r);
}
while (!m_todo.empty()) {
b_obj_arg curr = m_todo.back();

View File

@@ -177,3 +177,14 @@ info: [[2, 3, 4]]
-/
#guard_msgs in
#eval (tst6 2).run
unsafe def tst7 (x : Nat) : ShareCommonT IO Unit := do
let o0 := mkByteArray2 x
let o1 shareCommonM o0
let o2 shareCommonM o1
let o3 shareCommonM o0
check $ ptrAddrUnsafe o1 == ptrAddrUnsafe o2
check $ ptrAddrUnsafe o1 == ptrAddrUnsafe o3
#eval (tst7 3).run