Some changes had accidentally been reverted

model-checking · Nov 22, 2023 · 4b451cf · 4b451cf
1 parent 0c3cea7
commit 4b451cf
Show file tree

Hide file tree

Showing 3 changed files with 35 additions and 17 deletions.
diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
@@ -93,36 +93,54 @@ macro_rules! implies {
 }
 
 #[doc(hidden)]
-pub trait DecoupleLifetime<'a> {
+pub trait Pointer<'a> {
  type Inner;
- unsafe fn decouple_lifetime(&self) -> &'a Self::Inner;
+ unsafe fn decouple_lifetime(self) -> &'a Self::Inner;
+
+ unsafe fn assignable(self) -> &'a mut Self::Inner;
 }
 
-impl<'a, 'b, T> DecoupleLifetime<'a> for &'b T {
+impl<'a, 'b, T> Pointer<'a> for &'b T {
  type Inner = T;
- unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
- std::mem::transmute(*self)
+ unsafe fn decouple_lifetime(self) -> &'a Self::Inner {
+ std::mem::transmute(self)
+ }
+
+ unsafe fn assignable(self) -> &'a mut Self::Inner {
+ std::mem::transmute(self as *const T)
  }
 }
 
-impl<'a, 'b, T> DecoupleLifetime<'a> for &'b mut T {
+impl<'a, 'b, T> Pointer<'a> for &'b mut T {
  type Inner = T;
- unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
- *std::mem::transmute::<&'_ &'b mut T, &'_ &'a T>(self)
+ unsafe fn decouple_lifetime(self) -> &'a Self::Inner {
+ std::mem::transmute(self as *mut T)
+ }
+
+ unsafe fn assignable(self) -> &'a mut Self::Inner {
+ std::mem::transmute(self)
  }
 }
 
-impl<'a, T> DecoupleLifetime<'a> for *const T {
+impl<'a, T> Pointer<'a> for *const T {
  type Inner = T;
- unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
- &**self as &'a T
+ unsafe fn decouple_lifetime(self) -> &'a Self::Inner {
+ &*self as &'a T
+ }
+
+ unsafe fn assignable(self) -> &'a mut Self::Inner {
+ std::mem::transmute(self)
  }
 }
 
-impl<'a, T> DecoupleLifetime<'a> for *mut T {
+impl<'a, T> Pointer<'a> for *mut T {
  type Inner = T;
- unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
- &**self as &'a T
+ unsafe fn decouple_lifetime(self) -> &'a Self::Inner {
+ &*self as &'a T
+ }
+
+ unsafe fn assignable(self) -> &'a mut Self::Inner {
+ std::mem::transmute(self)
  }
 }
 

diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs
@@ -529,7 +529,7 @@ impl<'a> ContractConditionsHandler<'a> {
  let wrapper_args = make_wrapper_args(attr.len());
 
  quote!(
- #(let #wrapper_args = unsafe { kani::DecoupleLifetime::decouple_lifetime(&#attr) };)*
+ #(let #wrapper_args = unsafe { kani::Pointer::decouple_lifetime(#attr) };)*
  #(#inner)*
  )
  }
@@ -605,7 +605,7 @@ impl<'a> ContractConditionsHandler<'a> {
  ContractConditionsData::Modifies { attr } => {
  quote!(
  let result = #call_to_prior;
- #(*#attr = kani::any();)*
+ #(*unsafe { kani::Pointer::assignable(#attr) } = kani::any();)*
  result
  )
  }

diff --git a/tests/expected/function-contract/assigns_pass.expected b/tests/expected/function-contract/assigns_pass.expected
@@ -1 +1 @@
-VERIFICATION:- FAILED
+VERIFICATION:- SUCCESSFUL