Merge pull request #1264 from arnaudgolfouse/snapshot-ghost

`snapshot!` in ghost

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 }

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> {

creusot/tests/should_succeed/ghost/snapshot_in_ghost.rs

@@ -0,0 +1,17 @@
+extern crate creusot_contracts;
+use creusot_contracts::*;
+
+// Check that we can make snapshots in ghost code.
+pub fn foo() {
+    ghost! {
+        let x = snapshot!(1);
+        proof_assert!(*x == 1);
+    };
+}
+
+// Check that we can make snapshots in pure functions.
+#[pure]
+pub fn is_pure() {
+    let x = snapshot!(1);
+    proof_assert!(*x == 1);
+}