@@ -4028,9 +4028,11 @@ impl<T> [T] {
40284028 //The following two ensures clauses guarantee that middle is of maximum size within self
40294029 //If U or T are ZST, then middle has size zero, so we adapt the check in that case
40304030 #[ ensures( |( prefix, _, suffix) : & ( & [ T ] , & [ U ] , & [ T ] ) |
4031- ( ( U :: IS_ZST || T :: IS_ZST ) && prefix. len( ) == self . len( ) ) || ( ( prefix. len( ) * size_of:: <T >( ) < align_of:: <U >( ) ) &&
4032- ( suffix. len( ) * size_of:: <T >( ) < size_of:: <U >( ) ) )
4033- ) ]
4031+ ( ( U :: IS_ZST || T :: IS_ZST ) && prefix. len( ) == self . len( ) ) || (
4032+ ( prefix. len( ) * size_of:: <T >( ) < align_of:: <U >( ) ) &&
4033+ ( suffix. len( ) * size_of:: <T >( ) < size_of:: <U >( ) )
4034+ )
4035+ ) ]
40344036 //Either align_to just returns self in the prefix, or the 3 returned slices
40354037 //should be sequential, contiguous, and have same total length as self
40364038 #[ ensures( |( prefix, middle, suffix) : & ( & [ T ] , & [ U ] , & [ T ] ) |
@@ -4171,10 +4173,11 @@ impl<T> [T] {
41714173 //The following two ensures clauses guarantee that middle is of maximum size within self
41724174 //If U or T are ZST, then middle has size zero, so we adapt the check in that case
41734175 #[ ensures( |( prefix, _, suffix) : & ( * const [ T ] , * const [ U ] , * const [ T ] ) |
4174- ( ( U :: IS_ZST || T :: IS_ZST ) && prefix. len( ) == self . len( ) ) ||
4175- ( ( prefix. len( ) * size_of:: <T >( ) < align_of:: <U >( ) ) &&
4176- ( suffix. len( ) * size_of:: <T >( ) < size_of:: <U >( ) ) )
4177- ) ]
4176+ ( ( U :: IS_ZST || T :: IS_ZST ) && prefix. len( ) == self . len( ) ) || (
4177+ ( prefix. len( ) * size_of:: <T >( ) < align_of:: <U >( ) ) &&
4178+ ( suffix. len( ) * size_of:: <T >( ) < size_of:: <U >( ) )
4179+ )
4180+ ) ]
41784181 //Either align_to just returns self in the prefix, or the 3 returned slices
41794182 //should be sequential, contiguous, and have same total length as self
41804183 #[ ensures( |( prefix, middle, suffix) : & ( * const [ T ] , * const [ U ] , * const [ T ] ) |
0 commit comments