fmt

arch/cortex-m/src/lib.rs

@@ -7,6 +7,7 @@
 #![crate_name = "cortexm"]
 #![crate_type = "rlib"]
 #![no_std]
+#![feature(proc_macro_hygiene)]
 
 use core::fmt::Write;
 

capsules/system/Cargo.toml

@@ -11,6 +11,7 @@ edition.workspace = true
 [dependencies]
 kernel = { path = "../../kernel" }
 tock-tbf = { path = "../../libraries/tock-tbf" }
+flux-rs = { git = "https://github.com/flux-rs/flux" }
 
 [lints]
 workspace = true

flux_support/src/extern_specs/non_null.rs

@@ -1,3 +1,3 @@
 #[flux_rs::extern_spec(core::ptr)]
 #[refined_by(n: int)]
-struct NonNull<T>;
+struct NonNull<T>;

flux_support/src/extern_specs/num.rs

@@ -1,31 +1,31 @@
 // The spec we need to prove log_base_two
 #[flux_rs::extern_spec]
 impl u32 {
-    #[sig(fn(num: u32) -> u32{r: (num == 0 => r == 32) && 
-                                 (num > 0 => r <= 31) && 
-                                 (num > 1 => r <= 30) 
+    #[sig(fn(num: u32) -> u32{r: (num == 0 => r == 32) &&
+                                 (num > 0 => r <= 31) &&
+                                 (num > 1 => r <= 30)
                             })]
     fn leading_zeros(self) -> u32;
-    
+
     #[sig(fn(num: u32) -> u32{r: (num == 0 => r == 32) && (num != 0 =>r <= 31) })]
     fn trailing_zeros(self) -> u32;
 }
 
 #[flux_rs::extern_spec]
 impl u64 {
-    #[sig(fn(num: u64) -> u32{r: (num == 0 => r == 64) && 
-                                 (num > 0 => r <= 63) && 
-                                 (num > 1 => r <= 62) 
+    #[sig(fn(num: u64) -> u32{r: (num == 0 => r == 64) &&
+                                 (num > 0 => r <= 63) &&
+                                 (num > 1 => r <= 62)
                             })]
     fn leading_zeros(self) -> u32;
 }
 
 // Only works when usize is 32-bits
 #[flux_rs::extern_spec]
 impl usize {
-    #[sig(fn(num: usize{num < 4294967295}) -> u32{r: (num == 0 => r == 32) && 
-                                 (num > 0 => r <= 31) && 
-                                 (num > 1 => r <= 30) 
+    #[sig(fn(num: usize{num < 4294967295}) -> u32{r: (num == 0 => r == 32) &&
+                                 (num > 0 => r <= 31) &&
+                                 (num > 1 => r <= 30)
                             })]
     fn leading_zeros(self) -> u32;
-}
+}

kernel/src/collections/ring_buffer.rs

@@ -6,8 +6,6 @@
 
 use crate::collections::queue;
 
-
-
 #[flux_rs::refined_by(ring_len: int, head: int, tail: int)]
 #[flux_rs::invariant(ring_len > 1)]
 pub struct RingBuffer<'a, T: 'a> {
@@ -27,7 +25,6 @@ flux_rs::defs! {
     fn next_tl(rb: RingBuffer) -> int { rb_next(rb.tail, rb.ring_len) }
 }
 
-
 impl<'a, T: Copy> RingBuffer<'a, T> {
     #[flux_rs::sig(fn({&mut [T][@ring_len] | ring_len > 1}) -> RingBuffer<T>[ring_len, 0, 0])]
     pub fn new(ring: &'a mut [T]) -> RingBuffer<'a, T> {
@@ -102,12 +99,12 @@ impl<T: Copy> queue::Queue<T> for RingBuffer<'_, T> {
     }
 
     #[flux_rs::sig(
-        fn(self: &strg RingBuffer<T>[@ring_len, @hd, @tl], _) -> bool 
-            ensures self: RingBuffer<T>{ rg: 
+        fn(self: &strg RingBuffer<T>[@ring_len, @hd, @tl], _) -> bool
+            ensures self: RingBuffer<T>{ rg:
                 // if this is the case then we've overlapped and will overwrite a space
                 // that hasn't been read
-                rg.head != rg.tail 
-                && 
+                rg.head != rg.tail
+                &&
                 // either we're full and don't update
                 // hd == rb_next(tl, ring_len) -> rg.tail == tl && rg.head == hd
                 (hd == rb_next(tl, ring_len) => rg.tail == tl && rg.head == hd)
@@ -129,13 +126,13 @@ impl<T: Copy> queue::Queue<T> for RingBuffer<'_, T> {
     }
 
     #[flux_rs::sig(
-        fn(self: &strg RingBuffer<T>[@old], _) -> Option<T> 
-            ensures self: RingBuffer<T>{ rg: 
+        fn(self: &strg RingBuffer<T>[@old], _) -> Option<T>
+            ensures self: RingBuffer<T>{ rg:
                 // if this is the case then we've overlapped and will overwrite a space
                 // that hasn't been read
                 rg.head != rg.tail
-                && 
-                // either the buffer is full so we dequeue and then enqueue 
+                &&
+                // either the buffer is full so we dequeue and then enqueue
                 (full(old) => (rg.head == next_hd(old) && rg.tail == next_tl(old)))
                 &&
                 // or we have space so we just enqueue
@@ -157,9 +154,9 @@ impl<T: Copy> queue::Queue<T> for RingBuffer<'_, T> {
     }
 
     #[flux_rs::sig(
-        fn(self: &strg RingBuffer<T>[@ring_len, @hd, @tl]) -> Option<T> 
+        fn(self: &strg RingBuffer<T>[@ring_len, @hd, @tl]) -> Option<T>
             ensures self: RingBuffer<T>{
-                rg: 
+                rg:
                 (hd == tl => (rg.head == hd && rg.tail == tl && rg.head == rg.tail))
                 &&
                 (hd != tl => rg.head == rb_next(hd, ring_len))
@@ -183,7 +180,7 @@ impl<T: Copy> queue::Queue<T> for RingBuffer<'_, T> {
     ///
     /// If an element was removed, this function returns it as `Some(elem)`.
     #[flux_rs::sig(
-        fn(self: &strg RingBuffer<T>[@ring_len, @hd, @tl], _) -> Option<T> 
+        fn(self: &strg RingBuffer<T>[@ring_len, @hd, @tl], _) -> Option<T>
             ensures self: RingBuffer<T>{rg: rg.tail < rg.ring_len}
     )]
     // NOTE: May want to strengthen this to talk about correctness
@@ -214,7 +211,7 @@ impl<T: Copy> queue::Queue<T> for RingBuffer<'_, T> {
     }
 
     #[flux_rs::sig(
-        fn(self: &strg RingBuffer<T>[@ring_len, @hd, @tl]) 
+        fn(self: &strg RingBuffer<T>[@ring_len, @hd, @tl])
             ensures self: RingBuffer<T>[ring_len, 0, 0]
     )]
     fn empty(&mut self) {
@@ -223,7 +220,7 @@ impl<T: Copy> queue::Queue<T> for RingBuffer<'_, T> {
     }
 
     #[flux_rs::sig(
-        fn(self: &strg RingBuffer<T>[@ring_len, @hd, @tl], _) 
+        fn(self: &strg RingBuffer<T>[@ring_len, @hd, @tl], _)
             ensures self: RingBuffer<T>{rg: rg.tail < rg.ring_len}
     )]
     fn retain<F>(&mut self, mut f: F)

kernel/src/hil/can.rs

@@ -320,7 +320,6 @@ impl<T: Configure> StandardBitTiming for T {
             }
             ts = clock_rate / (prescaler * bitrate);
 
-
             sample_point_err = calc_sample_point_err(
                 sp,
                 ts,

kernel/src/process_binary.rs

@@ -144,7 +144,6 @@ impl ProcessBinary {
         tbf_version: u16,
         require_kernel_version: bool,
     ) -> Result<Self, ProcessBinaryError> {
-
         // Get a slice for just the app header.
         let header_flash = app_flash
             .get(0..header_length)

kernel/src/utilities/binary_write.rs

@@ -8,7 +8,6 @@
 //! binary slice. This mirrors the `core::fmt::Write` interface but doesn't
 //! expect a `&str`.
 
-
 /// Interface for writing an arbitrary buffer.
 pub trait BinaryWrite {
     /// Write the `buffer` to some underlying print mechanism.

kernel/src/utilities/math.rs

@@ -24,7 +24,8 @@ pub fn closest_power_of_two(mut num: u32) -> u32 {
     num
 }
 
-#[flux_rs::trusted] // bitwise arithmetic
+#[flux_rs::trusted]
+// bitwise arithmetic
 // 2147483648 is half of u32::MAX. Anything higher than that deviates from closest_power_of_two
 // I added this function to avoid unnecessary downcasts, which can be dangerous.
 #[flux_rs::sig(fn(num: usize) -> usize{r: (num < 2147483648 => r > num)})]

libraries/tock-register-interface/src/registers.rs

@@ -110,7 +110,6 @@ impl<T: UIntLike, R: RegisterLongName> Readable for ReadOnly<T, R> {
 // be removed. We `allow(dead_code)` here to suppress this warning.
 #[allow(dead_code)]
 #[repr(transparent)]
-#[allow(dead_code)]
 pub struct WriteOnly<T: UIntLike, R: RegisterLongName = ()> {
     value: UnsafeCell<T>,
     associated_register: PhantomData<R>,