Do not type aliases as sorts

PLSysSec · Nov 9, 2024 · 1330853 · 1330853
1 parent bf2b7e8
commit 1330853
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 3 deletions.
diff --git a/flux_support/src/flux_ptr.rs b/flux_support/src/flux_ptr.rs
@@ -159,9 +159,8 @@ impl PartialOrd for FluxPtr {
     }
 }
 
-#[flux_rs::alias(type FluxPtrU8[n: int] = FluxPtr[n])]
 pub type FluxPtrU8 = FluxPtr;
-#[flux_rs::alias(type FluxPtrU8Mut[n: int] = FluxPtr[n])]
+
 pub type FluxPtrU8Mut = FluxPtr;
 
 pub trait FluxPtrExt {

diff --git a/kernel/src/process_standard.rs b/kernel/src/process_standard.rs
@@ -123,7 +123,7 @@ struct ProcessBreaks {
 }
 
 /// A type for userspace processes in Tock.
-#[flux_rs::refined_by(mem_start: FluxPtrU8Mut, mem_len: int)]
+#[flux_rs::refined_by(mem_start: FluxPtr, mem_len: int)]
 #[flux_rs::invariant(mem_start + mem_len <= usize::MAX)] // mem doesn't overflow address space
 pub struct ProcessStandard<'a, C: 'static + Chip> {
     /// Identifier of this process and the index of the process in the process