Merge pull request #912 from arnaudgolfouse/final-borrow

implementation of final borrows
creusot-rs · Jan 29, 2024 · 846d296 · 846d296
2 parents 66b0ae4 + 7adfb17
commit 846d296
Show file tree

Hide file tree

Showing 283 changed files with 7,225 additions and 3,936 deletions.
diff --git a/creusot-contracts/src/std/slice.rs b/creusot-contracts/src/std/slice.rs
@@ -281,7 +281,7 @@ extern_spec! {
                 (**self)@.len() > 0 && (^*self)@.len() > 0 &&
                 (*^self)@ == (**self)@.tail() && (^^self)@ == (^*self)@.tail()
             }
-            None => ^self == * self && (**self)@.len() == 0
+            None => (*^self)@ == Seq::EMPTY && (^*self)@ == Seq::EMPTY && (**self)@ == Seq::EMPTY && (^^self)@ == Seq::EMPTY
         })]
         fn take_first_mut<'a>(self_: &mut &'a mut [T]) -> Option<&'a mut T>;
 

diff --git a/creusot/src/analysis.rs b/creusot/src/analysis.rs
@@ -12,11 +12,13 @@ use rustc_middle::mir::{
 mod frozen_locals;
 mod init_locals;
 mod liveness_no_drop;
+mod not_final_places;
 mod uninit_locals;
 
 pub use frozen_locals::*;
 pub use init_locals::*;
 pub use liveness_no_drop::*;
+pub use not_final_places::NotFinalPlaces;
 pub use uninit_locals::*;
 
 pub struct NeverLive(BitSet<Local>);