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
[ownership] When lowering store_borrow, RAUW its result with its input dest.
A store_borrow is a manner to temporarily "borrow" a guaranteed value into
memory for purposes like reabstraction. To make this safer in OSSA, we treat a
store_borrow's result as an interior pointer into the stored guaranteed value,
causing all uses of that result to be validated as being within the lifetime of
the guaranteed value.
NOTE: This is not the complete store_borrow verification story. We also will
verify that the memory that is being store_borrowed into is not written to while
the store_borrow's result is live.
0 commit comments