diff options
author | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2017-10-14 17:07:35 +0000 |
---|---|---|
committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2017-10-14 17:07:35 +0000 |
commit | 92b751fdc698c7b2040f986aaa125e4163003a2d (patch) | |
tree | 9877668163ec28526d8a074dc94e2f8c2e60e565 /gcc/ada | |
parent | 2e60feb59198791c0a3b58838af26e6e5cd32677 (diff) | |
download | gcc-92b751fdc698c7b2040f986aaa125e4163003a2d.zip gcc-92b751fdc698c7b2040f986aaa125e4163003a2d.tar.gz gcc-92b751fdc698c7b2040f986aaa125e4163003a2d.tar.bz2 |
[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
Diffstat (limited to 'gcc/ada')
-rw-r--r-- | gcc/ada/ChangeLog | 36 | ||||
-rw-r--r-- | gcc/ada/cstand.adb | 2 | ||||
-rw-r--r-- | gcc/ada/debug.adb | 9 | ||||
-rw-r--r-- | gcc/ada/doc/gnat_ugn/elaboration_order_handling_in_gnat.rst | 62 | ||||
-rw-r--r-- | gcc/ada/exp_util.adb | 4 | ||||
-rw-r--r-- | gcc/ada/freeze.adb | 2 | ||||
-rw-r--r-- | gcc/ada/gnat_ugn.texi | 88 | ||||
-rw-r--r-- | gcc/ada/layout.adb | 32 | ||||
-rw-r--r-- | gcc/ada/layout.ads | 5 | ||||
-rw-r--r-- | gcc/ada/sem_aggr.adb | 6 | ||||
-rw-r--r-- | gcc/ada/sem_elab.adb | 28 | ||||
-rw-r--r-- | gcc/ada/sem_prag.adb | 20 | ||||
-rw-r--r-- | gcc/ada/sem_util.adb | 4 | ||||
-rw-r--r-- | gcc/ada/sem_util.ads | 6 | ||||
-rw-r--r-- | gcc/ada/sem_warn.adb | 2 |
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 |