| 37 | #[rr::invariant("ml.(conf_start) `aligned_to` (page_size_in_bytes_nat Size4KiB)")] |
| 38 | #[rr::invariant("ml.(conf_end) `aligned_to` (page_size_in_bytes_nat Size4KiB)")] |
| 39 | pub struct MemoryLayout { |
| 40 | #[rr::field("ml.(non_conf_start)")] |
| 41 | non_confidential_memory_start: *mut usize, |
| 42 | #[rr::field("ml.(non_conf_end)")] |
| 43 | non_confidential_memory_end: *const usize, |
| 44 | #[rr::field("ml.(conf_start)")] |
| 45 | confidential_memory_start: *mut usize, |
| 46 | #[rr::field("ml.(conf_end)")] |
| 47 | confidential_memory_end: *const usize, |
| 48 | } |
| 49 | |
| 50 | /// Send+Sync are not automatically declared on the `MemoryLayout` type because it stores internally raw pointers that |
| 51 | /// are not safe to pass in a multi-threaded program. Declaring Send+Sync is safe because because we never expose raw |
nothing calls this directly
no outgoing calls
no test coverage detected