Functions should be able to initialize their arguments #793
Labels
A-type-system
Area: Type system
C-enhancement
Category: An issue proposing an enhancement or a PR with one.
This came up in the course of writing comms as a library. I want to be able to write this:
recv_into
has the form it does because it calls into the runtime library, which needs a pointer to the place where the data should go. Ideally, we won't always want to initialize this, and in fact in some cases we may not be able to (for example, a tag type is exported from a module, but not its constructor).What would be nice is some time of typestate annotation that says a parameter may not be initialized (or perhaps even stronger, is not initialized), and then declare as a postcondition that its argument is initialized.
I'm not sure what ramifications this might have as far as safety and typestate analysis, but this pattern is relatively common in a lot of systems code I've seen.
The text was updated successfully, but these errors were encountered: