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
[LangRef] Relax semantics of writeonly / memory(write)
Instead of making writes immediate undefined behavior, consider
these attributes in terms of their externally observable effects.
We don't care if a location is read within the function, as long
as it has no impact on observed behavior. In particular, allow:
* Reading a location after writing it.
* Reading a location before writing it (within the function)
returns a poison value.
The latter could be further relaxed to also allow things like
"reading the value and then writing it back", but I'm not sure
how one would specify that operationally (so that proof checkers
can verify it).
Fixes#95152.
0 commit comments