@@ -4031,8 +4031,6 @@ impl<T> [T] {
40314031 ( ( U :: IS_ZST || T :: IS_ZST ) && prefix. len( ) == self . len( ) ) || ( ( prefix. len( ) * size_of:: <T >( ) < align_of:: <U >( ) ) &&
40324032 ( suffix. len( ) * size_of:: <T >( ) < size_of:: <U >( ) ) )
40334033 ) ]
4034- #[ ensures( |( prefix, _, _) : & ( & [ T ] , & [ U ] , & [ T ] ) | prefix. len( ) * size_of:: <T >( ) < align_of:: <U >( ) ) ]
4035- #[ ensures( |( _, _, suffix) : & ( & [ T ] , & [ U ] , & [ T ] ) | suffix. len( ) * size_of:: <T >( ) < size_of:: <U >( ) ) ]
40364034 //Either align_to just returns self in the prefix, or the 3 returned slices
40374035 //should be sequential, contiguous, and have same total length as self
40384036 #[ ensures( |( prefix, middle, suffix) : & ( & [ T ] , & [ U ] , & [ T ] ) |
@@ -4172,7 +4170,7 @@ impl<T> [T] {
41724170 ) ]
41734171 //The following two ensures clauses guarantee that middle is of maximum size within self
41744172 //If U or T are ZST, then middle has size zero, so we adapt the check in that case
4175- #[ ensures( |( prefix, _, suffix) : & ( & [ T ] , & [ U ] , & [ T ] ) |
4173+ #[ ensures( |( prefix, _, suffix) : & ( * const [ T ] , * const [ U ] , * const [ T ] ) |
41764174 ( ( U :: IS_ZST || T :: IS_ZST ) && prefix. len( ) == self . len( ) ) ||
41774175 ( ( prefix. len( ) * size_of:: <T >( ) < align_of:: <U >( ) ) &&
41784176 ( suffix. len( ) * size_of:: <T >( ) < size_of:: <U >( ) ) )
0 commit comments