From 06ca9ca723ae491af3de672516c12a40500ef728 Mon Sep 17 00:00:00 2001 From: dewert99 Date: Tue, 6 Aug 2024 09:02:17 -0700 Subject: [PATCH] Fix spec for `GhostPtrTokenMut::deref_mut` --- creusot-contracts/src/ghost_ptr.rs | 1 + creusot/tests/should_succeed/ghost_ptr_token.coma | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/creusot-contracts/src/ghost_ptr.rs b/creusot-contracts/src/ghost_ptr.rs index 9db635d3ea..1f130e1fa4 100644 --- a/creusot-contracts/src/ghost_ptr.rs +++ b/creusot-contracts/src/ghost_ptr.rs @@ -267,6 +267,7 @@ impl<'a, T: ?Sized> DerefMut for GhostPtrTokenMut<'a, T> { #[trusted] #[ensures((*result)@ == (*self).cur())] #[ensures((^self).cur() == (^result)@)] + #[ensures((^self).fin() == (*self).fin())] fn deref_mut(&mut self) -> &mut Self::Target { Box::leak(Box::new(GhostPtrToken(PhantomData))) } diff --git a/creusot/tests/should_succeed/ghost_ptr_token.coma b/creusot/tests/should_succeed/ghost_ptr_token.coma index 6b5463622f..a990f70993 100644 --- a/creusot/tests/should_succeed/ghost_ptr_token.coma +++ b/creusot/tests/should_succeed/ghost_ptr_token.coma @@ -186,7 +186,7 @@ module GhostPtrToken_Test let%span span44 = "../../../../creusot-contracts/src/ghost_ptr.rs" 202 4 202 44 - let%span span45 = "../../../../creusot-contracts/src/ghost_ptr.rs" 280 8 280 32 + let%span span45 = "../../../../creusot-contracts/src/ghost_ptr.rs" 281 8 281 32 let%span span46 = "../../../../creusot-contracts/src/logic/fmap.rs" 13 15 13 19