[COMMITTED] ada: Remove GNATcheck violations

[COMMITTED] ada: Remove GNATcheck violations

[Marc Poulhiès]

From: Sheri Bernstein <bernstein@adacore.com>

Remove GNATcheck violations by refactoring code and also using
pragma Annotate to exempt them.

gcc/ada/

	* libgnat/i-cstrin.adb (Free): Rewrite code so there is only one
	return, to remove Improper_Returns violation.
	(Position_Of_Nul): Add pragma to exempt Improper_Returns
	violation.
	(To_Chars_Ptr): Likewise.
	(Value): Likewise

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/libgnat/i-cstrin.adb | 24 +++++++++++++++++++-----
 1 file changed, 19 insertions(+), 5 deletions(-)

diff --git a/gcc/ada/libgnat/i-cstrin.adb b/gcc/ada/libgnat/i-cstrin.adb
index afbac727e31..1eb28655004 100644
--- a/gcc/ada/libgnat/i-cstrin.adb
+++ b/gcc/ada/libgnat/i-cstrin.adb
@@ -92,12 +92,10 @@ is
 
    procedure Free (Item : in out chars_ptr) is
    begin
-      if Item = Null_Ptr then
-         return;
+      if Item /= Null_Ptr then
+         Memory_Free (Item);
+         Item := Null_Ptr;
       end if;
-
-      Memory_Free (Item);
-      Item := Null_Ptr;
    end Free;
 
    --------------------
@@ -187,6 +185,8 @@ is
 
    function Position_Of_Nul (Into : char_array) return size_t is
    begin
+      pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns",
+                       "early returns for performance");
       for J in Into'Range loop
          if Into (J) = nul then
             return J;
@@ -194,6 +194,8 @@ is
       end loop;
 
       return Into'Last + 1;
+
+      pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
    end Position_Of_Nul;
 
    ------------
@@ -226,6 +228,8 @@ is
       Nul_Check : Boolean := False) return chars_ptr
    is
    begin
+      pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns",
+                       "early returns for performance");
       if Item = null then
          return Null_Ptr;
       elsif Nul_Check
@@ -235,6 +239,8 @@ is
       else
          return To_chars_ptr (Item (Item'First)'Address);
       end if;
+
+      pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
    end To_Chars_Ptr;
 
    ------------
@@ -302,6 +308,8 @@ is
       Length : size_t) return char_array
    is
    begin
+      pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns",
+                       "early returns for performance");
       if Item = Null_Ptr then
          raise Dereference_Error;
       end if;
@@ -328,6 +336,8 @@ is
 
          return Result;
       end;
+
+      pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
    end Value;
 
    function Value (Item : chars_ptr) return String is
@@ -339,6 +349,8 @@ is
       Result : char_array (0 .. Length);
 
    begin
+      pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns",
+                       "early returns for performance");
       --  As per AI-00177, this is equivalent to:
 
       --    To_Ada (Value (Item, Length) & nul);
@@ -357,6 +369,8 @@ is
 
       Result (Length) := nul;
       return To_Ada (Result);
+
+      pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
    end Value;
 
 end Interfaces.C.Strings;
-- 
2.42.0

[COMMITTED] ada: Remove GNATcheck violations

[Marc Poulhiès]

From: Sheri Bernstein <bernstein@adacore.com>

Remove GNATcheck violations by refactoring code and also using
pragma Annotate to exempt them.

gcc/ada/

	* libgnat/a-comlin.adb (Argument_Count): Rewrite code so there is
	only one return, to remove Improper_Returns violation.
	(Command_Name): Add pragma to exempt Improper_Returns violation.

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/libgnat/a-comlin.adb | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

diff --git a/gcc/ada/libgnat/a-comlin.adb b/gcc/ada/libgnat/a-comlin.adb
index b95ecd3290c..8a6686181bd 100644
--- a/gcc/ada/libgnat/a-comlin.adb
+++ b/gcc/ada/libgnat/a-comlin.adb
@@ -77,16 +77,11 @@ package body Ada.Command_Line is
 
    function Argument_Count return Natural is
    begin
-      if not Initialized then
-         --  RM A.15 (11)
-         return 0;
-      end if;
-
-      if Remove_Args = null then
-         return Arg_Count - 1;
-      else
-         return Remove_Count;
-      end if;
+      return
+         (if not Initialized then 0  --  RM A.15 (11)
+          elsif Remove_Args = null then Arg_Count - 1
+          else Remove_Count
+         );
    end Argument_Count;
 
    -----------------
@@ -107,6 +102,8 @@ package body Ada.Command_Line is
 
    function Command_Name return String is
    begin
+      pragma Annotate (Gnatcheck, Exempt_On, "Improper_Returns",
+                       "early returns for performance");
       if not Initialized then
          return "";
       end if;
@@ -118,6 +115,7 @@ package body Ada.Command_Line is
          Fill_Arg (Arg'Address, 0);
          return Arg;
       end;
+      pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
    end Command_Name;
 
 end Ada.Command_Line;
-- 
2.43.0

[COMMITTED] ada: Remove GNATcheck violations

[Marc Poulhiès]

From: Sheri Bernstein <bernstein@adacore.com>

Use pragma Annotate to exempt GNATcheck violations that are related
to proof code. Specifically, exempt rules "Metrics_LSLOC" and
"Metrics_Cyclomatic_Complexity" whose limits are exceeded due to
proof code, and exempt rule "Discriminated_Records" for a variant record
that is only used in proof code.

gcc/ada/

	* libgnat/s-aridou.adb: Add pragma to exempt Metrics_LSLOC.
	(Double_Divide): Add pragma to exempt
	Metrics_Cyclomatic_Complexity.
	(Scaled_Divide): Likewise.
	* libgnat/s-vauspe.ads (Uns_Option): Add pragma to exempt
	Discriminated_Records.

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/libgnat/s-aridou.adb | 11 +++++++++++
 gcc/ada/libgnat/s-vauspe.ads |  3 +++
 2 files changed, 14 insertions(+)

diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb
index beb56bfabe1..6bcce59cfeb 100644
--- a/gcc/ada/libgnat/s-aridou.adb
+++ b/gcc/ada/libgnat/s-aridou.adb
@@ -29,6 +29,9 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
+pragma Annotate (Gnatcheck, Exempt_On, "Metrics_LSLOC",
+                 "limit exceeded due to proof code");
+
 with Ada.Unchecked_Conversion;
 with System.SPARK.Cut_Operations; use System.SPARK.Cut_Operations;
 
@@ -814,6 +817,8 @@ is
    -- Double_Divide --
    -------------------
 
+   pragma Annotate (Gnatcheck, Exempt_On, "Metrics_Cyclomatic_Complexity",
+                    "limit exceeded due to proof code");
    procedure Double_Divide
      (X, Y, Z : Double_Int;
       Q, R    : out Double_Int;
@@ -1221,6 +1226,7 @@ is
 
       Prove_Signs;
    end Double_Divide;
+   pragma Annotate (Gnatcheck, Exempt_Off, "Metrics_Cyclomatic_Complexity");
 
    ---------
    -- Le3 --
@@ -1899,6 +1905,8 @@ is
    -- Scaled_Divide --
    -------------------
 
+   pragma Annotate (Gnatcheck, Exempt_On, "Metrics_Cyclomatic_Complexity",
+                    "limit exceeded due to proof code");
    procedure Scaled_Divide
      (X, Y, Z : Double_Int;
       Q, R    : out Double_Int;
@@ -3317,6 +3325,7 @@ is
       Prove_Sign_R;
       Prove_Signs;
    end Scaled_Divide;
+   pragma Annotate (Gnatcheck, Exempt_Off, "Metrics_Cyclomatic_Complexity");
 
    ----------
    -- Sub3 --
@@ -3658,3 +3667,5 @@ is
 
    pragma Annotate (Gnatcheck, Exempt_Off, "Improper_Returns");
 end System.Arith_Double;
+
+pragma Annotate (Gnatcheck, Exempt_Off, "Metrics_LSLOC");
diff --git a/gcc/ada/libgnat/s-vauspe.ads b/gcc/ada/libgnat/s-vauspe.ads
index a6f81d715c4..b276eed5105 100644
--- a/gcc/ada/libgnat/s-vauspe.ads
+++ b/gcc/ada/libgnat/s-vauspe.ads
@@ -68,6 +68,8 @@ is
         when others => raise Program_Error)
    with Ghost;
 
+   pragma Annotate (Gnatcheck, Exempt_On, "Discriminated_Records",
+                    "variant record only used in proof code");
    type Uns_Option (Overflow : Boolean := False) is record
       case Overflow is
          when True =>
@@ -76,6 +78,7 @@ is
             Value : Uns := 0;
       end case;
    end record;
+   pragma Annotate (Gnatcheck, Exempt_Off, "Discriminated_Records");
 
    function Wrap_Option (Value : Uns) return Uns_Option is
      (Overflow => False, Value => Value);
-- 
2.40.0