Skip to content

Commit a34ac3c

Browse files
committed
correct what we say about Miri
1 parent 5007333 commit a34ac3c

File tree

1 file changed

+4
-1
lines changed

1 file changed

+4
-1
lines changed

wip/stacked-borrows.md

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -161,7 +161,7 @@ In other words, the per-stack-frame `CallId` is initialized by `Tracking::new_ca
161161
We say that a `CallId` is *active* if the call stack contains a stack frame with that ID.
162162
In the following, we pretend there exists a function `call_is_active(id)` that can check this.
163163

164-
**Note**: Miri uses a slightly more complex system with a `HashSet<CallId>` tracking the set of active `CallId`; that is just an optimization to avoid having to scan the call stack all the time.
164+
**Note**: Miri uses a slightly more complex system to track the set of active `CallId`; that is just an optimization to avoid having to scan the call stack all the time.
165165

166166
### Preliminaries for items
167167

@@ -334,6 +334,9 @@ For those we perform the following steps:
334334

335335
We do not recurse into fields of structs or other compound types, only "bare" references/... get retagged.
336336

337+
**Note**: Miri offers a flag, `-Zmiri-retag-fields`, that changes this behavior to also recurse into compound types to search for references to retag.
338+
We never recurse through a pointer indirection.
339+
337340
### Deallocating memory
338341

339342
Memory deallocation first acts like a write access through the pointer used for deallocation.

0 commit comments

Comments
 (0)