refine mpu::Permissions

PLSysSec · Oct 10, 2024 · fab81ad · fab81ad
1 parent 692fcb1
commit fab81ad
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/kernel/src/platform/mpu.rs b/kernel/src/platform/mpu.rs
@@ -11,11 +11,17 @@ use flux_support::*;
 
 /// User mode access permissions.
 #[derive(Copy, Clone, Debug)]
+#[flux_rs::refined_by(r: bool, w: bool, x: bool)]
 pub enum Permissions {
+    #[flux::variant(Permissions[true, true, true])]
     ReadWriteExecute,
+    #[flux::variant(Permissions[true, true, false])]
     ReadWriteOnly,
+    #[flux::variant(Permissions[true, false, true])]
     ReadExecuteOnly,
+    #[flux::variant(Permissions[true, false, false])]
     ReadOnly,
+    #[flux::variant(Permissions[false, false, true])]
     ExecuteOnly,
 }