Allow usage of snapshot! in ghost code

A missing `#[pure]` annotation made this impossible before.
creusot-rs · Nov 28, 2024 · d14b7d8 · d14b7d8
1 parent 244fefa
commit d14b7d8
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 0 deletions.
diff --git a/creusot-contracts/src/snapshot.rs b/creusot-contracts/src/snapshot.rs
@@ -28,6 +28,7 @@ impl<T: View + ?Sized> View for Snapshot<T> {
 }
 
 impl<T: ?Sized> Clone for Snapshot<T> {
+    #[pure]
     #[ensures(result == *self)]
     fn clone(&self) -> Self {
         snapshot! { **self }

diff --git a/creusot-contracts/src/stubs.rs b/creusot-contracts/src/stubs.rs
@@ -64,6 +64,7 @@ pub fn variant_check<R: crate::well_founded::WellFounded + ?Sized>(_: R) -> Box<
 #[rustc_diagnostic_item = "closure_result_constraint"]
 pub fn closure_result<R: ?Sized>(_: R, _: R) {}
 
+#[crate::pure]
 #[creusot::no_translate]
 #[rustc_diagnostic_item = "snapshot_from_fn"]
 pub fn snapshot_from_fn<T: ?Sized, F: Fn() -> crate::Snapshot<T>>(_: F) -> crate::Snapshot<T> {