format code

creusot-contracts/src/lib.rs

@@ -216,9 +216,9 @@ pub mod snapshot {
     impl<T: ?Sized> Copy for Snapshot<T> {}
 }
 
-pub mod ptr_own;
 pub mod invariant;
 pub mod model;
+pub mod ptr_own;
 pub mod resolve;
 pub mod util;
 pub mod well_founded;

creusot-contracts/src/ptr_own.rs

@@ -1,6 +1,6 @@
-use crate::*;
 #[cfg(creusot)]
 use crate::util::SizedW;
+use crate::*;
 
 /// Raw pointer whose ownership is tracked by a ghost [PtrOwn].
 pub type RawPtr<T> = *const T;
@@ -20,11 +20,15 @@ pub struct PtrOwn<T: ?Sized>(std::marker::PhantomData<T>);
 impl<T: ?Sized> PtrOwn<T> {
     #[trusted]
     #[logic]
-    pub fn ptr(&self) -> RawPtr<T> { dead }
+    pub fn ptr(&self) -> RawPtr<T> {
+        dead
+    }
 
     #[trusted]
     #[logic]
-    pub fn val(&self) -> SizedW<T> { dead }
+    pub fn val(&self) -> SizedW<T> {
+        dead
+    }
 }
 
 impl<T: ?Sized> Invariant for PtrOwn<T> {
@@ -48,14 +52,8 @@ pub fn new<T>(v: T) -> (RawPtr<T>, GhostBox<PtrOwn<T>>) {
 #[trusted]
 #[ensures(result.1.ptr() == result.0 && *result.1.val() == *val)]
 pub fn from_box<T: ?Sized>(val: Box<T>) -> (RawPtr<T>, GhostBox<PtrOwn<T>>) {
-    assert!(
-        core::mem::size_of_val::<T>(&*val) > 0,
-        "PtrOwn doesn't support ZSTs"
-    );
-    (
-        Box::into_raw(val),
-        GhostBox::conjure(),
-    )
+    assert!(core::mem::size_of_val::<T>(&*val) > 0, "PtrOwn doesn't support ZSTs");
+    (Box::into_raw(val), GhostBox::conjure())
 }
 
 /// Immutably borrows the underlying `T`.

creusot/tests/should_succeed/linked_list.rs

@@ -1,5 +1,9 @@
 extern crate creusot_contracts;
-use creusot_contracts::{logic::Seq, ptr_own::{RawPtr, PtrOwn}, *};
+use creusot_contracts::{
+    logic::Seq,
+    ptr_own::{PtrOwn, RawPtr},
+    *,
+};
 
 struct Cell<T> {
     v: T,
@@ -75,19 +79,12 @@ fn seq_map_snoc<T, U>() {}
 impl<T> List<T> {
     #[ensures(result@ == Seq::EMPTY)]
     pub fn new() -> List<T> {
-        List {
-            first: std::ptr::null(),
-            last: std::ptr::null(),
-            seq: Seq::new(),
-        }
+        List { first: std::ptr::null(), last: std::ptr::null(), seq: Seq::new() }
     }
 
     #[ensures((^self)@ == (*self)@.push_back(x))]
     pub fn push_back(&mut self, x: T) {
-        let cell = Box::new(Cell {
-            v: x,
-            next: std::ptr::null(),
-        });
+        let cell = Box::new(Cell { v: x, next: std::ptr::null() });
         let (cell_ptr, cell_own) = ptr_own::from_box(cell);
         if self.last.is_null() {
             self.first = cell_ptr;
@@ -111,10 +108,7 @@ impl<T> List<T> {
 
     #[ensures((^self)@ == (*self)@.push_front(x))]
     pub fn push_front(&mut self, x: T) {
-        let (cell_ptr, cell_own) = ptr_own::new(Cell {
-            v: x,
-            next: self.first,
-        });
+        let (cell_ptr, cell_own) = ptr_own::new(Cell { v: x, next: self.first });
         self.first = cell_ptr;
         if self.last.is_null() {
             self.last = cell_ptr;