From 5df7ada68a507d77536dde24f5fb99d98dc92ae2 Mon Sep 17 00:00:00 2001 From: Pat Rogers Date: Tue, 27 Feb 2024 13:35:41 -0600 Subject: [PATCH] Add new function As_String, corresponding to toString() in C++ version. Added for completeness. Make explicit the bounds for the result of Raw_String via postcondition, for the sake of documenting them. This is an inline function expression so the change is not required for proof. --- .../ada/avtas/lmcp/avtas-lmcp-bytebuffers.adb | 44 +++++++++++++++++++ .../ada/avtas/lmcp/avtas-lmcp-bytebuffers.ads | 30 ++++++++++--- 2 files changed, 69 insertions(+), 5 deletions(-) diff --git a/src/templates/ada/avtas/lmcp/avtas-lmcp-bytebuffers.adb b/src/templates/ada/avtas/lmcp/avtas-lmcp-bytebuffers.adb index 4091c9a..f561f36 100644 --- a/src/templates/ada/avtas/lmcp/avtas-lmcp-bytebuffers.adb +++ b/src/templates/ada/avtas/lmcp/avtas-lmcp-bytebuffers.adb @@ -21,6 +21,50 @@ is return Result; end Raw_Bytes_As_String; + --------------- + -- As_String -- + --------------- + + function As_String (This : ByteBuffer) return String is + Result : Unbounded_String; + Hex_Digit : constant array (Byte range 0 .. 15) of Character := "0123456789ABCDEF"; + Nibble_Size : constant := 4; -- bits + Nibble : Byte; + begin + for K in This.Content'First .. This.Highest_Write_Pos - 1 loop + declare + Next_Byte : constant Byte := This.Content (K); + begin + Nibble := Shift_Right (Next_Byte and 2#1111_0000#, Nibble_Size); + Append (Result, Hex_Digit (Nibble)); + Nibble := Next_Byte and 2#0000_1111#; + Append (Result, Hex_Digit (Nibble)); + + if K mod 4 = 3 then + Append (Result, ASCII.LF); + -- Hence every fourth byte in Content is followed by a linefeed + -- in the resulting string, instead of a blank + else + Append (Result, ' '); + -- Otherwise, every two characters, representing one byte in + -- Content, has a blank following them in the resulting string + end if; + + pragma Loop_Invariant + (Length (Result) = Length (Result'Loop_Entry) + Natural (3 * (K + 1))); + -- Every iteration adds three characters to the string. But + -- remember K starts at 0, hence the expression above. + + pragma Loop_Invariant + (for all J in 1 .. Length (Result) => + (if J mod 3 = 0 then + (Element (Result, J) = (if J mod 12 = 0 then ASCII.LF else ' ')))); + end; + end loop; + Append (Result, ASCII.LF); + return To_String (Result); + end As_String; + ------------ -- Rewind -- ------------ diff --git a/src/templates/ada/avtas/lmcp/avtas-lmcp-bytebuffers.ads b/src/templates/ada/avtas/lmcp/avtas-lmcp-bytebuffers.ads index b885a65..4d9f423 100644 --- a/src/templates/ada/avtas/lmcp/avtas-lmcp-bytebuffers.ads +++ b/src/templates/ada/avtas/lmcp/avtas-lmcp-bytebuffers.ads @@ -441,20 +441,40 @@ is New_Content_Equal (This, Position (This)'Old, Value) and then Prior_Content_Unchanged (This, Old_Value => This'Old); - function Raw_Bytes (This : ByteBuffer) return Byte_Array; - -- Returns the entire internal byte array content, up to but not including - -- High_Water_Mark (This) + function Raw_Bytes (This : ByteBuffer) return Byte_Array with + Post => Raw_Bytes'Result'First = 0 and then + Raw_Bytes'Result'Length = High_Water_Mark (This); + -- Returns the internal byte array content function Raw_Bytes_As_String (This : ByteBuffer) return String with Pre => High_Water_Mark (This) <= Index (Positive'Last), Post => Raw_Bytes_As_String'Result'First = 1 and then Raw_Bytes_As_String'Result'Length = High_Water_Mark (This); - -- Returns the entire internal byte array content, as a String + -- Same as Raw_Bytes, except as a String value (and hence with bounds + -- consistent with String's requirements). There is no formatting, + -- unlike the result of function As_String. + + function As_String (This : ByteBuffer) return String with + Pre => (High_Water_Mark (This) * 3) + 1 <= Index'Last and then + (High_Water_Mark (This) * 3) + 1 <= Index (Positive'Last), + Post => As_String'Result'First = 1 and then + As_String'Result'Length = (High_Water_Mark (This) * 3) + 1 and then + (for all K in As_String'Result'Range => + (if K mod 3 = 0 then + As_String'Result (K) = (if K mod 12 = 0 then ASCII.LF else ' '))) + and then + As_String'Result (As_String'Result'Last) = ASCII.LF; + -- Returns the internal byte array content as a formatted String value. + -- Each internal byte is represented as two numeric hex characters, with an + -- additional blank or linefeed inserted after these two characters. Hence + -- there are three characters in the result per contained byte in This. + -- After the fourth set of two bytes, a linefeed is inserted instead of + -- a blank. This is function toString() in the C++ version. function Checksum (This : ByteBuffer; Last : Index) return UInt32 with Pre => Last <= High_Water_Mark (This) - 1; -- Computes the checksum of the slice of the internal byte array from the - -- first byte up to Last (inclusive). + -- first byte up to Last (inclusive). subtype Two_Bytes is Byte_Array (0 .. 1) with Object_Size => 16; subtype Four_Bytes is Byte_Array (0 .. 3) with Object_Size => 32;