Rollup merge of #125342 - tbu-:pr_doc_write, r=ChrisDenton · model-checking/verify-rust-std@8883bcf (original) (raw)
`@@ -767,11 +767,33 @@ fn buffer_capacity_required(mut file: &File) -> Option {
`
767
767
``
768
768
`#[stable(feature = "rust1", since = "1.0.0")]
`
769
769
`impl Read for &File {
`
``
770
`+
/// Read some bytes from the file.
`
``
771
`+
///
`
``
772
`` +
/// See [Read::read] docs for more info.
``
``
773
`+
///
`
``
774
`+
/// # Platform-specific behavior
`
``
775
`+
///
`
``
776
`` +
/// This function currently corresponds to the read function on Unix and
``
``
777
`` +
/// the NtReadFile function on Windows. Note that this [may change in
``
``
778
`+
/// the future][changes].
`
``
779
`+
///
`
``
780
`+
/// [changes]: io#platform-specific-behavior
`
770
781
`#[inline]
`
771
782
`fn read(&mut self, buf: &mut [u8]) -> io::Result {
`
772
783
`self.inner.read(buf)
`
773
784
`}
`
774
785
``
``
786
`` +
/// Like read, except that it reads into a slice of buffers.
``
``
787
`+
///
`
``
788
`` +
/// See [Read::read_vectored] docs for more info.
``
``
789
`+
///
`
``
790
`+
/// # Platform-specific behavior
`
``
791
`+
///
`
``
792
`` +
/// This function currently corresponds to the readv function on Unix and
``
``
793
`` +
/// falls back to the read implementation on Windows. Note that this
``
``
794
`+
/// [may change in the future][changes].
`
``
795
`+
///
`
``
796
`+
/// [changes]: io#platform-specific-behavior
`
775
797
`#[inline]
`
776
798
`fn read_vectored(&mut self, bufs: &mut [IoSliceMut<'_>]) -> io::Result {
`
777
799
`self.inner.read_vectored(bufs)
`
`@@ -782,6 +804,16 @@ impl Read for &File {
`
782
804
`self.inner.read_buf(cursor)
`
783
805
`}
`
784
806
``
``
807
`` +
/// Determines if File has an efficient read_vectored implementation.
``
``
808
`+
///
`
``
809
`` +
/// See [Read::is_read_vectored] docs for more info.
``
``
810
`+
///
`
``
811
`+
/// # Platform-specific behavior
`
``
812
`+
///
`
``
813
`` +
/// This function currently returns true on Unix an false on Windows.
``
``
814
`+
/// Note that this [may change in the future][changes].
`
``
815
`+
///
`
``
816
`+
/// [changes]: io#platform-specific-behavior
`
785
817
`#[inline]
`
786
818
`fn is_read_vectored(&self) -> bool {
`
787
819
`self.inner.is_read_vectored()
`
`@@ -803,19 +835,63 @@ impl Read for &File {
`
803
835
`}
`
804
836
`#[stable(feature = "rust1", since = "1.0.0")]
`
805
837
`impl Write for &File {
`
``
838
`+
/// Write some bytes from the file.
`
``
839
`+
///
`
``
840
`` +
/// See [Write::write] docs for more info.
``
``
841
`+
///
`
``
842
`+
/// # Platform-specific behavior
`
``
843
`+
///
`
``
844
`` +
/// This function currently corresponds to the write function on Unix and
``
``
845
`` +
/// the NtWriteFile function on Windows. Note that this [may change in
``
``
846
`+
/// the future][changes].
`
``
847
`+
///
`
``
848
`+
/// [changes]: io#platform-specific-behavior
`
806
849
`fn write(&mut self, buf: &[u8]) -> io::Result {
`
807
850
`self.inner.write(buf)
`
808
851
`}
`
809
852
``
``
853
`` +
/// Like write, except that it writes into a slice of buffers.
``
``
854
`+
///
`
``
855
`` +
/// See [Write::write_vectored] docs for more info.
``
``
856
`+
///
`
``
857
`+
/// # Platform-specific behavior
`
``
858
`+
///
`
``
859
`` +
/// This function currently corresponds to the writev function on Unix
``
``
860
`` +
/// and falls back to the write implementation on Windows. Note that this
``
``
861
`+
/// [may change in the future][changes].
`
``
862
`+
///
`
``
863
`+
/// [changes]: io#platform-specific-behavior
`
810
864
`fn write_vectored(&mut self, bufs: &[IoSlice<'_>]) -> io::Result {
`
811
865
`self.inner.write_vectored(bufs)
`
812
866
`}
`
813
867
``
``
868
`` +
/// Determines if File has an efficient write_vectored implementation.
``
``
869
`+
///
`
``
870
`` +
/// See [Write::is_write_vectored] docs for more info.
``
``
871
`+
///
`
``
872
`+
/// # Platform-specific behavior
`
``
873
`+
///
`
``
874
`` +
/// This function currently returns true on Unix an false on Windows.
``
``
875
`+
/// Note that this [may change in the future][changes].
`
``
876
`+
///
`
``
877
`+
/// [changes]: io#platform-specific-behavior
`
814
878
`#[inline]
`
815
879
`fn is_write_vectored(&self) -> bool {
`
816
880
`self.inner.is_write_vectored()
`
817
881
`}
`
818
882
``
``
883
`+
/// Flushes the file, ensuring that all intermediately buffered contents
`
``
884
`+
/// reach their destination.
`
``
885
`+
///
`
``
886
`` +
/// See [Write::flush] docs for more info.
``
``
887
`+
///
`
``
888
`+
/// # Platform-specific behavior
`
``
889
`+
///
`
``
890
`` +
/// Since a File structure doesn't contain any buffers, this function is
``
``
891
`+
/// currently a no-op on Unix and Windows. Note that this [may change in
`
``
892
`+
/// the future][changes].
`
``
893
`+
///
`
``
894
`+
/// [changes]: io#platform-specific-behavior
`
819
895
`#[inline]
`
820
896
`fn flush(&mut self) -> io::Result<()> {
`
821
897
`self.inner.flush()
`