small fixes

PLSysSec · Nov 16, 2024 · 1dca902 · 1dca902
1 parent 793c017
commit 1dca902
Show file tree

Hide file tree

Showing 7 changed files with 6 additions and 9 deletions.
diff --git a/kernel/src/collections/queue.rs b/kernel/src/collections/queue.rs
@@ -29,7 +29,6 @@ pub trait Queue<T> {
 
     /// Remove and return one (the first) element that matches the predicate.
     #[flux_rs::trusted_impl]
-    // #[flux_rs::sig(fn(self: &strg Self, _) -> Option<_> ensures self: Self)]
     fn remove_first_matching<F>(&mut self, f: F) -> Option<T>
     where
         F: Fn(&T) -> bool;

diff --git a/kernel/src/grant.rs b/kernel/src/grant.rs
@@ -1813,7 +1813,7 @@ impl<'a, T: Default, Upcalls: UpcallSize, AllowROs: AllowRoSize, AllowRWs: Allow
 {
     type Item = ProcessGrant<'a, T, Upcalls, AllowROs, AllowRWs>;
 
-    #[flux_rs::trusted] // `to_sort_list` called on bound variable list with non-refinements
+    #[flux_rs::trusted] // cannot infer substitution
     fn next(&mut self) -> Option<Self::Item> {
         let grant = self.grant;
         // Get the next `ProcessId` from the kernel processes array that is

diff --git a/kernel/src/hil/can.rs b/kernel/src/hil/can.rs
@@ -228,7 +228,6 @@ pub trait StandardBitTiming {
 /// is inspired by the Zephyr CAN driver available at
 /// `<https://github.com/zephyrproject-rtos/zephyr/tree/main/drivers/can>`
 impl<T: Configure> StandardBitTiming for T {
-    #[flux_rs::trusted] // VTOCK: error jumping to join point
     fn bit_timing_for_bitrate(clock_rate: u32, bitrate: u32) -> Result<BitTiming, ErrorCode> {
         fn calc_sample_point_err(
             sp: u32,

diff --git a/kernel/src/kernel.rs b/kernel/src/kernel.rs
@@ -187,7 +187,7 @@ impl Kernel {
     }
 
     /// Returns an iterator over all processes loaded by the kernel.
-    #[flux_rs::trusted] // Unsupported Cast: `PointerCoercion(ReifyFnPointer)`
+    #[flux_rs::trusted] // cannot infer substitution (filter map)
     pub(crate) fn get_process_iter(
         &self,
     ) -> core::iter::FilterMap<

diff --git a/kernel/src/processbuffer.rs b/kernel/src/processbuffer.rs
@@ -796,7 +796,7 @@ impl ReadableProcessSlice {
     }
 
     /// Iterate the slice in chunks.
-    #[flux_rs::trusted] // Unsupported Terminator
+    #[flux_rs::trusted] // Unexpected escaping region
     pub fn chunks(
         &self,
         chunk_size: usize,
@@ -1037,7 +1037,7 @@ impl WriteableProcessSlice {
     }
 
     /// Iterate over the slice in chunks.
-    #[flux_rs::trusted] // Unsupported Terminator
+    #[flux_rs::trusted] // Unexpected escaping region
     pub fn chunks(
         &self,
         chunk_size: usize,

diff --git a/kernel/src/scheduler/priority.rs b/kernel/src/scheduler/priority.rs
@@ -38,7 +38,7 @@ impl PrioritySched {
 }
 
 impl<C: Chip> Scheduler<C> for PrioritySched {
-    #[flux_rs::trusted] // ICE: `to_sort_list` called on bound variable list with non-refinements
+    #[flux_rs::trusted] // ICE: cannot infer subtitution (filter_map)
     fn next(&self) -> SchedulingDecision {
         // Iterates in-order through the process array, always running the
         // first process it finds that is ready to run. This enforces the

diff --git a/kernel/src/utilities/math.rs b/kernel/src/utilities/math.rs
@@ -24,8 +24,7 @@ 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)})]