From 03a855047f2d76f30a9733d8b5ec93899c8334e0 Mon Sep 17 00:00:00 2001 From: Dominik Stolz Date: Thu, 19 Oct 2023 19:09:17 +0200 Subject: [PATCH] Rename 05_take test to 16_take --- .../iterators/05_take/why3shapes.gz | Bin 882 -> 0 bytes .../{05_take.mlcfg => 16_take.mlcfg} | 450 +++++++++--------- .../iterators/{05_take.rs => 16_take.rs} | 0 .../{05_take => 16_take}/why3session.xml | 21 +- .../iterators/16_take/why3shapes.gz | Bin 0 -> 880 bytes 5 files changed, 236 insertions(+), 235 deletions(-) delete mode 100644 creusot/tests/should_succeed/iterators/05_take/why3shapes.gz rename creusot/tests/should_succeed/iterators/{05_take.mlcfg => 16_take.mlcfg} (57%) rename creusot/tests/should_succeed/iterators/{05_take.rs => 16_take.rs} (100%) rename creusot/tests/should_succeed/iterators/{05_take => 16_take}/why3session.xml (65%) create mode 100644 creusot/tests/should_succeed/iterators/16_take/why3shapes.gz diff --git a/creusot/tests/should_succeed/iterators/05_take/why3shapes.gz b/creusot/tests/should_succeed/iterators/05_take/why3shapes.gz deleted file mode 100644 index e40fbea48239f5e339069652e694dfa96b4df568..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 882 zcmV-&1C9J2iwFP!00000|D9D$kJ~s5z2{f>*6tJqOi`Z;%pnNIaDZYjEp%)k+fp~^ zj6HQS)Arx5zMLp&fTEj2Y*KuW)T2bdy{iuYnrC~cUhRC?PvhSeukQX@9lx3V_^RtB zzk!BkWuE70ctsXPxYxrMP$&&QuyWUyFj zAX*l2pj8f3+q9~hmEKftnyV#dH(U2uP(vu2gc5#NZZM&!5)X|}NoNG`hI<6{Ke>H-lO>r)q+D{1^v z*#%8h53%-LH@%F*;n&p*A+OqW?grtp3(NC@gkN=IyWmcvVYEMvr^|RT#b_7^Op9=9 zZ#bLv)f_Ku9s<&x(91nz+2+|6*_PMega6CZgx@L-nqB;kUF;+~N>F9Hp$5@W1&%mkOs9lky<^5!1X@zJpcVl0 ztfI$$Acl8N3`SsABlTGb2S)k`AO*m(ffH~>5!*S6t{*6+yzjW-K>9&O02YA%00-N6 I_t6Ld0CYgI1^@s6 diff --git a/creusot/tests/should_succeed/iterators/05_take.mlcfg b/creusot/tests/should_succeed/iterators/16_take.mlcfg similarity index 57% rename from creusot/tests/should_succeed/iterators/05_take.mlcfg rename to creusot/tests/should_succeed/iterators/16_take.mlcfg index f4389d5d5e..5ef9acc6a5 100644 --- a/creusot/tests/should_succeed/iterators/05_take.mlcfg +++ b/creusot/tests/should_succeed/iterators/16_take.mlcfg @@ -1,5 +1,5 @@ -module C05Take_Take_Type +module C16Take_Take_Type use prelude.Int use prelude.UIntSize type t_take 'i = @@ -36,12 +36,12 @@ module CreusotContracts_Resolve_Impl1_Resolve ensures { result = resolve self } end -module C05Take_Common_Iterator_Completed_Stub +module C16Take_Common_Iterator_Completed_Stub type self use prelude.Borrow predicate completed [#"../common.rs" 11 4 11 36] (self : borrowed self) end -module C05Take_Common_Iterator_Completed_Interface +module C16Take_Common_Iterator_Completed_Interface type self use prelude.Borrow predicate completed [#"../common.rs" 11 4 11 36] (self : borrowed self) @@ -49,7 +49,7 @@ module C05Take_Common_Iterator_Completed_Interface ensures { result = completed self } end -module C05Take_Common_Iterator_Completed +module C16Take_Common_Iterator_Completed type self use prelude.Borrow predicate completed [#"../common.rs" 11 4 11 36] (self : borrowed self) @@ -57,62 +57,62 @@ module C05Take_Common_Iterator_Completed ensures { result = completed self } end -module C05Take_Impl0_Completed_Stub +module C16Take_Impl0_Completed_Stub type i use prelude.Borrow - use C05Take_Take_Type as C05Take_Take_Type - predicate completed [#"../05_take.rs" 22 4 22 35] (self : borrowed (C05Take_Take_Type.t_take i)) + use C16Take_Take_Type as C16Take_Take_Type + predicate completed [#"../16_take.rs" 22 4 22 35] (self : borrowed (C16Take_Take_Type.t_take i)) end -module C05Take_Impl0_Completed_Interface +module C16Take_Impl0_Completed_Interface type i use prelude.Borrow - use C05Take_Take_Type as C05Take_Take_Type - predicate completed [#"../05_take.rs" 22 4 22 35] (self : borrowed (C05Take_Take_Type.t_take i)) - val completed [#"../05_take.rs" 22 4 22 35] (self : borrowed (C05Take_Take_Type.t_take i)) : bool + use C16Take_Take_Type as C16Take_Take_Type + predicate completed [#"../16_take.rs" 22 4 22 35] (self : borrowed (C16Take_Take_Type.t_take i)) + val completed [#"../16_take.rs" 22 4 22 35] (self : borrowed (C16Take_Take_Type.t_take i)) : bool ensures { result = completed self } end -module C05Take_Impl0_Completed +module C16Take_Impl0_Completed type i use prelude.Borrow use prelude.UIntSize use prelude.Int - clone C05Take_Common_Iterator_Completed_Stub as Completed0 with + clone C16Take_Common_Iterator_Completed_Stub as Completed0 with type self = i - use C05Take_Take_Type as C05Take_Take_Type + use C16Take_Take_Type as C16Take_Take_Type clone CreusotContracts_Resolve_Impl1_Resolve_Stub as Resolve0 with - type t = C05Take_Take_Type.t_take i - predicate completed [#"../05_take.rs" 22 4 22 35] (self : borrowed (C05Take_Take_Type.t_take i)) = - [#"../05_take.rs" 23 8 26 9] UIntSize.to_int (C05Take_Take_Type.take_n ( * self)) = 0 /\ Resolve0.resolve self \/ UIntSize.to_int (C05Take_Take_Type.take_n ( * self)) > 0 /\ UIntSize.to_int (C05Take_Take_Type.take_n ( * self)) = UIntSize.to_int (C05Take_Take_Type.take_n ( ^ self)) + 1 /\ Completed0.completed {current = C05Take_Take_Type.take_iter ( * self); final = C05Take_Take_Type.take_iter ( ^ self)} - val completed [#"../05_take.rs" 22 4 22 35] (self : borrowed (C05Take_Take_Type.t_take i)) : bool + type t = C16Take_Take_Type.t_take i + predicate completed [#"../16_take.rs" 22 4 22 35] (self : borrowed (C16Take_Take_Type.t_take i)) = + [#"../16_take.rs" 23 8 26 9] UIntSize.to_int (C16Take_Take_Type.take_n ( * self)) = 0 /\ Resolve0.resolve self \/ UIntSize.to_int (C16Take_Take_Type.take_n ( * self)) > 0 /\ UIntSize.to_int (C16Take_Take_Type.take_n ( * self)) = UIntSize.to_int (C16Take_Take_Type.take_n ( ^ self)) + 1 /\ Completed0.completed {current = C16Take_Take_Type.take_iter ( * self); final = C16Take_Take_Type.take_iter ( ^ self)} + val completed [#"../16_take.rs" 22 4 22 35] (self : borrowed (C16Take_Take_Type.t_take i)) : bool ensures { result = completed self } end -module C05Take_Common_Iterator_Item_Type +module C16Take_Common_Iterator_Item_Type type self type item end -module C05Take_Common_Iterator_Produces_Stub +module C16Take_Common_Iterator_Produces_Stub type self use seq.Seq - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = self predicate produces [#"../common.rs" 8 4 8 66] (self : self) (visited : Seq.seq Item0.item) (_o : self) end -module C05Take_Common_Iterator_Produces_Interface +module C16Take_Common_Iterator_Produces_Interface type self use seq.Seq - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = self predicate produces [#"../common.rs" 8 4 8 66] (self : self) (visited : Seq.seq Item0.item) (_o : self) val produces [#"../common.rs" 8 4 8 66] (self : self) (visited : Seq.seq Item0.item) (_o : self) : bool ensures { result = produces self visited _o } end -module C05Take_Common_Iterator_Produces +module C16Take_Common_Iterator_Produces type self use seq.Seq - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = self predicate produces [#"../common.rs" 8 4 8 66] (self : self) (visited : Seq.seq Item0.item) (_o : self) val produces [#"../common.rs" 8 4 8 66] (self : self) (visited : Seq.seq Item0.item) (_o : self) : bool @@ -138,24 +138,24 @@ module CreusotContracts_Invariant_Inv ensures { result = inv _x } end -module C05Take_Common_Iterator_ProducesRefl_Stub +module C16Take_Common_Iterator_ProducesRefl_Stub type self use seq.Seq - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = self - clone C05Take_Common_Iterator_Produces_Stub as Produces0 with + clone C16Take_Common_Iterator_Produces_Stub as Produces0 with type self = self, type Item0.item = Item0.item clone CreusotContracts_Invariant_Inv_Stub as Inv0 with type t = self function produces_refl [#"../common.rs" 15 4 15 30] (a : self) : () end -module C05Take_Common_Iterator_ProducesRefl_Interface +module C16Take_Common_Iterator_ProducesRefl_Interface type self use seq.Seq - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = self - clone C05Take_Common_Iterator_Produces_Stub as Produces0 with + clone C16Take_Common_Iterator_Produces_Stub as Produces0 with type self = self, type Item0.item = Item0.item clone CreusotContracts_Invariant_Inv_Stub as Inv0 with @@ -168,12 +168,12 @@ module C05Take_Common_Iterator_ProducesRefl_Interface axiom produces_refl_spec : forall a : self . ([#"../common.rs" 15 21 15 22] Inv0.inv a) -> ([#"../common.rs" 14 14 14 39] Produces0.produces a (Seq.empty ) a) end -module C05Take_Common_Iterator_ProducesRefl +module C16Take_Common_Iterator_ProducesRefl type self use seq.Seq - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = self - clone C05Take_Common_Iterator_Produces_Stub as Produces0 with + clone C16Take_Common_Iterator_Produces_Stub as Produces0 with type self = self, type Item0.item = Item0.item clone CreusotContracts_Invariant_Inv_Stub as Inv0 with @@ -186,33 +186,33 @@ module C05Take_Common_Iterator_ProducesRefl axiom produces_refl_spec : forall a : self . ([#"../common.rs" 15 21 15 22] Inv0.inv a) -> ([#"../common.rs" 14 14 14 39] Produces0.produces a (Seq.empty ) a) end -module C05Take_Common_Iterator_ProducesTrans_Stub +module C16Take_Common_Iterator_ProducesTrans_Stub type self use seq.Seq - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = self use seq.Seq clone CreusotContracts_Invariant_Inv_Stub as Inv1 with type t = Seq.seq Item0.item clone CreusotContracts_Invariant_Inv_Stub as Inv0 with type t = self - clone C05Take_Common_Iterator_Produces_Stub as Produces0 with + clone C16Take_Common_Iterator_Produces_Stub as Produces0 with type self = self, type Item0.item = Item0.item function produces_trans [#"../common.rs" 21 4 21 91] (a : self) (ab : Seq.seq Item0.item) (b : self) (bc : Seq.seq Item0.item) (c : self) : () end -module C05Take_Common_Iterator_ProducesTrans_Interface +module C16Take_Common_Iterator_ProducesTrans_Interface type self use seq.Seq - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = self use seq.Seq clone CreusotContracts_Invariant_Inv_Stub as Inv1 with type t = Seq.seq Item0.item clone CreusotContracts_Invariant_Inv_Stub as Inv0 with type t = self - clone C05Take_Common_Iterator_Produces_Stub as Produces0 with + clone C16Take_Common_Iterator_Produces_Stub as Produces0 with type self = self, type Item0.item = Item0.item function produces_trans [#"../common.rs" 21 4 21 91] (a : self) (ab : Seq.seq Item0.item) (b : self) (bc : Seq.seq Item0.item) (c : self) : () @@ -230,17 +230,17 @@ module C05Take_Common_Iterator_ProducesTrans_Interface axiom produces_trans_spec : forall a : self, ab : Seq.seq Item0.item, b : self, bc : Seq.seq Item0.item, c : self . ([#"../common.rs" 18 15 18 32] Produces0.produces a ab b) -> ([#"../common.rs" 19 15 19 32] Produces0.produces b bc c) -> ([#"../common.rs" 21 22 21 23] Inv0.inv a) -> ([#"../common.rs" 21 31 21 33] Inv1.inv ab) -> ([#"../common.rs" 21 52 21 53] Inv0.inv b) -> ([#"../common.rs" 21 61 21 63] Inv1.inv bc) -> ([#"../common.rs" 21 82 21 83] Inv0.inv c) -> ([#"../common.rs" 20 14 20 42] Produces0.produces a (Seq.(++) ab bc) c) end -module C05Take_Common_Iterator_ProducesTrans +module C16Take_Common_Iterator_ProducesTrans type self use seq.Seq - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = self use seq.Seq clone CreusotContracts_Invariant_Inv_Stub as Inv1 with type t = Seq.seq Item0.item clone CreusotContracts_Invariant_Inv_Stub as Inv0 with type t = self - clone C05Take_Common_Iterator_Produces_Stub as Produces0 with + clone C16Take_Common_Iterator_Produces_Stub as Produces0 with type self = self, type Item0.item = Item0.item function produces_trans [#"../common.rs" 21 4 21 91] (a : self) (ab : Seq.seq Item0.item) (b : self) (bc : Seq.seq Item0.item) (c : self) : () @@ -264,102 +264,102 @@ module TyInv_Trivial type t = t axiom inv_trivial : forall self : t . Inv0.inv self = true end -module C05Take_Impl0_Produces_Stub +module C16Take_Impl0_Produces_Stub type i use seq.Seq - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = i - use C05Take_Take_Type as C05Take_Take_Type - predicate produces [#"../05_take.rs" 31 4 31 64] (self : C05Take_Take_Type.t_take i) (visited : Seq.seq Item0.item) (o : C05Take_Take_Type.t_take i) + use C16Take_Take_Type as C16Take_Take_Type + predicate produces [#"../16_take.rs" 31 4 31 64] (self : C16Take_Take_Type.t_take i) (visited : Seq.seq Item0.item) (o : C16Take_Take_Type.t_take i) end -module C05Take_Impl0_Produces_Interface +module C16Take_Impl0_Produces_Interface type i use seq.Seq - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = i - use C05Take_Take_Type as C05Take_Take_Type - predicate produces [#"../05_take.rs" 31 4 31 64] (self : C05Take_Take_Type.t_take i) (visited : Seq.seq Item0.item) (o : C05Take_Take_Type.t_take i) + use C16Take_Take_Type as C16Take_Take_Type + predicate produces [#"../16_take.rs" 31 4 31 64] (self : C16Take_Take_Type.t_take i) (visited : Seq.seq Item0.item) (o : C16Take_Take_Type.t_take i) - val produces [#"../05_take.rs" 31 4 31 64] (self : C05Take_Take_Type.t_take i) (visited : Seq.seq Item0.item) (o : C05Take_Take_Type.t_take i) : bool + val produces [#"../16_take.rs" 31 4 31 64] (self : C16Take_Take_Type.t_take i) (visited : Seq.seq Item0.item) (o : C16Take_Take_Type.t_take i) : bool ensures { result = produces self visited o } end -module C05Take_Impl0_Produces +module C16Take_Impl0_Produces type i use seq.Seq use prelude.UIntSize use prelude.Int - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = i - clone C05Take_Common_Iterator_Produces_Stub as Produces0 with + clone C16Take_Common_Iterator_Produces_Stub as Produces0 with type self = i, type Item0.item = Item0.item - use C05Take_Take_Type as C05Take_Take_Type - predicate produces [#"../05_take.rs" 31 4 31 64] (self : C05Take_Take_Type.t_take i) (visited : Seq.seq Item0.item) (o : C05Take_Take_Type.t_take i) + use C16Take_Take_Type as C16Take_Take_Type + predicate produces [#"../16_take.rs" 31 4 31 64] (self : C16Take_Take_Type.t_take i) (visited : Seq.seq Item0.item) (o : C16Take_Take_Type.t_take i) = - [#"../05_take.rs" 32 8 34 9] UIntSize.to_int (C05Take_Take_Type.take_n self) = UIntSize.to_int (C05Take_Take_Type.take_n o) + Seq.length visited /\ Produces0.produces (C05Take_Take_Type.take_iter self) visited (C05Take_Take_Type.take_iter o) - val produces [#"../05_take.rs" 31 4 31 64] (self : C05Take_Take_Type.t_take i) (visited : Seq.seq Item0.item) (o : C05Take_Take_Type.t_take i) : bool + [#"../16_take.rs" 32 8 34 9] UIntSize.to_int (C16Take_Take_Type.take_n self) = UIntSize.to_int (C16Take_Take_Type.take_n o) + Seq.length visited /\ Produces0.produces (C16Take_Take_Type.take_iter self) visited (C16Take_Take_Type.take_iter o) + val produces [#"../16_take.rs" 31 4 31 64] (self : C16Take_Take_Type.t_take i) (visited : Seq.seq Item0.item) (o : C16Take_Take_Type.t_take i) : bool ensures { result = produces self visited o } end -module C05Take_Impl0_ProducesRefl_Stub +module C16Take_Impl0_ProducesRefl_Stub type i use seq.Seq - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = i - use C05Take_Take_Type as C05Take_Take_Type - clone C05Take_Impl0_Produces_Stub as Produces0 with + use C16Take_Take_Type as C16Take_Take_Type + clone C16Take_Impl0_Produces_Stub as Produces0 with type i = i, type Item0.item = Item0.item clone CreusotContracts_Invariant_Inv_Stub as Inv0 with - type t = C05Take_Take_Type.t_take i - function produces_refl [#"../05_take.rs" 40 4 40 29] (a : C05Take_Take_Type.t_take i) : () + type t = C16Take_Take_Type.t_take i + function produces_refl [#"../16_take.rs" 40 4 40 29] (a : C16Take_Take_Type.t_take i) : () end -module C05Take_Impl0_ProducesRefl_Interface +module C16Take_Impl0_ProducesRefl_Interface type i use seq.Seq - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = i - use C05Take_Take_Type as C05Take_Take_Type - clone C05Take_Impl0_Produces_Stub as Produces0 with + use C16Take_Take_Type as C16Take_Take_Type + clone C16Take_Impl0_Produces_Stub as Produces0 with type i = i, type Item0.item = Item0.item clone CreusotContracts_Invariant_Inv_Stub as Inv0 with - type t = C05Take_Take_Type.t_take i - function produces_refl [#"../05_take.rs" 40 4 40 29] (a : C05Take_Take_Type.t_take i) : () - val produces_refl [#"../05_take.rs" 40 4 40 29] (a : C05Take_Take_Type.t_take i) : () - requires {[#"../05_take.rs" 40 21 40 22] Inv0.inv a} - ensures { [#"../05_take.rs" 39 14 39 39] Produces0.produces a (Seq.empty ) a } + type t = C16Take_Take_Type.t_take i + function produces_refl [#"../16_take.rs" 40 4 40 29] (a : C16Take_Take_Type.t_take i) : () + val produces_refl [#"../16_take.rs" 40 4 40 29] (a : C16Take_Take_Type.t_take i) : () + requires {[#"../16_take.rs" 40 21 40 22] Inv0.inv a} + ensures { [#"../16_take.rs" 39 14 39 39] Produces0.produces a (Seq.empty ) a } ensures { result = produces_refl a } - axiom produces_refl_spec : forall a : C05Take_Take_Type.t_take i . ([#"../05_take.rs" 40 21 40 22] Inv0.inv a) -> ([#"../05_take.rs" 39 14 39 39] Produces0.produces a (Seq.empty ) a) + axiom produces_refl_spec : forall a : C16Take_Take_Type.t_take i . ([#"../16_take.rs" 40 21 40 22] Inv0.inv a) -> ([#"../16_take.rs" 39 14 39 39] Produces0.produces a (Seq.empty ) a) end -module C05Take_Impl0_ProducesRefl +module C16Take_Impl0_ProducesRefl type i use seq.Seq - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = i - use C05Take_Take_Type as C05Take_Take_Type - clone C05Take_Impl0_Produces_Stub as Produces0 with + use C16Take_Take_Type as C16Take_Take_Type + clone C16Take_Impl0_Produces_Stub as Produces0 with type i = i, type Item0.item = Item0.item clone CreusotContracts_Invariant_Inv_Stub as Inv0 with - type t = C05Take_Take_Type.t_take i - function produces_refl [#"../05_take.rs" 40 4 40 29] (a : C05Take_Take_Type.t_take i) : () = - [#"../05_take.rs" 37 4 37 10] () - val produces_refl [#"../05_take.rs" 40 4 40 29] (a : C05Take_Take_Type.t_take i) : () - requires {[#"../05_take.rs" 40 21 40 22] Inv0.inv a} - ensures { [#"../05_take.rs" 39 14 39 39] Produces0.produces a (Seq.empty ) a } + type t = C16Take_Take_Type.t_take i + function produces_refl [#"../16_take.rs" 40 4 40 29] (a : C16Take_Take_Type.t_take i) : () = + [#"../16_take.rs" 37 4 37 10] () + val produces_refl [#"../16_take.rs" 40 4 40 29] (a : C16Take_Take_Type.t_take i) : () + requires {[#"../16_take.rs" 40 21 40 22] Inv0.inv a} + ensures { [#"../16_take.rs" 39 14 39 39] Produces0.produces a (Seq.empty ) a } ensures { result = produces_refl a } - axiom produces_refl_spec : forall a : C05Take_Take_Type.t_take i . ([#"../05_take.rs" 40 21 40 22] Inv0.inv a) -> ([#"../05_take.rs" 39 14 39 39] Produces0.produces a (Seq.empty ) a) + axiom produces_refl_spec : forall a : C16Take_Take_Type.t_take i . ([#"../16_take.rs" 40 21 40 22] Inv0.inv a) -> ([#"../16_take.rs" 39 14 39 39] Produces0.produces a (Seq.empty ) a) end -module C05Take_Impl0_ProducesRefl_Impl +module C16Take_Impl0_ProducesRefl_Impl type i use seq.Seq - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = i use seq.Seq clone CreusotContracts_Invariant_Inv_Interface as Inv2 with @@ -374,118 +374,118 @@ module C05Take_Impl0_ProducesRefl_Impl type t = i, predicate Inv0.inv = Inv1.inv, axiom . - clone C05Take_Common_Iterator_Produces_Interface as Produces1 with + clone C16Take_Common_Iterator_Produces_Interface as Produces1 with type self = i, type Item0.item = Item0.item - clone C05Take_Common_Iterator_ProducesTrans_Interface as ProducesTrans0 with + clone C16Take_Common_Iterator_ProducesTrans_Interface as ProducesTrans0 with type self = i, predicate Produces0.produces = Produces1.produces, predicate Inv0.inv = Inv1.inv, predicate Inv1.inv = Inv2.inv, type Item0.item = Item0.item, axiom . - clone C05Take_Common_Iterator_ProducesRefl_Interface as ProducesRefl0 with + clone C16Take_Common_Iterator_ProducesRefl_Interface as ProducesRefl0 with type self = i, predicate Inv0.inv = Inv1.inv, predicate Produces0.produces = Produces1.produces, type Item0.item = Item0.item, axiom . - use C05Take_Take_Type as C05Take_Take_Type + use C16Take_Take_Type as C16Take_Take_Type clone CreusotContracts_Invariant_Inv_Interface as Inv0 with - type t = C05Take_Take_Type.t_take i + type t = C16Take_Take_Type.t_take i clone TyInv_Trivial as TyInv_Trivial0 with - type t = C05Take_Take_Type.t_take i, + type t = C16Take_Take_Type.t_take i, predicate Inv0.inv = Inv0.inv, axiom . - clone C05Take_Impl0_Produces as Produces0 with + clone C16Take_Impl0_Produces as Produces0 with type i = i, type Item0.item = Item0.item, predicate Produces0.produces = Produces1.produces - let rec ghost function produces_refl [#"../05_take.rs" 40 4 40 29] (a : C05Take_Take_Type.t_take i) : () - requires {[#"../05_take.rs" 40 21 40 22] Inv0.inv a} - ensures { [#"../05_take.rs" 39 14 39 39] Produces0.produces a (Seq.empty ) a } + let rec ghost function produces_refl [#"../16_take.rs" 40 4 40 29] (a : C16Take_Take_Type.t_take i) : () + requires {[#"../16_take.rs" 40 21 40 22] Inv0.inv a} + ensures { [#"../16_take.rs" 39 14 39 39] Produces0.produces a (Seq.empty ) a } = [@vc:do_not_keep_trace] [@vc:sp] - [#"../05_take.rs" 37 4 37 10] () + [#"../16_take.rs" 37 4 37 10] () end -module C05Take_Impl0_ProducesTrans_Stub +module C16Take_Impl0_ProducesTrans_Stub type i use seq.Seq - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = i use seq.Seq - use C05Take_Take_Type as C05Take_Take_Type + use C16Take_Take_Type as C16Take_Take_Type clone CreusotContracts_Invariant_Inv_Stub as Inv1 with type t = Seq.seq Item0.item clone CreusotContracts_Invariant_Inv_Stub as Inv0 with - type t = C05Take_Take_Type.t_take i - clone C05Take_Impl0_Produces_Stub as Produces0 with + type t = C16Take_Take_Type.t_take i + clone C16Take_Impl0_Produces_Stub as Produces0 with type i = i, type Item0.item = Item0.item - function produces_trans [#"../05_take.rs" 47 4 47 90] (a : C05Take_Take_Type.t_take i) (ab : Seq.seq Item0.item) (b : C05Take_Take_Type.t_take i) (bc : Seq.seq Item0.item) (c : C05Take_Take_Type.t_take i) : () + function produces_trans [#"../16_take.rs" 47 4 47 90] (a : C16Take_Take_Type.t_take i) (ab : Seq.seq Item0.item) (b : C16Take_Take_Type.t_take i) (bc : Seq.seq Item0.item) (c : C16Take_Take_Type.t_take i) : () end -module C05Take_Impl0_ProducesTrans_Interface +module C16Take_Impl0_ProducesTrans_Interface type i use seq.Seq - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = i use seq.Seq - use C05Take_Take_Type as C05Take_Take_Type + use C16Take_Take_Type as C16Take_Take_Type clone CreusotContracts_Invariant_Inv_Stub as Inv1 with type t = Seq.seq Item0.item clone CreusotContracts_Invariant_Inv_Stub as Inv0 with - type t = C05Take_Take_Type.t_take i - clone C05Take_Impl0_Produces_Stub as Produces0 with + type t = C16Take_Take_Type.t_take i + clone C16Take_Impl0_Produces_Stub as Produces0 with type i = i, type Item0.item = Item0.item - function produces_trans [#"../05_take.rs" 47 4 47 90] (a : C05Take_Take_Type.t_take i) (ab : Seq.seq Item0.item) (b : C05Take_Take_Type.t_take i) (bc : Seq.seq Item0.item) (c : C05Take_Take_Type.t_take i) : () - - val produces_trans [#"../05_take.rs" 47 4 47 90] (a : C05Take_Take_Type.t_take i) (ab : Seq.seq Item0.item) (b : C05Take_Take_Type.t_take i) (bc : Seq.seq Item0.item) (c : C05Take_Take_Type.t_take i) : () - requires {[#"../05_take.rs" 44 15 44 32] Produces0.produces a ab b} - requires {[#"../05_take.rs" 45 15 45 32] Produces0.produces b bc c} - requires {[#"../05_take.rs" 47 22 47 23] Inv0.inv a} - requires {[#"../05_take.rs" 47 31 47 33] Inv1.inv ab} - requires {[#"../05_take.rs" 47 52 47 53] Inv0.inv b} - requires {[#"../05_take.rs" 47 61 47 63] Inv1.inv bc} - requires {[#"../05_take.rs" 47 82 47 83] Inv0.inv c} - ensures { [#"../05_take.rs" 46 14 46 42] Produces0.produces a (Seq.(++) ab bc) c } + function produces_trans [#"../16_take.rs" 47 4 47 90] (a : C16Take_Take_Type.t_take i) (ab : Seq.seq Item0.item) (b : C16Take_Take_Type.t_take i) (bc : Seq.seq Item0.item) (c : C16Take_Take_Type.t_take i) : () + + val produces_trans [#"../16_take.rs" 47 4 47 90] (a : C16Take_Take_Type.t_take i) (ab : Seq.seq Item0.item) (b : C16Take_Take_Type.t_take i) (bc : Seq.seq Item0.item) (c : C16Take_Take_Type.t_take i) : () + requires {[#"../16_take.rs" 44 15 44 32] Produces0.produces a ab b} + requires {[#"../16_take.rs" 45 15 45 32] Produces0.produces b bc c} + requires {[#"../16_take.rs" 47 22 47 23] Inv0.inv a} + requires {[#"../16_take.rs" 47 31 47 33] Inv1.inv ab} + requires {[#"../16_take.rs" 47 52 47 53] Inv0.inv b} + requires {[#"../16_take.rs" 47 61 47 63] Inv1.inv bc} + requires {[#"../16_take.rs" 47 82 47 83] Inv0.inv c} + ensures { [#"../16_take.rs" 46 14 46 42] Produces0.produces a (Seq.(++) ab bc) c } ensures { result = produces_trans a ab b bc c } - axiom produces_trans_spec : forall a : C05Take_Take_Type.t_take i, ab : Seq.seq Item0.item, b : C05Take_Take_Type.t_take i, bc : Seq.seq Item0.item, c : C05Take_Take_Type.t_take i . ([#"../05_take.rs" 44 15 44 32] Produces0.produces a ab b) -> ([#"../05_take.rs" 45 15 45 32] Produces0.produces b bc c) -> ([#"../05_take.rs" 47 22 47 23] Inv0.inv a) -> ([#"../05_take.rs" 47 31 47 33] Inv1.inv ab) -> ([#"../05_take.rs" 47 52 47 53] Inv0.inv b) -> ([#"../05_take.rs" 47 61 47 63] Inv1.inv bc) -> ([#"../05_take.rs" 47 82 47 83] Inv0.inv c) -> ([#"../05_take.rs" 46 14 46 42] Produces0.produces a (Seq.(++) ab bc) c) + axiom produces_trans_spec : forall a : C16Take_Take_Type.t_take i, ab : Seq.seq Item0.item, b : C16Take_Take_Type.t_take i, bc : Seq.seq Item0.item, c : C16Take_Take_Type.t_take i . ([#"../16_take.rs" 44 15 44 32] Produces0.produces a ab b) -> ([#"../16_take.rs" 45 15 45 32] Produces0.produces b bc c) -> ([#"../16_take.rs" 47 22 47 23] Inv0.inv a) -> ([#"../16_take.rs" 47 31 47 33] Inv1.inv ab) -> ([#"../16_take.rs" 47 52 47 53] Inv0.inv b) -> ([#"../16_take.rs" 47 61 47 63] Inv1.inv bc) -> ([#"../16_take.rs" 47 82 47 83] Inv0.inv c) -> ([#"../16_take.rs" 46 14 46 42] Produces0.produces a (Seq.(++) ab bc) c) end -module C05Take_Impl0_ProducesTrans +module C16Take_Impl0_ProducesTrans type i use seq.Seq - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = i use seq.Seq - use C05Take_Take_Type as C05Take_Take_Type + use C16Take_Take_Type as C16Take_Take_Type clone CreusotContracts_Invariant_Inv_Stub as Inv1 with type t = Seq.seq Item0.item clone CreusotContracts_Invariant_Inv_Stub as Inv0 with - type t = C05Take_Take_Type.t_take i - clone C05Take_Impl0_Produces_Stub as Produces0 with + type t = C16Take_Take_Type.t_take i + clone C16Take_Impl0_Produces_Stub as Produces0 with type i = i, type Item0.item = Item0.item - function produces_trans [#"../05_take.rs" 47 4 47 90] (a : C05Take_Take_Type.t_take i) (ab : Seq.seq Item0.item) (b : C05Take_Take_Type.t_take i) (bc : Seq.seq Item0.item) (c : C05Take_Take_Type.t_take i) : () + function produces_trans [#"../16_take.rs" 47 4 47 90] (a : C16Take_Take_Type.t_take i) (ab : Seq.seq Item0.item) (b : C16Take_Take_Type.t_take i) (bc : Seq.seq Item0.item) (c : C16Take_Take_Type.t_take i) : () = - [#"../05_take.rs" 42 4 42 10] () - val produces_trans [#"../05_take.rs" 47 4 47 90] (a : C05Take_Take_Type.t_take i) (ab : Seq.seq Item0.item) (b : C05Take_Take_Type.t_take i) (bc : Seq.seq Item0.item) (c : C05Take_Take_Type.t_take i) : () - requires {[#"../05_take.rs" 44 15 44 32] Produces0.produces a ab b} - requires {[#"../05_take.rs" 45 15 45 32] Produces0.produces b bc c} - requires {[#"../05_take.rs" 47 22 47 23] Inv0.inv a} - requires {[#"../05_take.rs" 47 31 47 33] Inv1.inv ab} - requires {[#"../05_take.rs" 47 52 47 53] Inv0.inv b} - requires {[#"../05_take.rs" 47 61 47 63] Inv1.inv bc} - requires {[#"../05_take.rs" 47 82 47 83] Inv0.inv c} - ensures { [#"../05_take.rs" 46 14 46 42] Produces0.produces a (Seq.(++) ab bc) c } + [#"../16_take.rs" 42 4 42 10] () + val produces_trans [#"../16_take.rs" 47 4 47 90] (a : C16Take_Take_Type.t_take i) (ab : Seq.seq Item0.item) (b : C16Take_Take_Type.t_take i) (bc : Seq.seq Item0.item) (c : C16Take_Take_Type.t_take i) : () + requires {[#"../16_take.rs" 44 15 44 32] Produces0.produces a ab b} + requires {[#"../16_take.rs" 45 15 45 32] Produces0.produces b bc c} + requires {[#"../16_take.rs" 47 22 47 23] Inv0.inv a} + requires {[#"../16_take.rs" 47 31 47 33] Inv1.inv ab} + requires {[#"../16_take.rs" 47 52 47 53] Inv0.inv b} + requires {[#"../16_take.rs" 47 61 47 63] Inv1.inv bc} + requires {[#"../16_take.rs" 47 82 47 83] Inv0.inv c} + ensures { [#"../16_take.rs" 46 14 46 42] Produces0.produces a (Seq.(++) ab bc) c } ensures { result = produces_trans a ab b bc c } - axiom produces_trans_spec : forall a : C05Take_Take_Type.t_take i, ab : Seq.seq Item0.item, b : C05Take_Take_Type.t_take i, bc : Seq.seq Item0.item, c : C05Take_Take_Type.t_take i . ([#"../05_take.rs" 44 15 44 32] Produces0.produces a ab b) -> ([#"../05_take.rs" 45 15 45 32] Produces0.produces b bc c) -> ([#"../05_take.rs" 47 22 47 23] Inv0.inv a) -> ([#"../05_take.rs" 47 31 47 33] Inv1.inv ab) -> ([#"../05_take.rs" 47 52 47 53] Inv0.inv b) -> ([#"../05_take.rs" 47 61 47 63] Inv1.inv bc) -> ([#"../05_take.rs" 47 82 47 83] Inv0.inv c) -> ([#"../05_take.rs" 46 14 46 42] Produces0.produces a (Seq.(++) ab bc) c) + axiom produces_trans_spec : forall a : C16Take_Take_Type.t_take i, ab : Seq.seq Item0.item, b : C16Take_Take_Type.t_take i, bc : Seq.seq Item0.item, c : C16Take_Take_Type.t_take i . ([#"../16_take.rs" 44 15 44 32] Produces0.produces a ab b) -> ([#"../16_take.rs" 45 15 45 32] Produces0.produces b bc c) -> ([#"../16_take.rs" 47 22 47 23] Inv0.inv a) -> ([#"../16_take.rs" 47 31 47 33] Inv1.inv ab) -> ([#"../16_take.rs" 47 52 47 53] Inv0.inv b) -> ([#"../16_take.rs" 47 61 47 63] Inv1.inv bc) -> ([#"../16_take.rs" 47 82 47 83] Inv0.inv c) -> ([#"../16_take.rs" 46 14 46 42] Produces0.produces a (Seq.(++) ab bc) c) end -module C05Take_Impl0_ProducesTrans_Impl +module C16Take_Impl0_ProducesTrans_Impl type i use seq.Seq clone CreusotContracts_Invariant_Inv_Interface as Inv2 with @@ -494,22 +494,22 @@ module C05Take_Impl0_ProducesTrans_Impl type t = i, predicate Inv0.inv = Inv2.inv, axiom . - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = i use seq.Seq clone CreusotContracts_Invariant_Inv_Interface as Inv1 with type t = Seq.seq Item0.item - clone C05Take_Common_Iterator_Produces_Interface as Produces1 with + clone C16Take_Common_Iterator_Produces_Interface as Produces1 with type self = i, type Item0.item = Item0.item - clone C05Take_Common_Iterator_ProducesTrans_Interface as ProducesTrans0 with + clone C16Take_Common_Iterator_ProducesTrans_Interface as ProducesTrans0 with type self = i, predicate Produces0.produces = Produces1.produces, predicate Inv0.inv = Inv2.inv, predicate Inv1.inv = Inv1.inv, type Item0.item = Item0.item, axiom . - clone C05Take_Common_Iterator_ProducesRefl_Interface as ProducesRefl0 with + clone C16Take_Common_Iterator_ProducesRefl_Interface as ProducesRefl0 with type self = i, predicate Inv0.inv = Inv2.inv, predicate Produces0.produces = Produces1.produces, @@ -519,29 +519,29 @@ module C05Take_Impl0_ProducesTrans_Impl type t = Seq.seq Item0.item, predicate Inv0.inv = Inv1.inv, axiom . - use C05Take_Take_Type as C05Take_Take_Type + use C16Take_Take_Type as C16Take_Take_Type clone CreusotContracts_Invariant_Inv_Interface as Inv0 with - type t = C05Take_Take_Type.t_take i + type t = C16Take_Take_Type.t_take i clone TyInv_Trivial as TyInv_Trivial0 with - type t = C05Take_Take_Type.t_take i, + type t = C16Take_Take_Type.t_take i, predicate Inv0.inv = Inv0.inv, axiom . - clone C05Take_Impl0_Produces as Produces0 with + clone C16Take_Impl0_Produces as Produces0 with type i = i, type Item0.item = Item0.item, predicate Produces0.produces = Produces1.produces - let rec ghost function produces_trans [#"../05_take.rs" 47 4 47 90] (a : C05Take_Take_Type.t_take i) (ab : Seq.seq Item0.item) (b : C05Take_Take_Type.t_take i) (bc : Seq.seq Item0.item) (c : C05Take_Take_Type.t_take i) : () - requires {[#"../05_take.rs" 44 15 44 32] Produces0.produces a ab b} - requires {[#"../05_take.rs" 45 15 45 32] Produces0.produces b bc c} - requires {[#"../05_take.rs" 47 22 47 23] Inv0.inv a} - requires {[#"../05_take.rs" 47 31 47 33] Inv1.inv ab} - requires {[#"../05_take.rs" 47 52 47 53] Inv0.inv b} - requires {[#"../05_take.rs" 47 61 47 63] Inv1.inv bc} - requires {[#"../05_take.rs" 47 82 47 83] Inv0.inv c} - ensures { [#"../05_take.rs" 46 14 46 42] Produces0.produces a (Seq.(++) ab bc) c } + let rec ghost function produces_trans [#"../16_take.rs" 47 4 47 90] (a : C16Take_Take_Type.t_take i) (ab : Seq.seq Item0.item) (b : C16Take_Take_Type.t_take i) (bc : Seq.seq Item0.item) (c : C16Take_Take_Type.t_take i) : () + requires {[#"../16_take.rs" 44 15 44 32] Produces0.produces a ab b} + requires {[#"../16_take.rs" 45 15 45 32] Produces0.produces b bc c} + requires {[#"../16_take.rs" 47 22 47 23] Inv0.inv a} + requires {[#"../16_take.rs" 47 31 47 33] Inv1.inv ab} + requires {[#"../16_take.rs" 47 52 47 53] Inv0.inv b} + requires {[#"../16_take.rs" 47 61 47 63] Inv1.inv bc} + requires {[#"../16_take.rs" 47 82 47 83] Inv0.inv c} + ensures { [#"../16_take.rs" 46 14 46 42] Produces0.produces a (Seq.(++) ab bc) c } = [@vc:do_not_keep_trace] [@vc:sp] - [#"../05_take.rs" 42 4 42 10] () + [#"../16_take.rs" 42 4 42 10] () end module Core_Option_Option_Type type t_option 't = @@ -549,19 +549,19 @@ module Core_Option_Option_Type | C_Some 't end -module C05Take_Common_Iterator_Next_Interface +module C16Take_Common_Iterator_Next_Interface type self use prelude.Borrow use seq.Seq - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = self use Core_Option_Option_Type as Core_Option_Option_Type clone CreusotContracts_Invariant_Inv_Stub as Inv1 with type t = Core_Option_Option_Type.t_option Item0.item - clone C05Take_Common_Iterator_Produces_Stub as Produces0 with + clone C16Take_Common_Iterator_Produces_Stub as Produces0 with type self = self, type Item0.item = Item0.item - clone C05Take_Common_Iterator_Completed_Stub as Completed0 with + clone C16Take_Common_Iterator_Completed_Stub as Completed0 with type self = self clone CreusotContracts_Invariant_Inv_Stub as Inv0 with type t = borrowed self @@ -574,39 +574,39 @@ module C05Take_Common_Iterator_Next_Interface ensures { [#"../common.rs" 27 26 27 44] Inv1.inv result } end -module C05Take_Impl0_Next_Interface +module C16Take_Impl0_Next_Interface type i use prelude.Borrow use seq.Seq - use C05Take_Take_Type as C05Take_Take_Type - clone C05Take_Common_Iterator_Item_Type as Item0 with + use C16Take_Take_Type as C16Take_Take_Type + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = i use Core_Option_Option_Type as Core_Option_Option_Type clone CreusotContracts_Invariant_Inv_Stub as Inv1 with type t = Core_Option_Option_Type.t_option Item0.item - clone C05Take_Impl0_Produces_Stub as Produces0 with + clone C16Take_Impl0_Produces_Stub as Produces0 with type i = i, type Item0.item = Item0.item - clone C05Take_Impl0_Completed_Stub as Completed0 with + clone C16Take_Impl0_Completed_Stub as Completed0 with type i = i clone CreusotContracts_Invariant_Inv_Stub as Inv0 with - type t = borrowed (C05Take_Take_Type.t_take i) - val next [#"../05_take.rs" 53 4 53 41] (self : borrowed (C05Take_Take_Type.t_take i)) : Core_Option_Option_Type.t_option Item0.item - requires {[#"../05_take.rs" 53 17 53 21] Inv0.inv self} - ensures { [#"../05_take.rs" 49 14 52 5] match (result) with + type t = borrowed (C16Take_Take_Type.t_take i) + val next [#"../16_take.rs" 53 4 53 41] (self : borrowed (C16Take_Take_Type.t_take i)) : Core_Option_Option_Type.t_option Item0.item + requires {[#"../16_take.rs" 53 17 53 21] Inv0.inv self} + ensures { [#"../16_take.rs" 49 14 52 5] match (result) with | Core_Option_Option_Type.C_None -> Completed0.completed self | Core_Option_Option_Type.C_Some v -> Produces0.produces ( * self) (Seq.singleton v) ( ^ self) end } - ensures { [#"../05_take.rs" 53 26 53 41] Inv1.inv result } + ensures { [#"../16_take.rs" 53 26 53 41] Inv1.inv result } end -module C05Take_Impl0_Next +module C16Take_Impl0_Next type i use prelude.Int use prelude.UIntSize use prelude.Borrow use seq.Seq - clone C05Take_Common_Iterator_Item_Type as Item0 with + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = i use seq.Seq clone CreusotContracts_Invariant_Inv_Interface as Inv4 with @@ -628,21 +628,21 @@ module C05Take_Impl0_Next type t = Core_Option_Option_Type.t_option Item0.item, predicate Inv0.inv = Inv2.inv, axiom . - clone C05Take_Common_Iterator_Produces_Interface as Produces1 with + clone C16Take_Common_Iterator_Produces_Interface as Produces1 with type self = i, type Item0.item = Item0.item - clone C05Take_Common_Iterator_Completed_Interface as Completed1 with + clone C16Take_Common_Iterator_Completed_Interface as Completed1 with type self = i clone CreusotContracts_Invariant_Inv_Interface as Inv1 with type t = i - clone C05Take_Common_Iterator_ProducesTrans_Interface as ProducesTrans0 with + clone C16Take_Common_Iterator_ProducesTrans_Interface as ProducesTrans0 with type self = i, predicate Produces0.produces = Produces1.produces, predicate Inv0.inv = Inv1.inv, predicate Inv1.inv = Inv4.inv, type Item0.item = Item0.item, axiom . - clone C05Take_Common_Iterator_ProducesRefl_Interface as ProducesRefl0 with + clone C16Take_Common_Iterator_ProducesRefl_Interface as ProducesRefl0 with type self = i, predicate Inv0.inv = Inv1.inv, predicate Produces0.produces = Produces1.produces, @@ -652,57 +652,57 @@ module C05Take_Impl0_Next type t = i, predicate Inv0.inv = Inv1.inv, axiom . - use C05Take_Take_Type as C05Take_Take_Type + use C16Take_Take_Type as C16Take_Take_Type clone CreusotContracts_Invariant_Inv_Interface as Inv0 with - type t = borrowed (C05Take_Take_Type.t_take i) + type t = borrowed (C16Take_Take_Type.t_take i) clone TyInv_Trivial as TyInv_Trivial0 with - type t = borrowed (C05Take_Take_Type.t_take i), + type t = borrowed (C16Take_Take_Type.t_take i), predicate Inv0.inv = Inv0.inv, axiom . - clone C05Take_Impl0_Produces as Produces0 with + clone C16Take_Impl0_Produces as Produces0 with type i = i, type Item0.item = Item0.item, predicate Produces0.produces = Produces1.produces clone CreusotContracts_Resolve_Impl1_Resolve as Resolve0 with - type t = C05Take_Take_Type.t_take i - clone C05Take_Impl0_Completed as Completed0 with + type t = C16Take_Take_Type.t_take i + clone C16Take_Impl0_Completed as Completed0 with type i = i, predicate Resolve0.resolve = Resolve0.resolve, predicate Completed0.completed = Completed1.completed - clone C05Take_Common_Iterator_Next_Interface as Next0 with + clone C16Take_Common_Iterator_Next_Interface as Next0 with type self = i, predicate Inv0.inv = Inv3.inv, type Item0.item = Item0.item, predicate Completed0.completed = Completed1.completed, predicate Produces0.produces = Produces1.produces, predicate Inv1.inv = Inv2.inv - let rec cfg next [#"../05_take.rs" 53 4 53 41] [@cfg:stackify] [@cfg:subregion_analysis] (self : borrowed (C05Take_Take_Type.t_take i)) : Core_Option_Option_Type.t_option Item0.item - requires {[#"../05_take.rs" 53 17 53 21] Inv0.inv self} - ensures { [#"../05_take.rs" 49 14 52 5] match (result) with + let rec cfg next [#"../16_take.rs" 53 4 53 41] [@cfg:stackify] [@cfg:subregion_analysis] (self : borrowed (C16Take_Take_Type.t_take i)) : Core_Option_Option_Type.t_option Item0.item + requires {[#"../16_take.rs" 53 17 53 21] Inv0.inv self} + ensures { [#"../16_take.rs" 49 14 52 5] match (result) with | Core_Option_Option_Type.C_None -> Completed0.completed self | Core_Option_Option_Type.C_Some v -> Produces0.produces ( * self) (Seq.singleton v) ( ^ self) end } - ensures { [#"../05_take.rs" 53 26 53 41] Inv2.inv result } + ensures { [#"../16_take.rs" 53 26 53 41] Inv2.inv result } = [@vc:do_not_keep_trace] [@vc:sp] var _0 : Core_Option_Option_Type.t_option Item0.item; - var self : borrowed (C05Take_Take_Type.t_take i) = self; + var self : borrowed (C16Take_Take_Type.t_take i) = self; var _5 : borrowed i; { goto BB0 } BB0 { - switch ([#"../05_take.rs" 54 11 54 22] C05Take_Take_Type.take_n ( * self) <> ([#"../05_take.rs" 54 21 54 22] (0 : usize))) + switch ([#"../16_take.rs" 54 11 54 22] C16Take_Take_Type.take_n ( * self) <> ([#"../16_take.rs" 54 21 54 22] (0 : usize))) | False -> goto BB3 | True -> goto BB1 end } BB1 { - self <- { self with current = (let C05Take_Take_Type.C_Take a b = * self in C05Take_Take_Type.C_Take a ([#"../05_take.rs" 55 12 55 23] C05Take_Take_Type.take_n ( * self) - ([#"../05_take.rs" 55 22 55 23] (1 : usize)))) }; - _5 <- Borrow.borrow_mut (C05Take_Take_Type.take_iter ( * self)); - self <- { self with current = (let C05Take_Take_Type.C_Take a b = * self in C05Take_Take_Type.C_Take ( ^ _5) b) }; + self <- { self with current = (let C16Take_Take_Type.C_Take a b = * self in C16Take_Take_Type.C_Take a ([#"../16_take.rs" 55 12 55 23] C16Take_Take_Type.take_n ( * self) - ([#"../16_take.rs" 55 22 55 23] (1 : usize)))) }; + _5 <- Borrow.borrow_mut (C16Take_Take_Type.take_iter ( * self)); + self <- { self with current = (let C16Take_Take_Type.C_Take a b = * self in C16Take_Take_Type.C_Take ( ^ _5) b) }; assume { Inv1.inv ( ^ _5) }; - _0 <- ([#"../05_take.rs" 56 12 56 28] Next0.next _5); + _0 <- ([#"../16_take.rs" 56 12 56 28] Next0.next _5); _5 <- any borrowed i; goto BB2 } @@ -722,63 +722,63 @@ module C05Take_Impl0_Next } end -module C05Take_Impl0 +module C16Take_Impl0 type i - use seq.Seq use prelude.Borrow - clone C05Take_Common_Iterator_Completed_Interface as Completed1 with - type self = i - use C05Take_Take_Type as C05Take_Take_Type - clone CreusotContracts_Resolve_Impl1_Resolve as Resolve0 with - type t = C05Take_Take_Type.t_take i - clone C05Take_Common_Iterator_Item_Type as Item0 with + use seq.Seq + clone C16Take_Common_Iterator_Item_Type as Item0 with type self = i - use Core_Option_Option_Type as Core_Option_Option_Type + use seq.Seq clone CreusotContracts_Invariant_Inv_Interface as Inv3 with - type t = Core_Option_Option_Type.t_option Item0.item + type t = Seq.seq Item0.item clone TyInv_Trivial as TyInv_Trivial3 with - type t = Core_Option_Option_Type.t_option Item0.item, + type t = Seq.seq Item0.item, predicate Inv0.inv = Inv3.inv, axiom . + use C16Take_Take_Type as C16Take_Take_Type clone CreusotContracts_Invariant_Inv_Interface as Inv2 with - type t = borrowed (C05Take_Take_Type.t_take i) + type t = C16Take_Take_Type.t_take i clone TyInv_Trivial as TyInv_Trivial2 with - type t = borrowed (C05Take_Take_Type.t_take i), + type t = C16Take_Take_Type.t_take i, predicate Inv0.inv = Inv2.inv, axiom . - clone C05Take_Common_Iterator_Produces_Interface as Produces1 with + clone C16Take_Common_Iterator_Produces_Interface as Produces1 with type self = i, type Item0.item = Item0.item - use seq.Seq + clone C16Take_Common_Iterator_Completed_Interface as Completed1 with + type self = i + clone CreusotContracts_Resolve_Impl1_Resolve as Resolve0 with + type t = C16Take_Take_Type.t_take i + use Core_Option_Option_Type as Core_Option_Option_Type clone CreusotContracts_Invariant_Inv_Interface as Inv1 with - type t = Seq.seq Item0.item + type t = Core_Option_Option_Type.t_option Item0.item clone TyInv_Trivial as TyInv_Trivial1 with - type t = Seq.seq Item0.item, + type t = Core_Option_Option_Type.t_option Item0.item, predicate Inv0.inv = Inv1.inv, axiom . clone CreusotContracts_Invariant_Inv_Interface as Inv0 with - type t = C05Take_Take_Type.t_take i + type t = borrowed (C16Take_Take_Type.t_take i) clone TyInv_Trivial as TyInv_Trivial0 with - type t = C05Take_Take_Type.t_take i, + type t = borrowed (C16Take_Take_Type.t_take i), predicate Inv0.inv = Inv0.inv, axiom . - clone C05Take_Common_Iterator_Item_Type as Item1 with - type self = C05Take_Take_Type.t_take i - clone C05Take_Impl0_Completed as Completed0 with - type i = i, - predicate Resolve0.resolve = Resolve0.resolve, - predicate Completed0.completed = Completed1.completed - clone C05Take_Impl0_Produces as Produces0 with + clone C16Take_Common_Iterator_Item_Type as Item1 with + type self = C16Take_Take_Type.t_take i + clone C16Take_Impl0_Produces as Produces0 with type i = i, type Item0.item = Item0.item, predicate Produces0.produces = Produces1.produces - goal produces_trans_refn : [#"../05_take.rs" 47 4 47 90] forall a : C05Take_Take_Type.t_take i . forall ab : Seq.seq Item0.item . forall b : C05Take_Take_Type.t_take i . forall bc : Seq.seq Item0.item . forall c : C05Take_Take_Type.t_take i . Inv0.inv c /\ Inv1.inv bc /\ Inv0.inv b /\ Inv1.inv ab /\ Inv0.inv a /\ Produces0.produces b bc c /\ Produces0.produces a ab b -> Inv0.inv c /\ Inv1.inv bc /\ Inv0.inv b /\ Inv1.inv ab /\ Inv0.inv a /\ Produces0.produces b bc c /\ Produces0.produces a ab b /\ (forall result : () . Produces0.produces a (Seq.(++) ab bc) c -> Produces0.produces a (Seq.(++) ab bc) c) - goal produces_refl_refn : [#"../05_take.rs" 40 4 40 29] forall a : C05Take_Take_Type.t_take i . Inv0.inv a -> Inv0.inv a /\ (forall result : () . Produces0.produces a (Seq.empty ) a -> Produces0.produces a (Seq.empty ) a) - goal next_refn : [#"../05_take.rs" 53 4 53 41] forall self : borrowed (C05Take_Take_Type.t_take i) . Inv2.inv self -> Inv2.inv self /\ (forall result : Core_Option_Option_Type.t_option Item0.item . Inv3.inv result /\ match (result) with + clone C16Take_Impl0_Completed as Completed0 with + type i = i, + predicate Resolve0.resolve = Resolve0.resolve, + predicate Completed0.completed = Completed1.completed + goal next_refn : [#"../16_take.rs" 53 4 53 41] forall self : borrowed (C16Take_Take_Type.t_take i) . Inv0.inv self -> Inv0.inv self /\ (forall result : Core_Option_Option_Type.t_option Item0.item . Inv1.inv result /\ match (result) with | Core_Option_Option_Type.C_None -> Completed0.completed self | Core_Option_Option_Type.C_Some v -> Produces0.produces ( * self) (Seq.singleton v) ( ^ self) - end -> Inv3.inv result /\ match (result) with + end -> Inv1.inv result /\ match (result) with | Core_Option_Option_Type.C_None -> Completed0.completed self | Core_Option_Option_Type.C_Some v -> Produces0.produces ( * self) (Seq.singleton v) ( ^ self) end) + goal produces_refl_refn : [#"../16_take.rs" 40 4 40 29] forall a : C16Take_Take_Type.t_take i . Inv2.inv a -> Inv2.inv a /\ (forall result : () . Produces0.produces a (Seq.empty ) a -> Produces0.produces a (Seq.empty ) a) + goal produces_trans_refn : [#"../16_take.rs" 47 4 47 90] forall a : C16Take_Take_Type.t_take i . forall ab : Seq.seq Item0.item . forall b : C16Take_Take_Type.t_take i . forall bc : Seq.seq Item0.item . forall c : C16Take_Take_Type.t_take i . Inv2.inv c /\ Inv3.inv bc /\ Inv2.inv b /\ Inv3.inv ab /\ Inv2.inv a /\ Produces0.produces b bc c /\ Produces0.produces a ab b -> Inv2.inv c /\ Inv3.inv bc /\ Inv2.inv b /\ Inv3.inv ab /\ Inv2.inv a /\ Produces0.produces b bc c /\ Produces0.produces a ab b /\ (forall result : () . Produces0.produces a (Seq.(++) ab bc) c -> Produces0.produces a (Seq.(++) ab bc) c) end diff --git a/creusot/tests/should_succeed/iterators/05_take.rs b/creusot/tests/should_succeed/iterators/16_take.rs similarity index 100% rename from creusot/tests/should_succeed/iterators/05_take.rs rename to creusot/tests/should_succeed/iterators/16_take.rs diff --git a/creusot/tests/should_succeed/iterators/05_take/why3session.xml b/creusot/tests/should_succeed/iterators/16_take/why3session.xml similarity index 65% rename from creusot/tests/should_succeed/iterators/05_take/why3session.xml rename to creusot/tests/should_succeed/iterators/16_take/why3session.xml index edee7a7218..ca91def847 100644 --- a/creusot/tests/should_succeed/iterators/05_take/why3session.xml +++ b/creusot/tests/should_succeed/iterators/16_take/why3session.xml @@ -2,33 +2,34 @@ + - - + + - + - + - - - + + + - + - - + + diff --git a/creusot/tests/should_succeed/iterators/16_take/why3shapes.gz b/creusot/tests/should_succeed/iterators/16_take/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..d1e1dccf889ef85be13ed244bc313fac222b0755 GIT binary patch literal 880 zcmV-$1CRV4iwFP!00000|D9D$kK;BBz2{f>w(Tqmh@w6V%pn+z;Q&Q1Ep*&Kv86WH z8GD*!rtQBkEy;#3se}NIgpQcMr|+cmEcS%||#K_tW@eqnd~BSEoPxe*AE( zEpOnUUHP}eG`#oW=(zv<*`bq8ZSrby%LYHsbr>)YvXrwdpw zHE?IDIB>QE+D%@y?aDnhaXK_h%=QrCOGOQH*?cbH-^!g$sH(&ax-iXk*Hx=hOc6p| zgwr=gQwhKva0gfl2V578`MP*u@v!2t>xu**<7=NytnjS{r-L7lX9;;-G|t5cr;65C zo@Eob$Rvu1l>joMt_7;OO%cQtuvrwrxl#F5P|bwNTjuL0-%qb^FX0ph+KGSK{ydH0 zvPJ(edyo6^Hwu|X+Q0vj<9?Z5gCmB`{^`jd!f|@}2##k}MS6Lh1>>TKNiS6{>Lt5P zM!Cp&$;Bn*N?|z{7te_clY8dp=y%iMF#Q>ZPp@Ao@K^seq*ceckNeTTI55v;!MS-i zCIP8!me?L=kM$>7-R@7}kOH1l>E;f#1L;67#E=Ny_v1;4PxL=8{ZQGNc1#lXa9sr? zb&3M(vwr0aiV`6Dw9Wasxk*K?pXvnddhSEQA|0hihsL39%V|e_Ek5EM@yU4+A1&#a z!m{|pRjvo-D}-r1Wm5OMfOL9g5euQM_m7Z(6u{d}>H_ksE>L`mfO}ow+95l4p}moY zmg+7zZhJ_zZ+FxCI2^xSy%O@KO_y$PmAbGzuSnEQH#Q6IJQ~LE*Xev2X^PeNPTXmR zsCuDDOmXgnEEh^{{tJh`&ykyo=W#<{g)~C8=?hhj7Ewlv*xd0gM?);Ly}d%xz>`kT zQ|XSgUEh4CDqGC~3->yIK8mTbsf%fDzjptRrJaAPRb;|i48cUuMtG%o^oki2Aqwy@ zG^&%G=&<7*bZiw6rD3u+OhiQ^DMrhLA3Smt7R{~!=ztNxcBaz=@FB2(HX7WSsFXr2 zRX;?lrLo!~G+;W=9jFdu2ciS)prqRI9+dQK=S@&C0t2Zn=UVX~WAF`!j