[m-rev.] for review: make binary_{input, output}_stream_offset abort on overflow

[Julien Fischer]

For review by anyone.

----------------------------

Make binary_{input,output}_stream_offset abort on overflow.

Make binary{input,output}_stream_offset abort with an exception if the offset
they return cannot be respresented using Mercury's int type.  The current
impelmentation just silently casts the offset to an int.

library/io.m:
     As above.

     Document the new behaviour and direct users to the versions of these
     predicates that use 64-bit offsets.

Julien.


diff --git a/library/io.m b/library/io.m
index 8c1054c..a70c757 100644
--- a/library/io.m
+++ b/library/io.m
@@ -1367,6 +1367,9 @@
      int64::in, io::di, io::uo) is det.

      % Returns the offset (in bytes) into the specified binary output stream.
+    % Throws an exception if the offset is outside the range that can be
+    % represented by the int type; the 64-bit version below should be used in
+    % that case.
      %
  :- pred binary_output_stream_offset(io.binary_output_stream::in, int::out,
      io::di, io::uo) is det.
@@ -1449,6 +1452,9 @@
      int64::in, io::di, io::uo) is det.

      % Returns the offset (in bytes) into the specified binary input stream.
+    % Throws an exception if the offset is outside the range that can be
+    % represented by the int type; the 64-bit version below should be used in
+    % that case.
      %
  :- pred binary_input_stream_offset(io.binary_input_stream::in, int::out,
      io::di, io::uo) is det.
@@ -9463,12 +9469,20 @@ seek_binary_output64(binary_output_stream(Stream), Whence, Offset, !IO) :-
  binary_input_stream_offset(binary_input_stream(Stream), Offset, !IO) :-
      binary_stream_offset_2(Stream, Offset64, Error, !IO),
      throw_on_error(Error, "error getting file offset: ", !IO),
-    Offset = int64.cast_to_int(Offset64).
+    ( if int64.to_int(Offset64, OffsetPrime) then
+        Offset = OffsetPrime
+    else
+        error("io.binary_input_stream_offset: offset exceeds range of an int")
+    ).

  binary_output_stream_offset(binary_output_stream(Stream), Offset, !IO) :-
      binary_stream_offset_2(Stream, Offset64, Error, !IO),
      throw_on_error(Error, "error getting file offset: ", !IO),
-    Offset = int64.cast_to_int(Offset64).
+    ( if int64.to_int(Offset64, OffsetPrime) then
+        Offset = OffsetPrime
+    else
+        error("io.binary_output_stream_offset: offset exceeds range of an int")
+    ).

  binary_input_stream_offset64(binary_input_stream(Stream), Offset, !IO) :-
      binary_stream_offset_2(Stream, Offset, Error, !IO),