Merge pull request #4 from PLSysSec/trait

Update attributes for trait-impl checks

kernel/src/collections/queue.rs

@@ -16,23 +16,29 @@ pub trait Queue<T> {
 
     /// If the queue isn't full, add a new element to the back of the queue.
     /// Returns whether the element was added.
+    #[flux_rs::trusted_impl]
     fn enqueue(&mut self, val: T) -> bool;
 
     /// Add a new element to the back of the queue, poping one from the front if necessary.
+    #[flux_rs::trusted_impl]
     fn push(&mut self, val: T) -> Option<T>;
 
     /// Remove the element from the front of the queue.
+    #[flux_rs::trusted_impl]
     fn dequeue(&mut self) -> Option<T>;
 
     /// Remove and return one (the first) element that matches the predicate.
+    #[flux_rs::trusted_impl]
     fn remove_first_matching<F>(&mut self, f: F) -> Option<T>
     where
         F: Fn(&T) -> bool;
 
     /// Remove all elements from the ring buffer.
+    #[flux_rs::trusted_impl]
     fn empty(&mut self);
 
     /// Retains only the elements that satisfy the predicate.
+    #[flux_rs::trusted_impl]
     fn retain<F>(&mut self, f: F)
     where
         F: FnMut(&T) -> bool;

kernel/src/hil/time.rs

@@ -134,6 +134,7 @@ pub trait Ticks: Clone + Copy + From<u32> + fmt::Debug + Ord + PartialOrd + Eq {
 
     /// Scales the ticks by the specified numerator and denominator. If the resulting value would
     /// be greater than u32,`u32::MAX` is returned instead
+    #[flux_rs::sig(fn(Self, u32, u32{denom: denom > 0}) -> u32)]
     fn saturating_scale(self, numerator: u32, denominator: u32) -> u32;
 }
 
@@ -402,6 +403,7 @@ pub trait Timer<'a>: Time {
 #[derive(Debug)]
 pub enum Freq100MHz {}
 impl Frequency for Freq100MHz {
+    #[flux_rs::sig(fn() -> u32{r: r > 0})]
     fn frequency() -> u32 {
         100_000_000
     }
@@ -411,6 +413,7 @@ impl Frequency for Freq100MHz {
 #[derive(Debug)]
 pub enum Freq16MHz {}
 impl Frequency for Freq16MHz {
+    #[flux_rs::sig(fn() -> u32{r: r > 0})]
     fn frequency() -> u32 {
         16_000_000
     }
@@ -419,6 +422,7 @@ impl Frequency for Freq16MHz {
 /// 10MHz `Frequency`
 pub enum Freq10MHz {}
 impl Frequency for Freq10MHz {
+    #[flux_rs::sig(fn() -> u32{r: r > 0})]
     fn frequency() -> u32 {
         10_000_000
     }
@@ -428,6 +432,7 @@ impl Frequency for Freq10MHz {
 #[derive(Debug)]
 pub enum Freq1MHz {}
 impl Frequency for Freq1MHz {
+    #[flux_rs::sig(fn() -> u32{r: r > 0})]
     fn frequency() -> u32 {
         1_000_000
     }
@@ -437,6 +442,7 @@ impl Frequency for Freq1MHz {
 #[derive(Debug)]
 pub enum Freq32KHz {}
 impl Frequency for Freq32KHz {
+    #[flux_rs::sig(fn() -> u32{r: r > 0})]
     fn frequency() -> u32 {
         32_768
     }
@@ -446,6 +452,7 @@ impl Frequency for Freq32KHz {
 #[derive(Debug)]
 pub enum Freq16KHz {}
 impl Frequency for Freq16KHz {
+    #[flux_rs::sig(fn() -> u32{r: r > 0})]
     fn frequency() -> u32 {
         16_000
     }
@@ -455,6 +462,7 @@ impl Frequency for Freq16KHz {
 #[derive(Debug)]
 pub enum Freq1KHz {}
 impl Frequency for Freq1KHz {
+    #[flux_rs::sig(fn() -> u32{r: r > 0})]
     fn frequency() -> u32 {
         1_000
     }

kernel/src/processbuffer.rs

@@ -868,7 +868,8 @@ impl Index<usize> for ReadableProcessSlice {
     // Cell to read-only operations
     type Output = ReadableProcessByte;
 
-    #[flux_rs::sig(fn(self: &ReadableProcessSlice[@len], idx: usize) -> &Self::Output requires len > idx)]
+    #[flux_rs::trusted_impl]
+    #[flux_rs::sig(fn(self: &ReadableProcessSlice[@len], idx: usize ) -> &Self::Output requires len > idx)]
     fn index(&self, idx: usize) -> &Self::Output {
         // As ReadableProcessSlice is a transparent wrapper around its
         // inner type, [ReadableProcessByte], we can use the regular
@@ -1108,6 +1109,7 @@ impl Index<usize> for WriteableProcessSlice {
     // mutating the memory contents is allowed.
     type Output = Cell<u8>;
 
+    #[flux_rs::trusted_impl]
     #[flux_rs::sig(fn(self: &WriteableProcessSlice[@len], idx: usize) -> &Self::Output requires len > idx)]
     fn index(&self, idx: usize) -> &Self::Output {
         // As WriteableProcessSlice is a transparent wrapper around