Open
Description
I was trying to implement an abstraction over open_memstream
, and I realized it is less trivial than I initially thought. In fact, the stream opened by the OS is able to change the values of the pointed arguments ptr
and sizeloc
when fflush
and fclose
are called.
I think that the implementation of open_memstream
(and eventually open_wmemstream
) inside Miri would help a lot to check the invariances and the soundness of a safe abstraction, which requires carefully written pinned structures (because it's UB to move the structure containing the ptr
and size
passed to the function as pointers) and some attention to avoid breaking aliasing rules (it should be UB to call fflush
or fflush
if you have any reference to ptr
or size
).