[multiple changes]

2017-04-25  Gary Dismukes  <dismukes@adacore.com>

	* sem_ch3.adb, exp_util.adb, sem_prag.adb, exp_ch4.adb: Minor
	reformatting.

2017-04-25  Yannick Moy  <moy@adacore.com>

	* a-ngelfu.adb, a-ngelfu.ads: Add SPARK_Mode On on spec, Off
	on body.

From-SVN: r247207

7 files changed, 37 insertions, 22 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 4920702..a3a79cd 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,13 @@
+2017-04-25  Gary Dismukes  <dismukes@adacore.com>
+
+	* sem_ch3.adb, exp_util.adb, sem_prag.adb, exp_ch4.adb: Minor
+	reformatting.
+
+2017-04-25  Yannick Moy  <moy@adacore.com>
+
+	* a-ngelfu.adb, a-ngelfu.ads: Add SPARK_Mode On on spec, Off
+	on body.
+
 2017-04-25  Ed Schonberg  <schonberg@adacore.com>
 
 	* sem_disp.adb (Check_Dispatching_Context): Add guard to refine
diff --git a/gcc/ada/a-ngelfu.adb b/gcc/ada/a-ngelfu.adb
index f17d924..e7a75ee 100644
--- a/gcc/ada/a-ngelfu.adb
+++ b/gcc/ada/a-ngelfu.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -38,7 +38,9 @@
 
 with Ada.Numerics.Aux;
 
-package body Ada.Numerics.Generic_Elementary_Functions is
+package body Ada.Numerics.Generic_Elementary_Functions with
+  SPARK_Mode => Off
+is
 
    use type Ada.Numerics.Aux.Double;
 
diff --git a/gcc/ada/a-ngelfu.ads b/gcc/ada/a-ngelfu.ads
index 8b257b6..767708d 100644
--- a/gcc/ada/a-ngelfu.ads
+++ b/gcc/ada/a-ngelfu.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2012-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 2012-2016, Free Software Foundation, Inc.         --
 --                                                                          --
 -- This specification is derived from the Ada Reference Manual for use with --
 -- GNAT. The copyright notice above, and the license provisions that follow --
@@ -36,7 +36,9 @@
 generic
    type Float_Type is digits <>;
 
-package Ada.Numerics.Generic_Elementary_Functions is
+package Ada.Numerics.Generic_Elementary_Functions with
+  SPARK_Mode => On
+is
    pragma Pure;
 
    function Sqrt (X : Float_Type'Base) return Float_Type'Base with
diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb
index 658c3d8..bc0aea2 100644
--- a/gcc/ada/exp_ch4.adb
+++ b/gcc/ada/exp_ch4.adb
@@ -10779,9 +10779,9 @@ package body Exp_Ch4 is
 
       if Is_Access_Type (Target_Type) then
 
-         --  If this type conversion was internally generated by the frontend
+         --  If this type conversion was internally generated by the front end
          --  to displace the pointer to the object to reference an interface
-         --  type and the original node was an 'Unrestricted_Access reference
+         --  type and the original node was an Unrestricted_Access attribute,
          --  then skip applying accessibility checks (because, according to the
          --  GNAT Reference Manual, this attribute is similar to 'Access except
          --  that all accessibility and aliased view checks are omitted).
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 35c5ed2..19ba42b 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -1292,7 +1292,8 @@ package body Exp_Util is
          if Is_Ignored (DIC_Prag) then
             null;
 
-         --  Otherwise the DIC expression must be checked at runtime. Generate:
+         --  Otherwise the DIC expression must be checked at run time.
+         --  Generate:
 
          --    pragma Check (<Nam>, <DIC_Expr>);
 
@@ -2245,7 +2246,7 @@ package body Exp_Util is
 
          --  When the type inheriting the class-wide invariant is a concurrent
          --  type, use the corresponding record type because it contains all
-         --  primitive operations of the concurren type and allows for proper
+         --  primitive operations of the concurrent type and allows for proper
          --  substitution.
 
          if Is_Concurrent_Type (T) then
@@ -2417,7 +2418,7 @@ package body Exp_Util is
             null;
 
          --  Otherwise the invariant is checked. Build a pragma Check to verify
-         --  the expression at runtime.
+         --  the expression at run time.
 
          else
             Assoc := New_List (
@@ -3395,11 +3396,11 @@ package body Exp_Util is
       --      force every derived type to potentially provide an empty body.
 
       --    * The invariant procedure does not need to be declared as abstract.
-      --      This allows for a proper body which in turn avoids redundant
+      --      This allows for a proper body, which in turn avoids redundant
       --      processing of the same invariants for types with multiple views.
 
       --    * The class-wide type allows for calls to abstract primitives
-      --      within a non-abstract subprogram. The calls are treated as
+      --      within a nonabstract subprogram. The calls are treated as
       --      dispatching and require additional processing when they are
       --      remapped to call primitives of derived types. See routine
       --      Replace_References for details.
@@ -11506,7 +11507,7 @@ package body Exp_Util is
 
       function Replace_Ref (Ref : Node_Id) return Traverse_Result is
          procedure Remove_Controlling_Arguments (From_Arg : Node_Id);
-         --  Reset the Controlling_Argument of all function calls which
+         --  Reset the Controlling_Argument of all function calls that
          --  encapsulate node From_Arg.
 
          ----------------------------------
@@ -11630,14 +11631,14 @@ package body Exp_Util is
                New_Ref := New_Occurrence_Of (Deriv_Obj, Loc);
 
                --  The type of the _object parameter is class-wide when the
-               --  expression comes from an assertion pragma which applies to
+               --  expression comes from an assertion pragma that applies to
                --  an abstract parent type or an interface. The class-wide type
                --  facilitates the preanalysis of the expression by treating
-               --  calls to abstract primitives which mention the current
+               --  calls to abstract primitives that mention the current
                --  instance of the type as dispatching. Once the calls are
                --  remapped to invoke overriding or inherited primitives, the
                --  calls no longer need to be dispatching. Examine all function
-               --  calls which encapsule the _object parameter and reset their
+               --  calls that encapsulate the _object parameter and reset their
                --  Controlling_Argument attribute.
 
                if Is_Class_Wide_Type (Etype (Par_Obj))
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index f40d142..7a9e52d 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -1729,7 +1729,7 @@ package body Sem_Ch3 is
                   end if;
 
                   --  Apply legality checks in RM 6.1.1 (10-13) concerning
-                  --  non-conforming preconditions in both an ancestor and
+                  --  nonconforming preconditions in both an ancestor and
                   --  a progenitor operation.
 
                   if Present (Anc)
@@ -2289,9 +2289,9 @@ package body Sem_Ch3 is
                if Is_Interface (Typ) then
 
                   --  Interfaces are treated as the partial view of a private
-                  --  type in order to achieve uniformity with the general
+                  --  type, in order to achieve uniformity with the general
                   --  case. As a result, an interface receives only a "partial"
-                  --  invariant procedure which is never called.
+                  --  invariant procedure, which is never called.
 
                   if Has_Own_Invariants (Typ) then
                      Build_Invariant_Procedure_Body
@@ -15335,7 +15335,7 @@ package body Sem_Ch3 is
 
       New_Overloaded_Entity (New_Subp, Derived_Type);
 
-      --  Ada RM 6.1.1 (15): If a subprogram inherits non-conforming class-wide
+      --  Ada RM 6.1.1 (15): If a subprogram inherits nonconforming class-wide
       --  preconditions and the derived type is abstract, the derived operation
       --  is abstract as well if parent subprogram is not abstract or null.
 
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index d67beeb..53f6b42 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -17112,11 +17112,11 @@ package body Sem_Prag is
 
             Discard := Rep_Item_Too_Late (Typ, N, FOnly => True);
 
-            --  Create the declaration of the invariant procedure which will
-            --  verify the invariant at run-time. Interfaces are treated as the
+            --  Create the declaration of the invariant procedure that will
+            --  verify the invariant at run time. Interfaces are treated as the
             --  partial view of a private type in order to achieve uniformity
             --  with the general case. As a result, an interface receives only
-            --  a "partial" invariant procedure which is never called.
+            --  a "partial" invariant procedure, which is never called.
 
             Build_Invariant_Procedure_Declaration
               (Typ               => Typ,