Module vm_space_specs 

Structs

VmIoPermission

This struct is used for reading/writing memories represented by the VmReader or VmWriter. We also require a valid vmspace_owner must be present in this struct to ensure that the reader/writer is not created out of thin air.

VmSpaceOwner

A tracked struct for reasoning about verification-only properties of a VmSpace.