reorder short-circuiting comparison to make proof go through

PLSysSec · Jul 22, 2024 · 96f9f0c · 96f9f0c
1 parent f702f0d
commit 96f9f0c
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/arch/rv32i/src/pmp.rs b/arch/rv32i/src/pmp.rs
@@ -132,8 +132,8 @@ impl NAPOTRegionSpec {
     /// [`NAPOTRegionSpec`]'s documentation are satisfied, otherwise `None`.
     // #[flux::ignore]
     pub fn new(start: *const u8, size: usize) -> Option<Self> {
-        assume(size > 0); // I thought the struct has already refined this property?
-        if !size.is_power_of_two() || (start as usize) % size != 0 || size < 8 {
+        //assume(size > 0); // I thought the struct has already refined this property?
+        if size < 8 || !size.is_power_of_two() || (start as usize) % size != 0  {
             None
         } else {
             Some(NAPOTRegionSpec { start, size })