remove errors

kernel/src/collections/mod.rs

@@ -7,5 +7,5 @@
 pub mod list;
 //#[flux::ignore]
 pub mod queue;
-#[flux::ignore]
+// #[flux::ignore]
 pub mod ring_buffer;

kernel/src/collections/ring_buffer.rs

@@ -34,6 +34,7 @@ impl<'a, T: Copy> RingBuffer<'a, T> {
     }
 
     /// Returns the number of elements that can be enqueued until the ring buffer is full.
+    #[flux::ignore]
     pub fn available_len(&self) -> usize {
         // The maximum capacity of the queue is ring_len - 1, because head == tail for the empty
         // queue.
@@ -68,6 +69,7 @@ impl<'a, T: Copy> RingBuffer<'a, T> {
     }
 }
 
+#[flux::ignore]
 impl<T: Copy> queue::Queue<T> for RingBuffer<'_, T> {
     fn has_elements(&self) -> bool {
         self.head != self.tail

kernel/src/debug.rs

@@ -395,6 +395,8 @@ macro_rules! debug_flush_queue {
 
 /// Wrapper type that we need a mutable reference to for the core::fmt::Write
 /// interface.
+#[flux::trusted]
+#[flux::opaque]
 pub struct DebugWriterWrapper {
     dw: MapCell<&'static DebugWriter>,
 }

kernel/src/ipc.rs

@@ -23,7 +23,7 @@ pub const DRIVER_NUM: usize = 0x10000;
 mod ro_allow {
     pub(super) const SEARCH: usize = 0;
     /// The number of allow buffers the kernel stores for this grant.
-    pub(super) const COUNT: u8 = 1;
+    pub(super) const _COUNT: u8 = 1;
 }
 
 /// Enum to mark which type of upcall is scheduled for the IPC mechanism.