avoid the allocator feature to keep vstd compiling on stable rust

verus-lang · Nov 13, 2023 · 146fe0b · 146fe0b
1 parent 8fbbc3c
commit 146fe0b
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 8 deletions.
diff --git a/source/pervasive/ptr.rs b/source/pervasive/ptr.rs
@@ -2,7 +2,6 @@
 
 use alloc::alloc::Layout;
 use core::{marker, mem, mem::MaybeUninit};
-use alloc::alloc::Allocator;
 
 use builtin::*;
 use builtin_macros::*;
@@ -11,6 +10,8 @@ use crate::pervasive::*;
 use crate::modes::*;
 use crate::prelude::*;
 use crate::layout::*;
+
+#[cfg(verus_keep_ghost)]
 use crate::set_lib::set_int_range;
 
 verus!{
@@ -519,7 +520,7 @@ impl<V> PPtr<V> {
         // The 'add' can't overflow, since we already know (size, align) is a valid layout.
         let layout = Layout::from_size_align(size + align, align).unwrap();
         let p = PPtr {
-            uptr: alloc::alloc::Global.allocate(layout).unwrap().as_ptr() as *mut V,
+            uptr: unsafe { std::alloc::alloc(layout) as *mut V },
         };
 
         // See explanation about exposing pointers, above
@@ -645,13 +646,12 @@ impl<V> PPtr<V> {
         opens_invariants none
     {
         unsafe {
-            let nn = core::ptr::NonNull::new_unchecked(self.uptr as *mut u8);
             let layout = alloc::alloc::Layout::for_value(&*self.uptr);
             let size = layout.size();
             let align = layout.align();
             // Add the padding to match what we did in 'alloc'
             let layout = Layout::from_size_align_unchecked(size + align, align);
-            alloc::alloc::Global.deallocate(nn, alloc::alloc::Layout::for_value(&*self.uptr));
+            std::alloc::dealloc(self.uptr as *mut u8, alloc::alloc::Layout::for_value(&*self.uptr));
         }
     }
 
@@ -675,8 +675,7 @@ impl<V> PPtr<V> {
             // and that it's safe to call 'deallocate'
             // Remember to add the padding, like in `alloc`
             let layout = Layout::from_size_align_unchecked(size + align, align);
-            let nn = core::ptr::NonNull::new_unchecked(self.uptr as *mut u8);
-            alloc::alloc::Global.deallocate(nn, alloc::alloc::Layout::for_value(&*self.uptr));
+            std::alloc::dealloc(self.uptr as *mut u8, alloc::alloc::Layout::for_value(&*self.uptr));
         }
     }
 

diff --git a/source/pervasive/vstd.rs b/source/pervasive/vstd.rs
@@ -10,8 +10,8 @@
 #![allow(unused_attributes)]
 #![allow(rustdoc::invalid_rust_codeblocks)]
 
-#![feature(allocator_api)]
 #![cfg_attr(verus_keep_ghost, feature(core_intrinsics))]
+#![cfg_attr(verus_keep_ghost, feature(allocator_api))]
 
 #[cfg(feature = "alloc")]
 extern crate alloc;

diff --git a/source/tools/docs.sh b/source/tools/docs.sh
@@ -36,7 +36,6 @@ RUSTC_BOOTSTRAP=1 eval ""VERUSDOC=1 VERUS_Z3_PATH="$(pwd)/z3" rustdoc \
   -Zcrate-attr=feature\\\(register_tool\\\) \
   -Zcrate-attr=feature\\\(rustc_attrs\\\) \
   -Zcrate-attr=feature\\\(unboxed_closures\\\) \
-  -Zcrate-attr=feature\\\(allocator_api\\\) \
   -Zcrate-attr=register_tool\\\(verus\\\) \
   -Zcrate-attr=register_tool\\\(verifier\\\) \
   pervasive/vstd.rs""