conditionalize std specs

prusti-contracts/prusti-std/Cargo.toml

@@ -14,6 +14,9 @@ categories = ["development-tools", "development-tools::testing"]
 [dependencies]
 prusti-contracts = { path = "../prusti-contracts", version = "0.1.2" }
 
-# Forward "prusti" flag
 [features]
+default = ["alloc", "std"]
+alloc = []
+std = []
+# Forward "prusti" flag
 prusti = ["prusti-contracts/prusti"]

prusti-contracts/prusti-std/src/alloc_spec/mod.rs

@@ -1,5 +1,5 @@
-// In future, it might make sense to move these specs to yet another crate or have a feature to disable the std parts of this crate.
-// alloc is usable in some no_std environments, so it would be helpful to support the use case of core + alloc without std.
+// These specs can't be built-in like the core specs since some no_std crates may not even have an allocator.
+// Instead, prusti-std supports no_std through a feature.
 
 pub mod string;
 pub mod vec;

prusti-contracts/prusti-std/src/lib.rs

@@ -1,6 +1,16 @@
 #![feature(allocator_api)] // to specify Vec
+#![no_std] // disable std by default
 
+// link to std if the feature is set
+#[cfg(feature = "std")]
+extern crate std;
+
+// Even alloc can be disabled for consistency with std, and in preparation for future specs for other, possibly no_std, crates.
+#[cfg(feature = "alloc")]
 extern crate alloc;
 
+// modules have a `_spec` suffix to avoid name conflicts with their crates.
+#[cfg(feature = "alloc")]
 pub mod alloc_spec;
-pub mod collections;
+#[cfg(feature = "std")]
+pub mod std_spec;

prusti-contracts/prusti-std/src/std_spec/mod.rs

@@ -0,0 +1 @@
+pub mod collections;