Change style of Ada comments

Ref. #816
AdaCore · Sep 22, 2022 · 85004dc · 85004dc
1 parent 026f624
commit 85004dc
Show file tree

Hide file tree

Showing 275 changed files with 777 additions and 772 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -16,8 +16,14 @@ CLI:
 
 ### Changed
 
+Specification:
+
 - Syntax for defining initial and final states of session (#700)
 
+Generator:
+
+- Style of Ada comments (#816)
+
 ### Removed
 
 Specification:

diff --git a/defaults.gpr b/defaults.gpr
@@ -14,19 +14,19 @@ abstract project Defaults is
 
    case Compiler_Variant is
       when "community2020" =>
-         GNATVI := "";  --  https://github.com/Componolit/Workarounds/issues/43
-         GNATA  := "";  --  https://github.com/Componolit/Workarounds/issues/49
+         GNATVI := "";  -- https://github.com/Componolit/Workarounds/issues/43
+         GNATA  := "";  -- https://github.com/Componolit/Workarounds/issues/49
       when "community2021" =>
-         GNATA  := "";  --  https://github.com/Componolit/Workarounds/issues/49
+         GNATA  := "";  -- https://github.com/Componolit/Workarounds/issues/49
       when "pro20.2" =>
-         GNATVI := "";  --  https://github.com/Componolit/Workarounds/issues/43
-         GNATVO := "";  --  https://github.com/Componolit/Workarounds/issues/23
-         GNATEV := "";  --  https://github.com/Componolit/Workarounds/issues/22
-         GNATA  := "";  --  https://github.com/Componolit/Workarounds/issues/49
+         GNATVI := "";  -- https://github.com/Componolit/Workarounds/issues/43
+         GNATVO := "";  -- https://github.com/Componolit/Workarounds/issues/23
+         GNATEV := "";  -- https://github.com/Componolit/Workarounds/issues/22
+         GNATA  := "";  -- https://github.com/Componolit/Workarounds/issues/49
       when "pro21.2" | "pro22.0" =>
-         GNATA  := "";  --  https://github.com/Componolit/Workarounds/issues/49
+         GNATA  := "";  -- https://github.com/Componolit/Workarounds/issues/49
       when "fsf11.2.4" | "fsf12.1.2" =>
-         GNATA  := "";  --  https://github.com/Componolit/Workarounds/issues/49
+         GNATA  := "";  -- https://github.com/Componolit/Workarounds/issues/49
       when others =>
    end case;
 
@@ -68,8 +68,8 @@ abstract project Defaults is
       "--memlimit=2000",
       "--checks-as-errors",
       "--warnings=error",
-      --  https://github.com/Componolit/RecordFlux/issues/670
-      --  "--proof-warnings",
+      -- https://github.com/Componolit/RecordFlux/issues/670
+      -- "--proof-warnings",
       "--no-axiom-guard",
       "--counterexamples=off",
       Procs_Switch,
@@ -87,59 +87,59 @@ abstract project Defaults is
       "-gnatf",    -- Full errors. Multiple errors per line, all undefined references, do not attempt to suppress cascaded errors.
       "-gnatU",    -- Tag all error messages with the unique string ‘error:’.
 
-      --  Validity Checks
-      "-gnatVc",  --  Validity checks for copies.
-      "-gnatVd",  --  Default (RM) validity checks.
-      "-gnatVe",  --  Validity checks for elementary components.
-      "-gnatVf",  --  Validity checks for floating-point values.
-      GNATVI,     --  Validity checks for ``in`` mode parameters.
-      "-gnatVm",  --  Validity checks for ``in out`` mode parameters.
-      GNATVO,     --  Validity checks for operator and attribute operands.
-      "-gnatVp",  --  Validity checks for parameters.
-      "-gnatVr",  --  Validity checks for function returns.
-      "-gnatVs",  --  Validity checks for subscripts.
-      "-gnatVt",  --  Validity checks for tests.
-      GNATEV,     --  Check that all actual parameters of a subprogram call are valid according to the rules of validity checking (Validity Checking).
-
-      --  Debugging
-      "-fstack-check",  --  Activate stack checking.
-      "-g",             --  Enable generation of debugging information.
-      GNATA,            --  Enable assertions.
-
-      --  Warnings
-      "-gnatwa",   --  Activate most optional warnings.
-      "-gnatw.d",  --  Activate tagging of warning and info messages.
-      "-gnatwe",   --  Treat all run-time exception warnings as errors.
-      "-gnatwd",   --  Activate warnings on implicit dereferencing.
-      --  https://github.com/Componolit/Workarounds/issues/27
-      --  "-gnatwh",   --  Activate warnings on hiding.
-      "-gnatwt",   --  Activate warnings for tracking of deleted conditional code.
-      "-gnatwQ",   --  Suppress warnings on questionable missing parentheses.
-
-      --  Style Checks
-      "-gnaty3",    --  Specify indentation level.
-      "-gnatya",    --  Check attribute casing.
-      "-gnatyA",    --  Use of array index numbers in array attributes.
-      "-gnatyb",    --  Blanks not allowed at statement end.
-      "-gnatyc",    --  Check comments, double space.
-      "-gnatyd",    --  Check no DOS line terminators present.
-      "-gnatye",    --  Check end/exit labels.
-      "-gnatyf",    --  No form feeds or vertical tabs.
-      "-gnatyh",    --  No horizontal tabs.
-      "-gnatyi",    --  Check if-then layout.
-      "-gnatyI",    --  Check mode IN keywords.
-      "-gnatyk",    --  Check keyword casing.
-      "-gnatyl",    --  Check layout.
-      "-gnatyL9",   --  Set maximum nesting level.
-      "-gnatyM120", --  Set maximum line length.
-      "-gnatyn",    --  Check casing of entities in Standard.
-      "-gnatyO",    --  Check that overriding subprograms are explicitly marked as such.
-      "-gnatyp",    --  Check pragma casing.
-      "-gnatyr",    --  Check references.
-      "-gnatyS",    --  Check no statements after then/else.
-      "-gnatyt",    --  Check token spacing.
-      "-gnatyu",    --  Check unnecessary blank lines.
-      "-gnatyx",    --  Check extra parentheses.
+      -- Validity Checks
+      "-gnatVc",  -- Validity checks for copies.
+      "-gnatVd",  -- Default (RM) validity checks.
+      "-gnatVe",  -- Validity checks for elementary components.
+      "-gnatVf",  -- Validity checks for floating-point values.
+      GNATVI,     -- Validity checks for ``in`` mode parameters.
+      "-gnatVm",  -- Validity checks for ``in out`` mode parameters.
+      GNATVO,     -- Validity checks for operator and attribute operands.
+      "-gnatVp",  -- Validity checks for parameters.
+      "-gnatVr",  -- Validity checks for function returns.
+      "-gnatVs",  -- Validity checks for subscripts.
+      "-gnatVt",  -- Validity checks for tests.
+      GNATEV,     -- Check that all actual parameters of a subprogram call are valid according to the rules of validity checking (Validity Checking).
+
+      -- Debugging
+      "-fstack-check",  -- Activate stack checking.
+      "-g",             -- Enable generation of debugging information.
+      GNATA,            -- Enable assertions.
+
+      -- Warnings
+      "-gnatwa",   -- Activate most optional warnings.
+      "-gnatw.d",  -- Activate tagging of warning and info messages.
+      "-gnatwe",   -- Treat all run-time exception warnings as errors.
+      "-gnatwd",   -- Activate warnings on implicit dereferencing.
+      -- https://github.com/Componolit/Workarounds/issues/27
+      -- "-gnatwh",   -- Activate warnings on hiding.
+      "-gnatwt",   -- Activate warnings for tracking of deleted conditional code.
+      "-gnatwQ",   -- Suppress warnings on questionable missing parentheses.
+
+      -- Style Checks
+      "-gnaty3",    -- Specify indentation level.
+      "-gnatya",    -- Check attribute casing.
+      "-gnatyA",    -- Use of array index numbers in array attributes.
+      "-gnatyb",    -- Blanks not allowed at statement end.
+      "-gnatyC",    -- Check comments, single space.
+      "-gnatyd",    -- Check no DOS line terminators present.
+      "-gnatye",    -- Check end/exit labels.
+      "-gnatyf",    -- No form feeds or vertical tabs.
+      "-gnatyh",    -- No horizontal tabs.
+      "-gnatyi",    -- Check if-then layout.
+      "-gnatyI",    -- Check mode IN keywords.
+      "-gnatyk",    -- Check keyword casing.
+      "-gnatyl",    -- Check layout.
+      "-gnatyL9",   -- Set maximum nesting level.
+      "-gnatyM120", -- Set maximum line length.
+      "-gnatyn",    -- Check casing of entities in Standard.
+      "-gnatyO",    -- Check that overriding subprograms are explicitly marked as such.
+      "-gnatyp",    -- Check pragma casing.
+      "-gnatyr",    -- Check references.
+      "-gnatyS",    -- Check no statements after then/else.
+      "-gnatyt",    -- Check token spacing.
+      "-gnatyu",    -- Check unnecessary blank lines.
+      "-gnatyx",    -- Check extra parentheses.
 
       ""
    );

diff --git a/examples/apps/dhcp_client/specs/dhcp.rflx b/examples/apps/dhcp_client/specs/dhcp.rflx
@@ -1,25 +1,25 @@
 with IPv4;
 
---  Dynamic Host Configuration Protocol (RFC 2131)
+-- Dynamic Host Configuration Protocol (RFC 2131)
 
 package DHCP is
 
-   --  DHCP Options and BOOTP Vendor Extensions (RFC 1533)
+   -- DHCP Options and BOOTP Vendor Extensions (RFC 1533)
 
-   --  https://github.com/Componolit/RecordFlux-specifications/issues/70
-   --  The full list of Codes is defined in
-   --  https://www.iana.org/assignments/bootp-dhcp-parameters/bootp-dhcp-parameters.xml#options.
+   -- https://github.com/Componolit/RecordFlux-specifications/issues/70
+   -- The full list of Codes is defined in
+   -- https://www.iana.org/assignments/bootp-dhcp-parameters/bootp-dhcp-parameters.xml#options.
    type Code is
-      (--  BOOTP Vendor Information Extensions (RFC 1497)
+      (-- BOOTP Vendor Information Extensions (RFC 1497)
        Pad_Option                                              =>   0,
        End_Option                                              => 255,
        Subnet_Mask_Option                                      =>   1,
        Router_Option                                           =>   3,
        Domain_Name_Server_Option                               =>   6,
        Domain_Name_Option                                      =>  15,
-       --  IP Layer Parameters per Interface (RFC 1533)
+       -- IP Layer Parameters per Interface (RFC 1533)
        Broadcast_Address_Option                                =>  28,
-       --  DHCP Extensions (RFC 1533)
+       -- DHCP Extensions (RFC 1533)
        Requested_IP_Address_Option                             =>  50,
        IP_Address_Lease_Time_Option                            =>  51,
        Option_Overload_Option                                  =>  52,
@@ -74,9 +74,9 @@ package DHCP is
        File_And_Sname_Overload => 3)
    with Size => 8;
 
-   --  https://github.com/Componolit/RecordFlux-specifications/issues/70
-   --  The full list of Codes is defined in
-   --  https://www.iana.org/assignments/bootp-dhcp-parameters/bootp-dhcp-parameters.xml#message-type-53.
+   -- https://github.com/Componolit/RecordFlux-specifications/issues/70
+   -- The full list of Codes is defined in
+   -- https://www.iana.org/assignments/bootp-dhcp-parameters/bootp-dhcp-parameters.xml#message-type-53.
    type DHCP_Message_Type is
       (DHCPDISCOVER => 1,
        DHCPOFFER    => 2,
@@ -176,12 +176,12 @@ package DHCP is
             then null;
       end message;
 
-   --  DHCP Message (RFC 2131, 2)
+   -- DHCP Message (RFC 2131, 2)
 
    type Message_Op_Code is (BOOTREQUEST => 1, BOOTREPLY => 2) with Size => 8;
-   --  https://github.com/Componolit/RecordFlux-specifications/issues/70
-   --  The full list of Hardware Types is defined in
-   --  https://www.iana.org/assignments/arp-parameters/arp-parameters.xml#arp-parameters-2.
+   -- https://github.com/Componolit/RecordFlux-specifications/issues/70
+   -- The full list of Hardware Types is defined in
+   -- https://www.iana.org/assignments/arp-parameters/arp-parameters.xml#arp-parameters-2.
    type Hardware_Address_Type is (HT_Reserved => 0, HT_Ethernet_10 => 1) with Size => 8, Always_Valid;
    type Hardware_Address_Length is (HL_Ethernet => 6) with Size => 8;
    type Hops is mod 2 ** 8;

diff --git a/examples/apps/dhcp_client/specs/dhcp_client.rflx b/examples/apps/dhcp_client/specs/dhcp_client.rflx
@@ -24,7 +24,7 @@ package DHCP_Client is
                DHCP_Message_Type => DHCP::DHCPDISCOVER
             )
          );
-         --  https://github.com/Componolit/RecordFlux/issues/488
+         -- https://github.com/Componolit/RecordFlux/issues/488
          Parameter_Request_List'Append (DHCP::Subnet_Mask_Option);
          Parameter_Request_List'Append (DHCP::Router_Option);
          Parameter_Request_List'Append (DHCP::Domain_Name_Option);
@@ -54,7 +54,7 @@ package DHCP_Client is
             Yiaddr => 0,
             Siaddr => 0,
             Giaddr => 0,
-            --  https://github.com/Componolit/RecordFlux/issues/485
+            -- https://github.com/Componolit/RecordFlux/issues/485
             Chaddr => [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0],
             Sname => [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
                       0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0],
@@ -136,7 +136,7 @@ package DHCP_Client is
             Yiaddr => 0,
             Siaddr => Offer_Siaddr,
             Giaddr => 0,
-            --  https://github.com/Componolit/RecordFlux/issues/485
+            -- https://github.com/Componolit/RecordFlux/issues/485
             Chaddr => [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0],
             Sname => [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
                       0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0],

diff --git a/examples/apps/dhcp_client/src/channel.adb b/examples/apps/dhcp_client/src/channel.adb
@@ -7,8 +7,8 @@ is
    use type RFLX.RFLX_Builtin_Types.Index;
    use type Ada.Streams.Stream_Element_Offset;
 
-   --  https://github.com/Componolit/RecordFlux/issues/482
-   --  Ada.Streams.Stream_Element_Array is not yet supported as buffer type and thus a conversion is needed.
+   -- https://github.com/Componolit/RecordFlux/issues/482
+   -- Ada.Streams.Stream_Element_Array is not yet supported as buffer type and thus a conversion is needed.
 
    function To_Ada_Stream (Buffer : RFLX.RFLX_Builtin_Types.Bytes) return Ada.Streams.Stream_Element_Array with
       Pre =>

diff --git a/rflx/ada.py b/rflx/ada.py
@@ -1812,7 +1812,7 @@ def __init__(self, comment: str) -> None:
         self.comment = comment
 
     def __str__(self) -> str:
-        return f"--  {self.comment}"
+        return f"-- {self.comment}"
 
 
 class IfStatement(Statement):

diff --git a/rflx/generator/const.py b/rflx/generator/const.py
@@ -58,7 +58,7 @@
 UNREACHABLE = ada.Call(TYPES * "Unreachable")
 
 CONFIGURATION_PRAGMAS = [
-    ada.Pragma("Style_Checks", [ada.String("N3aAbcdefhiIklnOprStux")]),
+    ada.Pragma("Style_Checks", [ada.String("N3aAbCdefhiIklnOprStux")]),
     # https://github.com/Componolit/RecordFlux/issues/508
     ada.Pragma("Warnings", [ada.Variable("Off"), ada.String("redundant conversion")]),
 ]
diff --git a/rflx/templates/license_header b/rflx/templates/license_header
@@ -1,8 +1,8 @@
 --
---  Generated by RecordFlux {version} on {date}
+-- Generated by RecordFlux {version} on {date}
 --
---  Copyright (C) 2018-{year} Componolit GmbH
+-- Copyright (C) 2018-{year} Componolit GmbH
 --
---  This file is distributed under the terms of the GNU Affero General Public License version 3.
+-- This file is distributed under the terms of the GNU Affero General Public License version 3.
 --
 
diff --git a/rflx/templates/rflx_arithmetic.adb b/rflx/templates/rflx_arithmetic.adb
@@ -1,4 +1,4 @@
-pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+pragma Style_Checks ("N3aAbCdefhiIklnOprStux");
 
 package body {prefix}RFLX_Arithmetic with
   SPARK_Mode

diff --git a/rflx/templates/rflx_arithmetic.ads b/rflx/templates/rflx_arithmetic.ads
@@ -1,4 +1,4 @@
-pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+pragma Style_Checks ("N3aAbCdefhiIklnOprStux");
 
 package {prefix}RFLX_Arithmetic with
   SPARK_Mode,
@@ -11,8 +11,8 @@ is
 
    type Base_Integer is range 0 .. 2 ** 63 - 1;
 
-   --  Express that V contains at most Bits non-zero bits, in the least
-   --  significant part (the rest is zero).
+   -- Express that V contains at most Bits non-zero bits, in the least
+   -- significant part (the rest is zero).
    pragma Warnings (Off, "postcondition does not mention function result");
    function Fits_Into (V : U64; Bits : Natural) return Boolean
    is (if Bits < U64'Size then V < 2 ** Bits)
@@ -22,20 +22,20 @@ is
    is (if Bits < Base_Integer'Size then V < 2 ** Bits)
      with Post => True;
 
-   --  Express that V contains (U64'Size - Bits) leading zero bits, then (Bits -
-   --  Lower) bits of data, then Lower bits of zeros.
-   --  |- (U64'Size - bits) -|- (Bits-Lower) -|- Lower -|
-   --  |000000000000000000000|xxxxxxxxxxxxxxxx|000000000|
+   -- Express that V contains (U64'Size - Bits) leading zero bits, then (Bits -
+   -- Lower) bits of data, then Lower bits of zeros.
+   -- |- (U64'Size - bits) -|- (Bits-Lower) -|- Lower -|
+   -- |000000000000000000000|xxxxxxxxxxxxxxxx|000000000|
    function Fits_Into_Upper (V : U64; Bits, Lower : Natural) return Boolean
    is (if Bits < U64'Size then V <= 2 ** Bits - 2 ** Lower
        elsif Lower > 0 and then Lower < U64'Size then V <= U64'Last - 2 ** Lower + 1)
      with Pre => Bits <= U64'Size and then Lower <= Bits,
           Post => True;
    pragma Warnings (On, "postcondition does not mention function result");
 
-   --  V is assumed to contain Bits bits of data. Add the Amount bits contained
-   --  in Data by shifting V to the left and adding Data. The result contains
-   --  (Bits + Amount) bits of data.
+   -- V is assumed to contain Bits bits of data. Add the Amount bits contained
+   -- in Data by shifting V to the left and adding Data. The result contains
+   -- (Bits + Amount) bits of data.
    function Shift_Add (V : U64;
                        Data : U64;
                        Amount : Natural;
@@ -48,8 +48,8 @@ is
        and then Fits_Into (Data, Amount),
      Post => Fits_Into (Shift_Add'Result, Bits + Amount);
 
-   --  Wrapper of Shift_Right that expresses the operation in terms of
-   --  Fits_Into.
+   -- Wrapper of Shift_Right that expresses the operation in terms of
+   -- Fits_Into.
    function Right_Shift (V : U64; Amount : Natural; Size : Natural) return U64 with
      Pre =>
        Size <= U64'Size
@@ -58,8 +58,8 @@ is
        and then Size - Amount < U64'Size,
      Post => Fits_Into (Right_Shift'Result, Size - Amount);
 
-   --  Wrapper of Shift_Left that expresses the operation in terms of
-   --  Fits_Into/Fits_Into_Upper.
+   -- Wrapper of Shift_Left that expresses the operation in terms of
+   -- Fits_Into/Fits_Into_Upper.
    function Left_Shift (V : U64; Amount : Natural; Size : Natural) return U64 with
      Pre =>
        Size < U64'Size
@@ -68,18 +68,18 @@ is
        and then Size + Amount < U64'Size,
        Post => Fits_Into_Upper (Left_Shift'Result, Size + Amount, Amount);
 
-   --  V is assumed to have Bits bits of data. Set the lower bits of V to zero.
+   -- V is assumed to have Bits bits of data. Set the lower bits of V to zero.
    function Mask_Lower (V : U64; Mask, Bits : Natural) return U64
      with Pre => Bits <= U64'Size and then Fits_Into (V, Bits) and then Mask <= Bits and then Mask >= 1,
           Post => Fits_Into_Upper (Mask_Lower'Result, Bits, Mask);
 
-   --  Set the upper bits of V to zero.
+   -- Set the upper bits of V to zero.
    function Mask_Upper (V : U64; Mask : Natural) return U64
      with Pre => Mask < U64'Size,
           Post => Fits_Into (Mask_Upper'Result, Mask);
 
-   --  Add A and B in the special case where A only uses the upper bits and B
-   --  only the lower bits.
+   -- Add A and B in the special case where A only uses the upper bits and B
+   -- only the lower bits.
    function Add (A : U64; B : U64; Total_Bits, Lower_Bits : Natural) return U64
      with Pre =>
        Total_Bits <= U64'Size