From 4380e47bedc1fdac09b044f00637773280785c12 Mon Sep 17 00:00:00 2001 From: Evan Johnson Date: Fri, 22 Nov 2024 10:27:22 -0800 Subject: [PATCH] peel back trusted --- kernel/src/collections/queue.rs | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/kernel/src/collections/queue.rs b/kernel/src/collections/queue.rs index caa65c1ee9..e619566983 100644 --- a/kernel/src/collections/queue.rs +++ b/kernel/src/collections/queue.rs @@ -16,23 +16,19 @@ pub trait Queue { /// 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] // Unexpected Evar - // #[flux_rs::sig(fn(self: &strg Self, _) -> bool ensures self: Self)] + #[flux_rs::sig(fn(self: &strg Self, _) -> bool ensures self: Self)] 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] // Unexpected Evar - // #[flux_rs::sig(fn(self: &strg Self, _) -> Option ensures self: Self)] + #[flux_rs::sig(fn(self: &strg Self, _) -> Option ensures self: Self)] fn push(&mut self, val: T) -> Option; /// Remove the element from the front of the queue. - #[flux_rs::trusted_impl] // Unexpected Evar - // #[flux_rs::sig(fn(self: &strg Self) -> Option ensures self: Self)] + #[flux_rs::sig(fn(self: &strg Self) -> Option ensures self: Self)] fn dequeue(&mut self) -> Option; /// Remove and return one (the first) element that matches the predicate. - #[flux_rs::trusted_impl] // Unexpected evar - // #[flux_rs::sig(fn(self: &strg Self, _) -> Option ensures self: Self)] + #[flux_rs::sig(fn(self: &strg Self, _) -> Option ensures self: Self)] fn remove_first_matching(&mut self, f: F) -> Option where F: Fn(&T) -> bool;