diff --git a/arch/cortex-m/src/mpu.rs b/arch/cortex-m/src/mpu.rs index 90c093ed53..819b537732 100644 --- a/arch/cortex-m/src/mpu.rs +++ b/arch/cortex-m/src/mpu.rs @@ -452,21 +452,21 @@ struct CortexMLocation { pub size: usize, } -#[flux_rs::alias(type BaseAddr[mask: bitvec<32>, value: bitvec<32>] = FieldValueU32[mask, value])] -type BaseAddr = FieldValueU32; +// #[flux_rs::alias(type BaseAddr[mask: bitvec<32>, value: bitvec<32>] = FieldValueU32[mask, value])] +// type BaseAddr = FieldValueU32; -#[flux_rs::alias(type Attrs[mask: bitvec<32>, value: bitvec<32>] = FieldValueU32[mask, value])] -type Attrs = FieldValueU32; +// #[flux_rs::alias(type Attrs[mask: bitvec<32>, value: bitvec<32>] = FieldValueU32[mask, value])] +// type Attrs = FieldValueU32; // VTOCK_TODO: maybe cleaner implementation using aliases and refine by the field values? /// Struct storing configuration for a Cortex-M MPU region. #[derive(Copy, Clone)] -#[flux_rs::refined_by(rbar: BaseAddr, rasr: Attrs)] +#[flux_rs::refined_by(rbar: FieldValueU32, rasr: FieldValueU32)] pub struct CortexMRegion { location: Option, - #[field(BaseAddr[rbar])] + #[field(FieldValueU32[rbar])] base_address: FieldValueU32, - #[field(Attrs[rasr])] + #[field(FieldValueU32[rasr])] attributes: FieldValueU32, } @@ -564,12 +564,12 @@ impl CortexMRegion { Some((loc.addr, loc.size)) } - #[flux_rs::sig(fn(&CortexMRegion[@addr, @attrs]) -> BaseAddr[addr])] + #[flux_rs::sig(fn(&CortexMRegion[@addr, @attrs]) -> FieldValueU32[addr])] fn base_address(&self) -> FieldValueU32 { self.base_address } - #[flux_rs::sig(fn(&CortexMRegion[@addr, @attrs]) -> Attrs[attrs])] + #[flux_rs::sig(fn(&CortexMRegion[@addr, @attrs]) -> FieldValueU32[attrs])] fn attributes(&self) -> FieldValueU32 { self.attributes }