diff --git a/examples/apps/ping/src/basalt-strings.adb b/examples/apps/ping/src/basalt-strings.adb deleted file mode 100644 index 19a3f9c20..000000000 --- a/examples/apps/ping/src/basalt-strings.adb +++ /dev/null @@ -1,75 +0,0 @@ --- --- @summary String operations for common types --- @author Johannes Kliemann --- @date 2019-11-19 --- --- Copyright (C) 2019 Componolit GmbH --- --- This file is part of Basalt, which is distributed under the terms of the --- GNU Affero General Public License version 3. --- - -package body Basalt.Strings with - SPARK_Mode -is - - ----------- - -- Image -- - ----------- - - function Image (V : Boolean) return String - is - begin - if V then - return "True"; - else - return "False"; - end if; - end Image; - - ----------- - -- Image -- - ----------- - - function Image (V : Duration) return String - is - Seconds : Long_Integer; - Frac : Duration; - V2 : Duration; - begin - V2 := V; - if V > 9223372036.0 then - V2 := 9223372036.0; - end if; - if V < -9223372036.0 then - V2 := -9223372036.0; - end if; - if V2 = 0.0 then - Seconds := 0; - elsif V2 < 0.0 then - Seconds := Long_Integer (V2 + 0.5); - else -- V2 > 0.0 - Seconds := Long_Integer (V2 - 0.5); - end if; - Frac := abs (V2 - Duration (Seconds)); - Frac := Frac * 1000000 - 0.5; - -- FIXME: Calls of Image with explicit default parameters - -- Eng/RecordFlux/Workarounds#2 - declare - F_Image : constant String := Image (Long_Integer (Frac), 10, True); - Pad : constant String (1 .. 6) := (others => '0'); - S_Image : constant String := - (if Seconds = 0 then (if V2 < 0.0 then "-0" else "0") else Image (Seconds, 10, True)); - begin - if Frac = -0.5 then - return S_Image & "." & Pad; - end if; - if F_Image'Length >= 6 then - return S_Image & "." & F_Image (1 .. 6); - else -- F_Image'Length < 6 - return S_Image & "." & Pad (1 .. 6 - F_Image'Length) & F_Image; - end if; - end; - end Image; - -end Basalt.Strings; diff --git a/examples/apps/ping/src/basalt-strings.ads b/examples/apps/ping/src/basalt-strings.ads deleted file mode 100644 index 0512b794e..000000000 --- a/examples/apps/ping/src/basalt-strings.ads +++ /dev/null @@ -1,53 +0,0 @@ --- --- @summary String operation instances for common types --- @author Johannes Kliemann --- @date 2019-11-19 --- --- Copyright (C) 2019 Componolit GmbH --- --- This file is part of Basalt, which is distributed under the terms of the --- GNU Affero General Public License version 3. --- - -with Interfaces; -with Basalt.Strings_Generic; - -package Basalt.Strings with - SPARK_Mode, - Pure, - Annotate => (GNATprove, Terminating) -is - - -- Image instances for the most common ranged and modular types - function Image is new Strings_Generic.Image_Ranged (Integer); - function Image is new Strings_Generic.Image_Ranged (Long_Integer); - function Image is new Strings_Generic.Image_Modular (Standard.Interfaces.Unsigned_8); - function Image is new Strings_Generic.Image_Modular (Standard.Interfaces.Unsigned_16); - function Image is new Strings_Generic.Image_Modular (Standard.Interfaces.Unsigned_32); - function Image is new Strings_Generic.Image_Modular (Standard.Interfaces.Unsigned_64); - - -- Image function for Boolean - -- - -- @param V Boolean value - -- @return String "True" or "False" - function Image (V : Boolean) return String with - Post => Image'Result'Length <= 5 and Image'Result'First = 1; - - -- Image function for Duration - -- - -- @param V Duration value - -- @param Duration as string with 6 decimals - function Image (V : Duration) return String with - Post => Image'Result'Length <= 28 and Image'Result'First = 1; - - package Value_U8 is new Strings_Generic.Value_Option_Modular (Interfaces.Unsigned_8); - package Value_U16 is new Strings_Generic.Value_Option_Modular (Interfaces.Unsigned_16); - package Value_U32 is new Strings_Generic.Value_Option_Modular (Interfaces.Unsigned_32); - package Value_U64 is new Strings_Generic.Value_Option_Modular (Interfaces.Unsigned_64); - - package Value_Integer is new Strings_Generic.Value_Option_Ranged (Integer); - package Value_Long_Integer is new Strings_Generic.Value_Option_Ranged (Long_Integer); - package Value_Natural is new Strings_Generic.Value_Option_Ranged (Natural); - package Value_Positive is new Strings_Generic.Value_Option_Ranged (Positive); - -end Basalt.Strings;