fixed ensures clause unit type edge case

Author: AlexLB99

library/core/src/slice/mod.rs

@@ -4026,6 +4026,11 @@ impl<T> [T] {
         }
     )]
     //The following two ensures clauses guarantee that middle is of maximum size within self
+    //If U or T are ZST, then middle has size zero, so we adapt the check in that case
+    #[ensures(|(prefix, _, suffix): &(&[T], &[U], &[T])|
+        ((U::IS_ZST || T::IS_ZST) && prefix.len() == self.len()) ||                                             ((prefix.len() * size_of::<T>() < align_of::<U>()) &&
+        (suffix.len() * size_of::<T>() < size_of::<U>()))
+    )]    
     #[ensures(|(prefix, _, _): &(&[T], &[U], &[T])| prefix.len() * size_of::<T>() < align_of::<U>())]
     #[ensures(|(_, _, suffix): &(&[T], &[U], &[T])| suffix.len() * size_of::<T>() < size_of::<U>())]
     //Either align_to just returns self in the prefix, or the 3 returned slices
@@ -4166,9 +4171,12 @@ impl<T> [T] {
         }
     )]
     //The following two ensures clauses guarantee that middle is of maximum size within self
-    #[ensures(|(prefix, _, _): &(*const [T], *const [U], *const [T])| prefix.len() * size_of::<T>()
-< align_of::<U>())]
-    #[ensures(|(_, _, suffix): &(*const [T], *const [U], *const [T])| suffix.len() * size_of::<T>() < size_of::<U>())]
+    //If U or T are ZST, then middle has size zero, so we adapt the check in that case
+    #[ensures(|(prefix, _, suffix): &(&[T], &[U], &[T])|
+        ((U::IS_ZST || T::IS_ZST) && prefix.len() == self.len()) || 
+        ((prefix.len() * size_of::<T>() < align_of::<U>()) &&
+        (suffix.len() * size_of::<T>() < size_of::<U>()))
+    )]    
     //Either align_to just returns self in the prefix, or the 3 returned slices
     //should be sequential, contiguous, and have same total length as self
     #[ensures(|(prefix, middle, suffix): &(*const [T], *const [U], *const [T])|