ring_buffer

PLSysSec · Oct 2, 2024 · 6841867 · 6841867
1 parent 7793ebb
commit 6841867
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/kernel/src/collections/ring_buffer.rs b/kernel/src/collections/ring_buffer.rs
@@ -38,7 +38,7 @@ impl<'a, T: Copy> RingBuffer<'a, T> {
         }
     }
 
-    #[flux_rs::sig(fn(&RingBuffer<T>[@ring_len, @hd, @tl]) -> usize[ring_len]) ]
+    #[flux_rs::sig(fn(&RingBuffer<T>[@rb]) -> usize[rb.ring_len]) ]
     fn ring_len(&self) -> usize {
         self.ring.len()
     }