Merge pull request #1061 from dewert99/ghostptrtoken-derefmut

Fix spec for `GhostPtrTokenMut::deref_mut`
creusot-rs · Aug 6, 2024 · 9644f4e · 9644f4e
2 parents d7e2eef + 06ca9ca
commit 9644f4e
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git 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
@@ -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