mark flux_support as #![no_std]

PLSysSec · Oct 2, 2024 · 39e7ae5 · 39e7ae5
1 parent 9bc1237
commit 39e7ae5
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 3 deletions.
diff --git a/flux_support/src/extern_specs/iter.rs b/flux_support/src/extern_specs/iter.rs
@@ -1,6 +1,6 @@
 #![allow(unused)]
 use crate::assert;
-use std::slice::Iter; // TODO: not allowed to use std
+use core::slice::Iter;
 
 #[flux_rs::extern_spec(std::slice)]
 #[flux_rs::refined_by(idx: int, len: int)]

diff --git a/flux_support/src/extern_specs/slice.rs b/flux_support/src/extern_specs/slice.rs
@@ -1,5 +1,5 @@
 #![allow(unused)]
-use std::slice::{Iter, SliceIndex}; // TODO: not allowed to use std
+use core::slice::{Iter, SliceIndex}; // TODO: not allowed to use std
 
 // #[flux_rs::extern_spec]
 // #[generics(Self as base, T as base)]

diff --git a/flux_support/src/flux_ptr.rs b/flux_support/src/flux_ptr.rs
@@ -1,10 +1,12 @@
 use core::clone::Clone;
 use core::cmp::Eq;
+use core::cmp::Ord;
 use core::cmp::PartialEq;
 use core::cmp::PartialOrd;
 use core::convert::From;
 use core::fmt::Debug;
 use core::marker::Copy;
+use core::ops::Rem;
 use core::ops::{Deref, DerefMut};
 use core::option::Option;
 use core::option::Option::Some;
@@ -13,7 +15,6 @@ use core::ptr::NonNull;
 use core::todo;
 use core::unimplemented;
 use flux_rs::{refined_by, sig};
-use std::ops::Rem; // TODO: not allowed to use std
 
 #[flux_rs::opaque]
 #[derive(Clone, Copy, Debug, PartialEq, Eq)]
@@ -22,6 +23,7 @@ pub struct FluxPtr {
     inner: *mut u8,
 }
 
+#[flux_rs::trusted]
 impl From<usize> for FluxPtr {
     fn from(value: usize) -> Self {
         FluxPtr {
@@ -37,6 +39,7 @@ impl From<FluxPtr> for u32 {
     }
 }
 // convert FluxPtr to *const u8
+#[flux_rs::trusted]
 impl From<FluxPtr> for u8 {
     fn from(ptr: FluxPtr) -> u8 {
         ptr.inner as u8
@@ -50,6 +53,7 @@ impl From<FluxPtr> for usize {
 }
 
 // Implement Rem trait for FluxPtr
+#[flux_rs::trusted]
 impl Rem<usize> for FluxPtr {
     type Output = usize;
 
@@ -59,6 +63,7 @@ impl Rem<usize> for FluxPtr {
 }
 
 // implement implement `AddAssign<usize>`` for FluxPtr
+#[flux_rs::trusted]
 impl core::ops::AddAssign<usize> for FluxPtr {
     fn add_assign(&mut self, rhs: usize) {
         *self = FluxPtr {

diff --git a/flux_support/src/lib.rs b/flux_support/src/lib.rs
@@ -1,3 +1,5 @@
+#![no_std]
+
 mod extern_specs;
 mod flux_ptr;
 mod flux_range;