You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Auto merge of #872 - RalfJung:retag-shallow, r=oli-obk
Make Retag shallow
A shallow retag does not traverse into fields of compound typed to search for references to retag. It only retags "top-level"/"bare" references (and boxes).
This helps with rust-lang/unsafe-code-guidelines#125 because it also means that we do not add protectors for references passed in fields of a struct (or other compound types). Until we know what the rules should be for protectors, I prefer to be less aggressive about what we are rejecting.
This also matches our work-in-progress Coq formalization.
0 commit comments