From ca90cd0c6713c59a6ecf0ea3febed54e1943be65 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Arma=C3=ABl=20Gu=C3=A9neau?= Date: Wed, 20 Nov 2024 17:11:53 +0100 Subject: [PATCH] format code --- creusot-contracts/src/lib.rs | 2 +- creusot-contracts/src/ptr_own.rs | 20 ++- creusot/tests/should_succeed/linked_list.coma | 116 +++++++++--------- creusot/tests/should_succeed/linked_list.rs | 22 ++-- 4 files changed, 76 insertions(+), 84 deletions(-) diff --git a/creusot-contracts/src/lib.rs b/creusot-contracts/src/lib.rs index 121e29aacb..07e9bea5d5 100644 --- a/creusot-contracts/src/lib.rs +++ b/creusot-contracts/src/lib.rs @@ -216,9 +216,9 @@ pub mod snapshot { impl Copy for Snapshot {} } -pub mod ptr_own; pub mod invariant; pub mod model; +pub mod ptr_own; pub mod resolve; pub mod util; pub mod well_founded; diff --git a/creusot-contracts/src/ptr_own.rs b/creusot-contracts/src/ptr_own.rs index 0f97487613..8f1e7f7c3f 100644 --- a/creusot-contracts/src/ptr_own.rs +++ b/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 = *const T; @@ -20,11 +20,15 @@ pub struct PtrOwn(std::marker::PhantomData); impl PtrOwn { #[trusted] #[logic] - pub fn ptr(&self) -> RawPtr { dead } + pub fn ptr(&self) -> RawPtr { + dead + } #[trusted] #[logic] - pub fn val(&self) -> SizedW { dead } + pub fn val(&self) -> SizedW { + dead + } } impl Invariant for PtrOwn { @@ -48,14 +52,8 @@ pub fn new(v: T) -> (RawPtr, GhostBox>) { #[trusted] #[ensures(result.1.ptr() == result.0 && *result.1.val() == *val)] pub fn from_box(val: Box) -> (RawPtr, GhostBox>) { - assert!( - core::mem::size_of_val::(&*val) > 0, - "PtrOwn doesn't support ZSTs" - ); - ( - Box::into_raw(val), - GhostBox::conjure(), - ) + assert!(core::mem::size_of_val::(&*val) > 0, "PtrOwn doesn't support ZSTs"); + (Box::into_raw(val), GhostBox::conjure()) } /// Immutably borrows the underlying `T`. diff --git a/creusot/tests/should_succeed/linked_list.coma b/creusot/tests/should_succeed/linked_list.coma index 6caee580e4..0b609f0c6c 100644 --- a/creusot/tests/should_succeed/linked_list.coma +++ b/creusot/tests/should_succeed/linked_list.coma @@ -1,7 +1,7 @@ -module M_linked_list__seq_map_cons [#"linked_list.rs" 68 0 68 23] - let%span slinked_list0 = "linked_list.rs" 66 10 67 69 +module M_linked_list__seq_map_cons [#"linked_list.rs" 72 0 72 23] + let%span slinked_list0 = "linked_list.rs" 70 10 71 69 let%span sseq1 = "../../../creusot-contracts/src/logic/seq.rs" 143 8 143 27 - let%span slinked_list2 = "linked_list.rs" 62 4 62 41 + let%span slinked_list2 = "linked_list.rs" 66 4 66 41 use prelude.prelude.Intrinsic @@ -32,7 +32,7 @@ module M_linked_list__seq_map_cons [#"linked_list.rs" 68 0 68 23] use seq.Seq - function seq_map'0 [#"linked_list.rs" 61 0 61 66] (s : Seq.seq t_T'0) (f : Map.map t_T'0 t_U'0) : Seq.seq t_U'0 = + function seq_map'0 [#"linked_list.rs" 65 0 65 66] (s : Seq.seq t_T'0) (f : Map.map t_T'0 t_U'0) : Seq.seq t_U'0 = [%#slinked_list2] Seq.create (Seq.length s) (Mapping.from_fn (fun (i : int) -> Map.get f (Seq.get s i))) use seq.Seq @@ -48,9 +48,9 @@ module M_linked_list__seq_map_cons [#"linked_list.rs" 68 0 68 23] (! return' {result}) ] end -module M_linked_list__seq_map_snoc [#"linked_list.rs" 73 0 73 23] - let%span slinked_list0 = "linked_list.rs" 71 10 72 67 - let%span slinked_list1 = "linked_list.rs" 62 4 62 41 +module M_linked_list__seq_map_snoc [#"linked_list.rs" 77 0 77 23] + let%span slinked_list0 = "linked_list.rs" 75 10 76 67 + let%span slinked_list1 = "linked_list.rs" 66 4 66 41 use prelude.prelude.Intrinsic @@ -78,7 +78,7 @@ module M_linked_list__seq_map_snoc [#"linked_list.rs" 73 0 73 23] use seq.Seq - function seq_map'0 [#"linked_list.rs" 61 0 61 66] (s : Seq.seq t_T'0) (f : Map.map t_T'0 t_U'0) : Seq.seq t_U'0 = + function seq_map'0 [#"linked_list.rs" 65 0 65 66] (s : Seq.seq t_T'0) (f : Map.map t_T'0 t_U'0) : Seq.seq t_U'0 = [%#slinked_list1] Seq.create (Seq.length s) (Mapping.from_fn (fun (i : int) -> Map.get f (Seq.get s i))) use seq.Seq @@ -91,24 +91,24 @@ module M_linked_list__seq_map_snoc [#"linked_list.rs" 73 0 73 23] (! return' {result}) ] end -module M_linked_list__qyi14323471455460008969__new [#"linked_list.rs" 77 4 77 27] (* List *) - let%span slinked_list0 = "linked_list.rs" 79 19 79 35 - let%span slinked_list1 = "linked_list.rs" 80 18 80 34 - let%span slinked_list2 = "linked_list.rs" 81 17 81 27 - let%span slinked_list3 = "linked_list.rs" 77 20 77 27 - let%span slinked_list4 = "linked_list.rs" 76 14 76 35 +module M_linked_list__qyi14323471455460008969__new [#"linked_list.rs" 81 4 81 27] (* List *) + let%span slinked_list0 = "linked_list.rs" 82 22 82 38 + let%span slinked_list1 = "linked_list.rs" 82 46 82 62 + let%span slinked_list2 = "linked_list.rs" 82 69 82 79 + let%span slinked_list3 = "linked_list.rs" 81 20 81 27 + let%span slinked_list4 = "linked_list.rs" 80 14 80 35 let%span sptr5 = "../../../creusot-contracts/src/std/ptr.rs" 121 22 121 44 let%span sseq6 = "../../../creusot-contracts/src/logic/seq.rs" 254 4 254 34 let%span sseq7 = "../../../creusot-contracts/src/logic/seq.rs" 252 14 252 36 - let%span slinked_list8 = "linked_list.rs" 44 12 44 74 + let%span slinked_list8 = "linked_list.rs" 48 12 48 74 let%span sptr9 = "../../../creusot-contracts/src/std/ptr.rs" 80 14 80 48 let%span sptr10 = "../../../creusot-contracts/src/std/ptr.rs" 82 8 82 30 let%span sghost11 = "../../../creusot-contracts/src/ghost.rs" 200 9 200 15 - let%span slinked_list12 = "linked_list.rs" 62 4 62 41 - let%span slinked_list13 = "linked_list.rs" 22 12 32 69 + let%span slinked_list12 = "linked_list.rs" 66 4 66 41 + let%span slinked_list13 = "linked_list.rs" 26 12 36 69 let%span sboxed14 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 let%span sseq15 = "../../../creusot-contracts/src/logic/seq.rs" 444 20 444 95 - let%span sptr_own16 = "../../../creusot-contracts/src/ptr_own.rs" 36 20 36 66 + let%span sptr_own16 = "../../../creusot-contracts/src/ptr_own.rs" 40 20 40 66 use prelude.prelude.Opaque @@ -216,7 +216,7 @@ module M_linked_list__qyi14323471455460008969__new [#"linked_list.rs" 77 4 77 27 use seq.Seq - predicate invariant'0 [#"linked_list.rs" 20 4 20 30] (self : t_List'0) = + predicate invariant'0 [#"linked_list.rs" 24 4 24 30] (self : t_List'0) = [%#slinked_list13] inner_logic'0 self.t_List__seq'0 = (Seq.empty : Seq.seq (t_PtrOwn'0)) /\ is_null_logic'0 self.t_List__first'0 /\ is_null_logic'0 self.t_List__last'0 \/ Seq.length (inner_logic'0 self.t_List__seq'0) > 0 @@ -249,12 +249,12 @@ module M_linked_list__qyi14323471455460008969__new [#"linked_list.rs" 77 4 77 27 use seq.Seq - function seq_map'0 [#"linked_list.rs" 61 0 61 66] (s : Seq.seq (t_PtrOwn'0)) (f : Map.map (t_PtrOwn'0) t_T'0) : Seq.seq t_T'0 + function seq_map'0 [#"linked_list.rs" 65 0 65 66] (s : Seq.seq (t_PtrOwn'0)) (f : Map.map (t_PtrOwn'0) t_T'0) : Seq.seq t_T'0 = [%#slinked_list12] Seq.create (Seq.length s) (Mapping.from_fn (fun (i : int) -> Map.get f (Seq.get s i))) - function view'0 [#"linked_list.rs" 42 4 42 33] (self : t_List'0) : Seq.seq t_T'0 = + function view'0 [#"linked_list.rs" 46 4 46 33] (self : t_List'0) : Seq.seq t_T'0 = [%#slinked_list8] seq_map'0 (inner_logic'0 self.t_List__seq'0) (Mapping.from_fn (fun (ptr_own : t_PtrOwn'0) -> (val'0 ptr_own).t_Cell__v'0)) use seq.Seq @@ -279,28 +279,28 @@ module M_linked_list__qyi14323471455460008969__new [#"linked_list.rs" 77 4 77 27 end module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 86 4 86 37] (* List *) - let%span slinked_list0 = "linked_list.rs" 89 18 89 34 - let%span slinked_list1 = "linked_list.rs" 109 8 109 44 + let%span slinked_list0 = "linked_list.rs" 87 47 87 63 + let%span slinked_list1 = "linked_list.rs" 106 8 106 44 let%span slinked_list2 = "linked_list.rs" 86 26 86 30 let%span slinked_list3 = "linked_list.rs" 86 32 86 33 let%span slinked_list4 = "linked_list.rs" 85 14 85 47 let%span sptr5 = "../../../creusot-contracts/src/std/ptr.rs" 121 22 121 44 - let%span sptr_own6 = "../../../creusot-contracts/src/ptr_own.rs" 50 27 50 30 - let%span sptr_own7 = "../../../creusot-contracts/src/ptr_own.rs" 50 0 50 75 - let%span sptr_own8 = "../../../creusot-contracts/src/ptr_own.rs" 49 10 49 63 + let%span sptr_own6 = "../../../creusot-contracts/src/ptr_own.rs" 54 27 54 30 + let%span sptr_own7 = "../../../creusot-contracts/src/ptr_own.rs" 54 0 54 75 + let%span sptr_own8 = "../../../creusot-contracts/src/ptr_own.rs" 53 10 53 63 let%span sptr9 = "../../../creusot-contracts/src/std/ptr.rs" 107 18 107 48 let%span sghost10 = "../../../creusot-contracts/src/ghost.rs" 121 27 121 31 let%span sghost11 = "../../../creusot-contracts/src/ghost.rs" 121 4 121 52 let%span sghost12 = "../../../creusot-contracts/src/ghost.rs" 120 14 120 39 - let%span slinked_list13 = "linked_list.rs" 101 16 104 17 - let%span sptr_own14 = "../../../creusot-contracts/src/ptr_own.rs" 84 41 84 44 - let%span sptr_own15 = "../../../creusot-contracts/src/ptr_own.rs" 73 11 73 27 - let%span sptr_own16 = "../../../creusot-contracts/src/ptr_own.rs" 84 0 84 81 - let%span sptr_own17 = "../../../creusot-contracts/src/ptr_own.rs" 74 10 74 31 - let%span sptr_own18 = "../../../creusot-contracts/src/ptr_own.rs" 82 10 82 49 - let%span sptr_own19 = "../../../creusot-contracts/src/ptr_own.rs" 83 10 83 48 - let%span slinked_list20 = "linked_list.rs" 71 10 72 67 - let%span slinked_list21 = "linked_list.rs" 44 12 44 74 + let%span slinked_list13 = "linked_list.rs" 98 16 101 17 + let%span sptr_own14 = "../../../creusot-contracts/src/ptr_own.rs" 82 41 82 44 + let%span sptr_own15 = "../../../creusot-contracts/src/ptr_own.rs" 71 11 71 27 + let%span sptr_own16 = "../../../creusot-contracts/src/ptr_own.rs" 82 0 82 81 + let%span sptr_own17 = "../../../creusot-contracts/src/ptr_own.rs" 72 10 72 31 + let%span sptr_own18 = "../../../creusot-contracts/src/ptr_own.rs" 80 10 80 49 + let%span sptr_own19 = "../../../creusot-contracts/src/ptr_own.rs" 81 10 81 48 + let%span slinked_list20 = "linked_list.rs" 75 10 76 67 + let%span slinked_list21 = "linked_list.rs" 48 12 48 74 let%span sptr22 = "../../../creusot-contracts/src/std/ptr.rs" 80 14 80 48 let%span sptr23 = "../../../creusot-contracts/src/std/ptr.rs" 82 8 82 30 let%span sghost24 = "../../../creusot-contracts/src/ghost.rs" 200 9 200 15 @@ -323,22 +323,22 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 86 4 let%span sghost41 = "../../../creusot-contracts/src/ghost.rs" 51 14 51 35 let%span sseq42 = "../../../creusot-contracts/src/logic/seq.rs" 278 22 278 26 let%span sseq43 = "../../../creusot-contracts/src/logic/seq.rs" 277 14 277 34 - let%span slinked_list44 = "linked_list.rs" 51 10 51 25 + let%span slinked_list44 = "linked_list.rs" 55 10 55 25 let%span sseq45 = "../../../creusot-contracts/src/logic/seq.rs" 380 30 380 34 let%span sseq46 = "../../../creusot-contracts/src/logic/seq.rs" 380 4 380 65 let%span sseq47 = "../../../creusot-contracts/src/logic/seq.rs" 374 14 377 5 let%span sseq48 = "../../../creusot-contracts/src/logic/seq.rs" 378 14 378 84 let%span sseq49 = "../../../creusot-contracts/src/logic/seq.rs" 379 14 379 44 let%span soption50 = "../../../creusot-contracts/src/std/option.rs" 31 0 423 1 - let%span slinked_list51 = "linked_list.rs" 62 4 62 41 + let%span slinked_list51 = "linked_list.rs" 66 4 66 41 let%span sinvariant52 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sseq53 = "../../../creusot-contracts/src/logic/seq.rs" 62 4 62 12 let%span sboxed54 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 let%span sseq55 = "../../../creusot-contracts/src/logic/seq.rs" 444 20 444 95 let%span sresolve56 = "../../../creusot-contracts/src/resolve.rs" 68 8 68 23 - let%span sptr_own57 = "../../../creusot-contracts/src/ptr_own.rs" 36 20 36 66 + let%span sptr_own57 = "../../../creusot-contracts/src/ptr_own.rs" 40 20 40 66 let%span sinvariant58 = "../../../creusot-contracts/src/invariant.rs" 24 8 24 18 - let%span slinked_list59 = "linked_list.rs" 22 12 32 69 + let%span slinked_list59 = "linked_list.rs" 26 12 36 69 use prelude.prelude.Opaque @@ -654,7 +654,7 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 86 4 use seq.Seq - predicate invariant'16 [#"linked_list.rs" 20 4 20 30] (self : t_List'0) = + predicate invariant'16 [#"linked_list.rs" 24 4 24 30] (self : t_List'0) = [%#slinked_list59] inner_logic'2 self.t_List__seq'0 = (Seq.empty : Seq.seq (t_PtrOwn'0)) /\ is_null_logic'0 self.t_List__first'0 /\ is_null_logic'0 self.t_List__last'0 \/ Seq.length (inner_logic'2 self.t_List__seq'0) > 0 @@ -922,7 +922,7 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 86 4 use seq.Seq - function seq_map'0 [#"linked_list.rs" 61 0 61 66] (s : Seq.seq (t_PtrOwn'0)) (f : Map.map (t_PtrOwn'0) t_T'0) : Seq.seq t_T'0 + function seq_map'0 [#"linked_list.rs" 65 0 65 66] (s : Seq.seq (t_PtrOwn'0)) (f : Map.map (t_PtrOwn'0) t_T'0) : Seq.seq t_T'0 = [%#slinked_list51] Seq.create (Seq.length s) (Mapping.from_fn (fun (i : int) -> Map.get f (Seq.get s i))) @@ -937,7 +937,7 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 86 4 use prelude.prelude.Mapping - function view'0 [#"linked_list.rs" 42 4 42 33] (self : t_List'0) : Seq.seq t_T'0 = + function view'0 [#"linked_list.rs" 46 4 46 33] (self : t_List'0) : Seq.seq t_T'0 = [%#slinked_list21] seq_map'0 (inner_logic'2 self.t_List__seq'0) (Mapping.from_fn (fun (ptr_own : t_PtrOwn'0) -> (val'0 ptr_own).t_Cell__v'0)) meta "compute_max_steps" 1000000 @@ -1057,20 +1057,20 @@ module M_linked_list__qyi14323471455460008969__push_back [#"linked_list.rs" 86 4 (! return' {result}) ] end -module M_linked_list__qyi14323471455460008969__push_front [#"linked_list.rs" 113 4 113 38] (* List *) - let%span slinked_list0 = "linked_list.rs" 124 8 124 44 - let%span slinked_list1 = "linked_list.rs" 113 27 113 31 - let%span slinked_list2 = "linked_list.rs" 113 33 113 34 - let%span slinked_list3 = "linked_list.rs" 112 14 112 48 - let%span sptr_own4 = "../../../creusot-contracts/src/ptr_own.rs" 43 14 43 15 - let%span sptr_own5 = "../../../creusot-contracts/src/ptr_own.rs" 43 0 43 55 - let%span sptr_own6 = "../../../creusot-contracts/src/ptr_own.rs" 42 10 42 60 +module M_linked_list__qyi14323471455460008969__push_front [#"linked_list.rs" 110 4 110 38] (* List *) + let%span slinked_list0 = "linked_list.rs" 118 8 118 44 + let%span slinked_list1 = "linked_list.rs" 110 27 110 31 + let%span slinked_list2 = "linked_list.rs" 110 33 110 34 + let%span slinked_list3 = "linked_list.rs" 109 14 109 48 + let%span sptr_own4 = "../../../creusot-contracts/src/ptr_own.rs" 47 14 47 15 + let%span sptr_own5 = "../../../creusot-contracts/src/ptr_own.rs" 47 0 47 55 + let%span sptr_own6 = "../../../creusot-contracts/src/ptr_own.rs" 46 10 46 60 let%span sptr7 = "../../../creusot-contracts/src/std/ptr.rs" 107 18 107 48 let%span sghost8 = "../../../creusot-contracts/src/ghost.rs" 121 27 121 31 let%span sghost9 = "../../../creusot-contracts/src/ghost.rs" 121 4 121 52 let%span sghost10 = "../../../creusot-contracts/src/ghost.rs" 120 14 120 39 - let%span slinked_list11 = "linked_list.rs" 66 10 67 69 - let%span slinked_list12 = "linked_list.rs" 44 12 44 74 + let%span slinked_list11 = "linked_list.rs" 70 10 71 69 + let%span slinked_list12 = "linked_list.rs" 48 12 48 74 let%span sseq13 = "../../../creusot-contracts/src/logic/seq.rs" 143 8 143 27 let%span sghost14 = "../../../creusot-contracts/src/ghost.rs" 200 9 200 15 let%span sptr15 = "../../../creusot-contracts/src/std/ptr.rs" 80 14 80 48 @@ -1089,13 +1089,13 @@ module M_linked_list__qyi14323471455460008969__push_front [#"linked_list.rs" 113 let%span sghost28 = "../../../creusot-contracts/src/ghost.rs" 162 14 162 28 let%span sghost29 = "../../../creusot-contracts/src/ghost.rs" 93 8 93 24 let%span sresolve30 = "../../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span slinked_list31 = "linked_list.rs" 62 4 62 41 + let%span slinked_list31 = "linked_list.rs" 66 4 66 41 let%span sinvariant32 = "../../../creusot-contracts/src/invariant.rs" 34 20 34 44 let%span sseq33 = "../../../creusot-contracts/src/logic/seq.rs" 444 20 444 95 let%span sresolve34 = "../../../creusot-contracts/src/resolve.rs" 68 8 68 23 let%span sboxed35 = "../../../creusot-contracts/src/std/boxed.rs" 28 8 28 18 - let%span sptr_own36 = "../../../creusot-contracts/src/ptr_own.rs" 36 20 36 66 - let%span slinked_list37 = "linked_list.rs" 22 12 32 69 + let%span sptr_own36 = "../../../creusot-contracts/src/ptr_own.rs" 40 20 40 66 + let%span slinked_list37 = "linked_list.rs" 26 12 36 69 use prelude.prelude.Opaque @@ -1410,7 +1410,7 @@ module M_linked_list__qyi14323471455460008969__push_front [#"linked_list.rs" 113 use seq.Seq - predicate invariant'9 [#"linked_list.rs" 20 4 20 30] (self : t_List'0) = + predicate invariant'9 [#"linked_list.rs" 24 4 24 30] (self : t_List'0) = [%#slinked_list37] inner_logic'1 self.t_List__seq'0 = (Seq.empty : Seq.seq (t_PtrOwn'0)) /\ is_null_logic'0 self.t_List__first'0 /\ is_null_logic'0 self.t_List__last'0 \/ Seq.length (inner_logic'1 self.t_List__seq'0) > 0 @@ -1454,7 +1454,7 @@ module M_linked_list__qyi14323471455460008969__push_front [#"linked_list.rs" 113 use seq.Seq - function seq_map'0 [#"linked_list.rs" 61 0 61 66] (s : Seq.seq (t_PtrOwn'0)) (f : Map.map (t_PtrOwn'0) t_T'0) : Seq.seq t_T'0 + function seq_map'0 [#"linked_list.rs" 65 0 65 66] (s : Seq.seq (t_PtrOwn'0)) (f : Map.map (t_PtrOwn'0) t_T'0) : Seq.seq t_T'0 = [%#slinked_list31] Seq.create (Seq.length s) (Mapping.from_fn (fun (i : int) -> Map.get f (Seq.get s i))) @@ -1472,7 +1472,7 @@ module M_linked_list__qyi14323471455460008969__push_front [#"linked_list.rs" 113 use prelude.prelude.Mapping - function view'0 [#"linked_list.rs" 42 4 42 33] (self : t_List'0) : Seq.seq t_T'0 = + function view'0 [#"linked_list.rs" 46 4 46 33] (self : t_List'0) : Seq.seq t_T'0 = [%#slinked_list12] seq_map'0 (inner_logic'1 self.t_List__seq'0) (Mapping.from_fn (fun (ptr_own : t_PtrOwn'0) -> (val'0 ptr_own).t_Cell__v'0)) meta "compute_max_steps" 1000000 diff --git a/creusot/tests/should_succeed/linked_list.rs b/creusot/tests/should_succeed/linked_list.rs index 6f5de0fcb5..bcdd311e3c 100644 --- a/creusot/tests/should_succeed/linked_list.rs +++ b/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 { v: T, @@ -75,19 +79,12 @@ fn seq_map_snoc() {} impl List { #[ensures(result@ == Seq::EMPTY)] pub fn new() -> List { - 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 List { #[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;