[multiple changes]

2017-10-14  Eric Botcazou  <ebotcazou@adacore.com>

	* layout.ads (Set_Elem_Alignment): Add Align parameter defaulted to 0.
	* layout.adb (Set_Elem_Alignment): Likewise.  Use M name as maximum
	alignment for consistency.  If Align is non-zero, use the minimum of
	Align and M for the alignment.
	* cstand.adb (Build_Float_Type): Use Set_Elem_Alignment instead of
	setting the alignment directly.

2017-10-14  Ed Schonberg  <schonberg@adacore.com>

	* sem_prag.adb (Analyze_Pragma, case Check): Defer evaluation of the
	optional string in an Assert pragma until the expansion of the pragma
	has rewritten it as a conditional statement, so that the string
	argument is only evaluaed if the assertion fails. This is mandated by
	RM 11.4.2.

2017-10-14  Hristian Kirtchev  <kirtchev@adacore.com>

	* debug.adb: Switch -gnatd.v and associated flag are now used to
	enforce the SPARK rules for elaboration in SPARK code.
	* sem_elab.adb: Describe switch -gnatd.v.
	(Process_Call): Verify the SPARK rules only when -gnatd.v is in effect.
	(Process_Instantiation): Verify the SPARK rules only when -gnatd.v is
	in effect.
	(Process_Variable_Assignment): Clarify why variable assignments are
	processed reglardless of whether -gnatd.v is in effect.
	* doc/gnat_ugn/elaboration_order_handling_in_gnat.rst: Update the
	sections on elaboration code and compilation switches.
	* gnat_ugn.texi: Regenerate.

2017-10-14  Gary Dismukes  <dismukes@adacore.com>

	* exp_util.adb, freeze.adb, sem_aggr.adb, sem_util.ads, sem_util.adb,
	sem_warn.adb: Minor reformattings.

From-SVN: r253757

15 files changed, 244 insertions, 62 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 5ffb2e4..d0d17ba 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,39 @@
+2017-10-14  Eric Botcazou  <ebotcazou@adacore.com>
+
+	* layout.ads (Set_Elem_Alignment): Add Align parameter defaulted to 0.
+	* layout.adb (Set_Elem_Alignment): Likewise.  Use M name as maximum
+	alignment for consistency.  If Align is non-zero, use the minimum of
+	Align and M for the alignment.
+	* cstand.adb (Build_Float_Type): Use Set_Elem_Alignment instead of
+	setting the alignment directly.
+
+2017-10-14  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_prag.adb (Analyze_Pragma, case Check): Defer evaluation of the
+	optional string in an Assert pragma until the expansion of the pragma
+	has rewritten it as a conditional statement, so that the string
+	argument is only evaluaed if the assertion fails. This is mandated by
+	RM 11.4.2.
+
+2017-10-14  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* debug.adb: Switch -gnatd.v and associated flag are now used to
+	enforce the SPARK rules for elaboration in SPARK code.
+	* sem_elab.adb: Describe switch -gnatd.v.
+	(Process_Call): Verify the SPARK rules only when -gnatd.v is in effect.
+	(Process_Instantiation): Verify the SPARK rules only when -gnatd.v is
+	in effect.
+	(Process_Variable_Assignment): Clarify why variable assignments are
+	processed reglardless of whether -gnatd.v is in effect.
+	* doc/gnat_ugn/elaboration_order_handling_in_gnat.rst: Update the
+	sections on elaboration code and compilation switches.
+	* gnat_ugn.texi: Regenerate.
+
+2017-10-14  Gary Dismukes  <dismukes@adacore.com>
+
+	* exp_util.adb, freeze.adb, sem_aggr.adb, sem_util.ads, sem_util.adb,
+	sem_warn.adb: Minor reformattings.
+
 2017-10-14  Ed Schonberg  <schonberg@adacore.com>
 
 	* doc/gnat_rm/implementation_defined_aspects.rst: Add documentation
diff --git a/gcc/ada/cstand.adb b/gcc/ada/cstand.adb
index 34617bb..e45c054 100644
--- a/gcc/ada/cstand.adb
+++ b/gcc/ada/cstand.adb
@@ -212,7 +212,7 @@ package body CStand is
       Init_Digits_Value              (E, Digs);
       Set_Float_Rep                  (E, Rep);
       Init_Size                      (E, Siz);
-      Set_Alignment                  (E, UI_From_Int (Align));
+      Set_Elem_Alignment             (E, Align);
       Set_Float_Bounds               (E);
       Set_Is_Frozen                  (E);
       Set_Is_Public                  (E);
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb
index 4e74720..2a81204 100644
--- a/gcc/ada/debug.adb
+++ b/gcc/ada/debug.adb
@@ -112,7 +112,7 @@ package body Debug is
    --  d.s  Strict secondary stack management
    --  d.t  Disable static allocation of library level dispatch tables
    --  d.u  Enable Modify_Tree_For_C (update tree for c)
-   --  d.v
+   --  d.v  Enforce SPARK elaboration rules in SPARK code
    --  d.w  Do not check for infinite loops
    --  d.x  No exception handlers
    --  d.y  Disable implicit pragma Elaborate_All on task bodies
@@ -600,6 +600,13 @@ package body Debug is
    --  d.u  Sets Modify_Tree_For_C mode in which tree is modified to make it
    --       easier to generate code using a C compiler.
 
+   --  d.v  This flag enforces the elaboration rules defined in the SPARK
+   --       Reference Manual, chapter 7.7, to all SPARK code within a unit. As
+   --       a result, constructs which violate the rules in chapter 7.7 are no
+   --       longer accepted, even if the implementation is able to statically
+   --       ensure that accepting these constructs does not introduce the
+   --       possibility of failing an elaboration check.
+
    --  d.w  This flag turns off the scanning of loops to detect possible
    --       infinite loops.
 
diff --git a/gcc/ada/doc/gnat_ugn/elaboration_order_handling_in_gnat.rst b/gcc/ada/doc/gnat_ugn/elaboration_order_handling_in_gnat.rst
index d943c71..c45d3fc 100644
--- a/gcc/ada/doc/gnat_ugn/elaboration_order_handling_in_gnat.rst
+++ b/gcc/ada/doc/gnat_ugn/elaboration_order_handling_in_gnat.rst
@@ -133,8 +133,43 @@ Elaboration Order
 =================
 
 The sequence by which the elaboration code of all units within a partition is
-executed is referred to as **elaboration order**. The elaboration order depends
-on the following factors:
+executed is referred to as **elaboration order**.
+
+Within a single unit, elaboration code is executed in sequential order.
+
+::
+
+   package body Client is
+      Result : ... := Server.Func;
+
+      procedure Proc is
+         package Inst is new Server.Gen;
+      begin
+         Inst.Eval (Result);
+      end Proc;
+   begin
+      Proc;
+   end Client;
+
+In the example above, the elaboration order within package body ``Client`` is
+as follows:
+
+1. The object declaration of ``Result`` is elaborated.
+
+   * Function ``Server.Func`` is invoked.
+
+2. The subprogram body of ``Proc`` is elaborated.
+
+3. Procedure ``Proc`` is invoked.
+
+   * Generic unit ``Server.Gen`` is instantiated as ``Inst``.
+
+   * Instance ``Inst`` is elaborated.
+
+   * Procedure ``Inst.Eval`` is invoked.
+
+The elaboration order of all units within a partition depends on the following
+factors:
 
 * |withed| units
 
@@ -571,7 +606,7 @@ elaboration order and to diagnose elaboration problems.
   a partition is elaboration code. GNAT performs very few diagnostics and
   generates run-time checks to verify the elaboration order of a program. This
   behavior is identical to that specified by the Ada Reference Manual. The
-  dynamic model is enabled with compilation switch :switch:`-gnatE`.
+  dynamic model is enabled with compiler switch :switch:`-gnatE`.
 
 .. index:: Static elaboration model
 
@@ -860,7 +895,7 @@ SPARK Elaboration Model in GNAT
 The SPARK model is identical to the static model in its handling of internal
 targets. The SPARK model, however, requires explicit ``Elaborate`` or
 ``Elaborate_All`` pragmas to be present in the program when a target is
-external, and emits hard errors instead of warnings:
+external, and compiler switch :switch:`-gnatd.v` is in effect.
 
 ::
 
@@ -987,7 +1022,7 @@ available.
 * *Switch to more permissive elaboration model*
 
   If the compilation was performed using the static model, enable the dynamic
-  model with compilation switch :switch:`-gnatE`. GNAT will no longer generate
+  model with compiler switch :switch:`-gnatE`. GNAT will no longer generate
   implicit ``Elaborate`` and ``Elaborate_All`` pragmas, resulting in a behavior
   identical to that specified by the Ada Reference Manual. The binder will
   generate an executable program that may or may not raise ``Program_Error``,
@@ -1504,6 +1539,17 @@ the elaboration order chosen by the binder.
   When this switch is in effect, GNAT will ignore ``'Access`` of an entry,
   operator, or subprogram when the static model is in effect.
 
+.. index:: -gnatd.v  (gnat)
+
+:switch:`-gnatd.v`
+  Enforce SPARK elaboration rules in SPARK code
+
+  When this switch is in effect, GNAT will enforce the SPARK rules of
+  elaboration as defined in the SPARK Reference Manual, section 7.7. As a
+  result, constructs which violate the SPARK elaboration rules are no longer
+  accepted, even if GNAT is able to statically ensure that these constructs
+  will not lead to ABE problems.
+
 .. index:: -gnatd.y  (gnat)
 
 :switch:`-gnatd.y`
@@ -1558,7 +1604,7 @@ the elaboration order chosen by the binder.
   - *SPARK model*
 
     GNAT will indicate how an elaboration requirement is met by the context of
-    a unit.
+    a unit. This diagnostic requires compiler switch :switch:`-gnatd.v`.
 
     ::
 
@@ -1612,8 +1658,8 @@ none of the binder or compiler switches. If the binder succeeds in finding an
 elaboration order, then apart from possible cases involing dispatching calls
 and access-to-subprogram types, the program is free of elaboration errors.
 If it is important for the program to be portable to compilers other than GNAT,
-then the programmer should use compilation switch :switch:`-gnatel` and
-consider the messages about missing or implicitly created ``Elaborate`` and
+then the programmer should use compiler switch :switch:`-gnatel` and consider
+the messages about missing or implicitly created ``Elaborate`` and
 ``Elaborate_All`` pragmas.
 
 If the binder reports an elaboration circularity, the programmer has several
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index b1ab606..d8ac4f8 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -11249,7 +11249,7 @@ package body Exp_Util is
          --  Exp_Ch2.Expand_Renaming). Otherwise the temporary must be
          --  elaborated by gigi, and is of course not to be replaced in-line
          --  by the expression it renames, which would defeat the purpose of
-         --  removing the side-effect.
+         --  removing the side effect.
 
          if Nkind_In (Exp, N_Selected_Component, N_Indexed_Component)
            and then Has_Non_Standard_Rep (Etype (Prefix (Exp)))
@@ -12650,7 +12650,7 @@ package body Exp_Util is
            and then Variable_Ref
          then
             --  Exception is a prefix that is the result of a previous removal
-            --  of side-effects.
+            --  of side effects.
 
             return Is_Entity_Name (Prefix (N))
               and then not Comes_From_Source (Prefix (N))
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index 794fdf3..a106d68 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -8450,7 +8450,7 @@ package body Freeze is
             --  The analysis of the expression may generate insert actions,
             --  which of course must not be executed. We wrap those actions
             --  in a procedure that is not called, and later on eliminated.
-            --  The following cases have no side-effects, and are analyzed
+            --  The following cases have no side effects, and are analyzed
             --  directly.
 
             if Nkind (Dcopy) = N_Identifier
diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi
index a39c257..08e4b4b 100644
--- a/gcc/ada/gnat_ugn.texi
+++ b/gcc/ada/gnat_ugn.texi
@@ -21,7 +21,7 @@
 
 @copying
 @quotation
-GNAT User's Guide for Native Platforms , Oct 09, 2017
+GNAT User's Guide for Native Platforms , Oct 14, 2017
 
 AdaCore
 
@@ -27187,8 +27187,62 @@ elaborated.
 
 
 The sequence by which the elaboration code of all units within a partition is
-executed is referred to as @strong{elaboration order}. The elaboration order depends
-on the following factors:
+executed is referred to as @strong{elaboration order}.
+
+Within a single unit, elaboration code is executed in sequential order.
+
+@example
+package body Client is
+   Result : ... := Server.Func;
+
+   procedure Proc is
+      package Inst is new Server.Gen;
+   begin
+      Inst.Eval (Result);
+   end Proc;
+begin
+   Proc;
+end Client;
+@end example
+
+In the example above, the elaboration order within package body @code{Client} is
+as follows:
+
+
+@enumerate 
+
+@item 
+The object declaration of @code{Result} is elaborated.
+
+
+@itemize *
+
+@item 
+Function @code{Server.Func} is invoked.
+@end itemize
+
+@item 
+The subprogram body of @code{Proc} is elaborated.
+
+@item 
+Procedure @code{Proc} is invoked.
+
+
+@itemize *
+
+@item 
+Generic unit @code{Server.Gen} is instantiated as @code{Inst}.
+
+@item 
+Instance @code{Inst} is elaborated.
+
+@item 
+Procedure @code{Inst.Eval} is invoked.
+@end itemize
+@end enumerate
+
+The elaboration order of all units within a partition depends on the following
+factors:
 
 
 @itemize *
@@ -27689,7 +27743,7 @@ dynamic model is in effect, GNAT assumes that all code within all units in
 a partition is elaboration code. GNAT performs very few diagnostics and
 generates run-time checks to verify the elaboration order of a program. This
 behavior is identical to that specified by the Ada Reference Manual. The
-dynamic model is enabled with compilation switch @code{-gnatE}.
+dynamic model is enabled with compiler switch @code{-gnatE}.
 @end itemize
 
 @geindex Static elaboration model
@@ -28001,7 +28055,7 @@ elaborated prior to the body of @code{Static_Model}.
 The SPARK model is identical to the static model in its handling of internal
 targets. The SPARK model, however, requires explicit @code{Elaborate} or
 @code{Elaborate_All} pragmas to be present in the program when a target is
-external, and emits hard errors instead of warnings:
+external, and compiler switch @code{-gnatd.v} is in effect.
 
 @example
 1. with Server;
@@ -28146,7 +28200,7 @@ code.
 @emph{Switch to more permissive elaboration model}
 
 If the compilation was performed using the static model, enable the dynamic
-model with compilation switch @code{-gnatE}. GNAT will no longer generate
+model with compiler switch @code{-gnatE}. GNAT will no longer generate
 implicit @code{Elaborate} and @code{Elaborate_All} pragmas, resulting in a behavior
 identical to that specified by the Ada Reference Manual. The binder will
 generate an executable program that may or may not raise @code{Program_Error},
@@ -28711,6 +28765,22 @@ When this switch is in effect, GNAT will ignore @code{'Access} of an entry,
 operator, or subprogram when the static model is in effect.
 @end table
 
+@geindex -gnatd.v (gnat)
+
+
+@table @asis
+
+@item @code{-gnatd.v}
+
+Enforce SPARK elaboration rules in SPARK code
+
+When this switch is in effect, GNAT will enforce the SPARK rules of
+elaboration as defined in the SPARK Reference Manual, section 7.7. As a
+result, constructs which violate the SPARK elaboration rules are no longer
+accepted, even if GNAT is able to statically ensure that these constructs
+will not lead to ABE problems.
+@end table
+
 @geindex -gnatd.y (gnat)
 
 
@@ -28785,7 +28855,7 @@ it will provide detailed traceback when an implicit @code{Elaborate} or
 @emph{SPARK model}
 
 GNAT will indicate how an elaboration requirement is met by the context of
-a unit.
+a unit. This diagnostic requires compiler switch @code{-gnatd.v}.
 
 @example
 1. with Server; pragma Elaborate_All (Server);
@@ -28846,8 +28916,8 @@ none of the binder or compiler switches. If the binder succeeds in finding an
 elaboration order, then apart from possible cases involing dispatching calls
 and access-to-subprogram types, the program is free of elaboration errors.
 If it is important for the program to be portable to compilers other than GNAT,
-then the programmer should use compilation switch @code{-gnatel} and
-consider the messages about missing or implicitly created @code{Elaborate} and
+then the programmer should use compiler switch @code{-gnatel} and consider
+the messages about missing or implicitly created @code{Elaborate} and
 @code{Elaborate_All} pragmas.
 
 If the binder reports an elaboration circularity, the programmer has several
diff --git a/gcc/ada/layout.adb b/gcc/ada/layout.adb
index 34c5b5d..52e8452 100644
--- a/gcc/ada/layout.adb
+++ b/gcc/ada/layout.adb
@@ -843,7 +843,7 @@ package body Layout is
    -- Set_Elem_Alignment --
    ------------------------
 
-   procedure Set_Elem_Alignment (E : Entity_Id) is
+   procedure Set_Elem_Alignment (E : Entity_Id; Align : Nat := 0) is
    begin
       --  Do not set alignment for packed array types, this is handled in the
       --  backend.
@@ -869,15 +869,12 @@ package body Layout is
          return;
       end if;
 
-      --  Here we calculate the alignment as the largest power of two multiple
-      --  of System.Storage_Unit that does not exceed either the object size of
-      --  the type, or the maximum allowed alignment.
+      --  We attempt to set the alignment in all the other cases
 
       declare
          S : Int;
          A : Nat;
-
-         Max_Alignment : Nat;
+         M : Nat;
 
       begin
          --  The given Esize may be larger that int'last because of a previous
@@ -908,7 +905,7 @@ package body Layout is
            and then S = 8
            and then Is_Floating_Point_Type (E)
          then
-            Max_Alignment := Ttypes.Target_Double_Float_Alignment;
+            M := Ttypes.Target_Double_Float_Alignment;
 
          --  If the default alignment of "double" or larger scalar types is
          --  specifically capped, enforce the cap.
@@ -917,18 +914,27 @@ package body Layout is
            and then S >= 8
            and then Is_Scalar_Type (E)
          then
-            Max_Alignment := Ttypes.Target_Double_Scalar_Alignment;
+            M := Ttypes.Target_Double_Scalar_Alignment;
 
          --  Otherwise enforce the overall alignment cap
 
          else
-            Max_Alignment := Ttypes.Maximum_Alignment;
+            M := Ttypes.Maximum_Alignment;
          end if;
 
-         A := 1;
-         while 2 * A <= Max_Alignment and then 2 * A <= S loop
-            A := 2 * A;
-         end loop;
+         --  We calculate the alignment as the largest power-of-two multiple
+         --  of System.Storage_Unit that does not exceed the object size of
+         --  the type and the maximum allowed alignment, if none was specified.
+         --  Otherwise we only cap it to the maximum allowed alignment.
+
+         if Align = 0 then
+            A := 1;
+            while 2 * A <= S and then 2 * A <= M loop
+               A := 2 * A;
+            end loop;
+         else
+            A := Nat'Min (Align, M);
+         end if;
 
          --  If alignment is currently not set, then we can safely set it to
          --  this new calculated value.
diff --git a/gcc/ada/layout.ads b/gcc/ada/layout.ads
index 57aa93e4..246970f 100644
--- a/gcc/ada/layout.ads
+++ b/gcc/ada/layout.ads
@@ -74,10 +74,11 @@ package Layout is
    --  types, the RM_Size is simply set to zero. This routine also sets
    --  the Is_Constrained flag in Def_Id.
 
-   procedure Set_Elem_Alignment (E : Entity_Id);
+   procedure Set_Elem_Alignment (E : Entity_Id; Align : Nat := 0);
    --  The front end always sets alignments for elementary types by calling
    --  this procedure. Note that we have to do this for discrete types (since
    --  the Alignment attribute is static), so we might as well do it for all
-   --  elementary types, since the processing is the same.
+   --  elementary types, as the processing is the same. If Align is nonzero,
+   --  it is an external alignment setting that we must respect.
 
 end Layout;
diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb
index 677d599..6c29b38 100644
--- a/gcc/ada/sem_aggr.adb
+++ b/gcc/ada/sem_aggr.adb
@@ -1594,7 +1594,7 @@ package body Sem_Aggr is
             --  unless the expression covers a single component, or the
             --  expander is inactive.
 
-            --  In SPARK mode, expressions that can perform side-effects will
+            --  In SPARK mode, expressions that can perform side effects will
             --  be recognized by the gnat2why back-end, and the whole
             --  subprogram will be ignored. So semantic analysis can be
             --  performed safely.
@@ -3605,7 +3605,7 @@ package body Sem_Aggr is
                      --  This is redundant if the others_choice covers only
                      --  one component (small optimization possible???), but
                      --  indispensable otherwise, because each one must be
-                     --  expanded individually to preserve side-effects.
+                     --  expanded individually to preserve side effects.
 
                      --  Ada 2005 (AI-287): In case of default initialization
                      --  of components, we duplicate the corresponding default
@@ -3881,7 +3881,7 @@ package body Sem_Aggr is
          --  expansion is delayed until the enclosing aggregate is expanded
          --  into assignments. In that case, do not generate checks on the
          --  expression, because they will be generated later, and will other-
-         --  wise force a copy (to remove side-effects) that would leave a
+         --  wise force a copy (to remove side effects) that would leave a
          --  dynamic-sized aggregate in the code, something that gigi cannot
          --  handle.
 
diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb
index 289e853..7f5a3d6 100644
--- a/gcc/ada/sem_elab.adb
+++ b/gcc/ada/sem_elab.adb
@@ -361,6 +361,13 @@ package body Sem_Elab is
    --           entries, operators, and subprograms. As a result, the scenarios
    --           are not recorder or processed.
    --
+   --  -gnatd.v enforce SPARK elaboration rules in SPARK code
+   --
+   --           The ABE mechanism applies some of the SPARK elaboration rules
+   --           defined in the SPARK reference manual, chapter 7.7. Note that
+   --           certain rules are always enforced, regardless of whether the
+   --           switch is active.
+   --
    --  -gnatd.y disable implicit pragma Elaborate_All on task bodies
    --
    --           The ABE mechanism does not generate implicit Elaborate_All when
@@ -6891,16 +6898,18 @@ package body Sem_Elab is
       elsif Is_Up_Level_Target (Target_Attrs.Spec_Decl) then
          return;
 
-      --  The SPARK rules are in effect
+      --  The SPARK rules are verified only when -gnatd.v (enforce SPARK
+      --  elaboration rules in SPARK code) is in effect.
 
-      elsif SPARK_Rules_On then
+      elsif SPARK_Rules_On and Debug_Flag_Dot_V then
          Process_Call_SPARK
            (Call         => Call,
             Call_Attrs   => Call_Attrs,
             Target_Id    => Target_Id,
             Target_Attrs => Target_Attrs);
 
-      --  Otherwise the Ada rules are in effect
+      --  Otherwise the Ada rules are in effect, or SPARK code is allowed to
+      --  violate the SPARK rules.
 
       else
          Process_Call_Ada
@@ -7459,9 +7468,10 @@ package body Sem_Elab is
       elsif Is_Up_Level_Target (Gen_Attrs.Spec_Decl) then
          return;
 
-      --  The SPARK rules are in effect
+      --  The SPARK rules are verified only when -gnatd.v (enforce SPARK
+      --  elaboration rules in SPARK code) is in effect.
 
-      elsif SPARK_Rules_On then
+      elsif SPARK_Rules_On and Debug_Flag_Dot_V then
          Process_Instantiation_SPARK
            (Exp_Inst   => Exp_Inst,
             Inst       => Inst,
@@ -7469,7 +7479,8 @@ package body Sem_Elab is
             Gen_Id     => Gen_Id,
             Gen_Attrs  => Gen_Attrs);
 
-      --  Otherwise the Ada rules are in effect
+      --  Otherwise the Ada rules are in effect, or SPARK code is allowed to
+      --  violate the SPARK rules.
 
       else
          Process_Instantiation_Ada
@@ -7869,7 +7880,10 @@ package body Sem_Elab is
             In_SPARK => SPARK_Rules_On);
       end if;
 
-      --  The SPARK rules are in effect
+      --  The SPARK rules are in effect. These rules are applied regardless of
+      --  whether -gnatd.v (enforce SPARK elaboration rules in SPARK code) is
+      --  in effect because the static model cannot ensure safe assignment of
+      --  variables.
 
       if SPARK_Rules_On then
          Process_Variable_Assignment_SPARK
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index e2bf4b5..f0562ae 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -13249,16 +13249,18 @@ package body Sem_Prag is
                --  If checks are not on we don't want any expansion (since
                --  such expansion would not get properly deleted) but
                --  we do want to analyze (to get proper references).
-               --  The Preanalyze_And_Resolve routine does just what we want
+               --  The Preanalyze_And_Resolve routine does just what we want.
+               --  Ditto if pragma is active, because it will be rewritten
+               --  as an if-statement whose analysis will complete analysis
+               --  and expansion of the string message. This makes a
+               --  difference in the unusual case where the expression for
+               --  the string may have a side effect, such as raising an
+               --  exception. This is mandated by RM 11.4.2, which specifies
+               --  that the string expression is only evaluated if the
+               --  check fails and Assertion_Error is to be raised.
+
+               Preanalyze_And_Resolve (Str, Standard_String);
 
-               if Is_Ignored (N) then
-                  Preanalyze_And_Resolve (Str, Standard_String);
-
-                  --  Otherwise we need a proper analysis and expansion
-
-               else
-                  Analyze_And_Resolve (Str, Standard_String);
-               end if;
             end if;
 
             --  Now you might think we could just do the same with the Boolean
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index e07d6fd..0eefd505 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -13387,7 +13387,7 @@ package body Sem_Util is
                end if;
 
             --  A discriminant check on a selected component may be expanded
-            --  into a dereference when removing side-effects. Recover the
+            --  into a dereference when removing side effects. Recover the
             --  original node and its type, which may be unconstrained.
 
             elsif Nkind (P) = N_Explicit_Dereference
@@ -20648,7 +20648,7 @@ package body Sem_Util is
       --  This construct appears in the context of dispatching calls.
 
       function Reference_To (Obj : Node_Id) return Node_Id;
-      --  An explicit dereference is created when removing side-effects from
+      --  An explicit dereference is created when removing side effects from
       --  expressions for constraint checking purposes. In this case a local
       --  access type is created for it. The correct access level is that of
       --  the original source node. We detect this case by noting that the
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index f7c4c56..c6958cb 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -2276,9 +2276,9 @@ package Sem_Util is
    --      type of the other operand is a descendant of System.Address.
 
    function Number_Of_Elements_In_Array (T : Entity_Id) return Int;
-   --  Returns the number elements in the array T if the index bounds of T is
-   --  known at compile time. If the bounds are not known at compile time, the
-   --  function returns the value zero.
+   --  Returns the number of elements in the array T if the index bounds of T
+   --  is known at compile time. If the bounds are not known at compile time,
+   --  the function returns the value zero.
 
    function Object_Access_Level (Obj : Node_Id) return Uint;
    --  Return the accessibility level of the view of the object Obj. For
diff --git a/gcc/ada/sem_warn.adb b/gcc/ada/sem_warn.adb
index 91f430a..0e498d3 100644
--- a/gcc/ada/sem_warn.adb
+++ b/gcc/ada/sem_warn.adb
@@ -509,7 +509,7 @@ package body Sem_Warn is
             end if;
 
             --  If the condition contains a function call, we consider it may
-            --  be modified by side-effects from a procedure call. Otherwise,
+            --  be modified by side effects from a procedure call. Otherwise,
             --  we consider the condition may not be modified, although that
             --  might happen if Variable is itself a by-reference parameter,
             --  and the procedure called modifies the global object referred to