From f71b4cd44483310677019f5d47cabbdeedfcfc75 Mon Sep 17 00:00:00 2001 From: Pierre-Marie de Rodat Date: Mon, 25 Sep 2017 09:24:26 +0000 Subject: [PATCH] [multiple changes] 2017-09-25 Hristian Kirtchev * sem_res.adb (Replace_Actual_Discriminants): Replace a discriminant for GNATprove. (Resolve_Entry): Clean up predicate 2017-09-25 Hristian Kirtchev * sem_prag.adb (Analyze_Constituent): Raise Unrecoverable_Error rather than Program_Error because U_E is more in line with respect to the intended behavior. 2017-09-25 Ed Schonberg * sem_ch13.adb (Resolve_Aspect_Expressions): The expression for aspect Storage_Size does not freeze, and thus can include references to deferred constants. 2017-09-25 Hristian Kirtchev * exp_spark.adb (Expand_SPARK_Potential_Renaming): Do not process a reference when it appears within a pragma of no significance to SPARK. (In_Insignificant_Pragma): New routine. * sem_prag.ads: Add new table Pragma_Significant_In_SPARK. 2017-09-25 Ed Schonberg * sem_ch12.adb (Analyze_Associations, case N_Formal_Package): If the actual is a renaming, indicate that it is the renamed package that must be frozen before the instantiation. 2017-09-25 Yannick Moy * doc/gnat_ugn/gnat_and_program_execution.rst: Fix typo in description of dimensionality system in GNAT UG. * gnat_ugn.texi: Regenerate. 2017-09-25 Yannick Moy * gnat1drv.adb: Call Check_Safe_Pointers from the frontend in GNATprove_Mode when switch -gnatdF used. 2017-09-25 Piotr Trojanek * adabkend.adb (Call_Back_End): Reset Current_Error_Node when starting the backend. From-SVN: r253140 --- gcc/ada/ChangeLog | 47 ++++++++++ gcc/ada/adabkend.adb | 10 ++- .../gnat_ugn/gnat_and_program_execution.rst | 18 ++-- gcc/ada/exp_imgv.adb | 18 ++-- gcc/ada/exp_spark.adb | 46 +++++++++- gcc/ada/gnat1drv.adb | 58 ++++++------- gcc/ada/gnat_ugn.texi | 6 +- gcc/ada/libgnarl/s-taprop__linux.adb | 86 +++++++++++++------ gcc/ada/sem_ch12.adb | 18 +++- gcc/ada/sem_ch13.adb | 8 ++ gcc/ada/sem_prag.adb | 4 +- gcc/ada/sem_prag.ads | 19 ++++ gcc/ada/sem_res.adb | 32 ++++--- 13 files changed, 275 insertions(+), 95 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 44ce6dbad70..3780b1db1b2 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,50 @@ +2017-09-25 Hristian Kirtchev + + * sem_res.adb (Replace_Actual_Discriminants): Replace a discriminant + for GNATprove. + (Resolve_Entry): Clean up predicate + +2017-09-25 Hristian Kirtchev + + * sem_prag.adb (Analyze_Constituent): Raise Unrecoverable_Error rather + than Program_Error because U_E is more in line with respect to the + intended behavior. + +2017-09-25 Ed Schonberg + + * sem_ch13.adb (Resolve_Aspect_Expressions): The expression for aspect + Storage_Size does not freeze, and thus can include references to + deferred constants. + +2017-09-25 Hristian Kirtchev + + * exp_spark.adb (Expand_SPARK_Potential_Renaming): Do not process a + reference when it appears within a pragma of no significance to SPARK. + (In_Insignificant_Pragma): New routine. + * sem_prag.ads: Add new table Pragma_Significant_In_SPARK. + +2017-09-25 Ed Schonberg + + * sem_ch12.adb (Analyze_Associations, case N_Formal_Package): If the + actual is a renaming, indicate that it is the renamed package that must + be frozen before the instantiation. + +2017-09-25 Yannick Moy + + * doc/gnat_ugn/gnat_and_program_execution.rst: Fix typo in description + of dimensionality system in GNAT UG. + * gnat_ugn.texi: Regenerate. + +2017-09-25 Yannick Moy + + * gnat1drv.adb: Call Check_Safe_Pointers from the frontend in + GNATprove_Mode when switch -gnatdF used. + +2017-09-25 Piotr Trojanek + + * adabkend.adb (Call_Back_End): Reset Current_Error_Node when starting + the backend. + 2017-09-25 Javier Miranda * exp_imgv.adb (Expand_Image_Attribute): Disable the optimized diff --git a/gcc/ada/adabkend.adb b/gcc/ada/adabkend.adb index 7eee8879019..3c84a483a58 100644 --- a/gcc/ada/adabkend.adb +++ b/gcc/ada/adabkend.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 2001-2016, AdaCore -- +-- Copyright (C) 2001-2017, AdaCore -- -- -- -- 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- -- @@ -22,6 +22,7 @@ -- This is the version of the Back_End package for back ends written in Ada +with Atree; use Atree; with Debug; with Lib; with Opt; use Opt; @@ -56,6 +57,13 @@ package body Adabkend is Write_Eol; end if; + -- Frontend leaves the Current_Error_Node at a location that is + -- meaningless and confusing when emitting bugboxes from the backed. By + -- resetting it here we default to "No source file position information + -- available" message on backend crashes. + + Current_Error_Node := Empty; + Driver (Lib.Cunit (Types.Main_Unit)); end Call_Back_End; diff --git a/gcc/ada/doc/gnat_ugn/gnat_and_program_execution.rst b/gcc/ada/doc/gnat_ugn/gnat_and_program_execution.rst index 952cc3d803c..68117ae2c49 100644 --- a/gcc/ada/doc/gnat_ugn/gnat_and_program_execution.rst +++ b/gcc/ada/doc/gnat_ugn/gnat_and_program_execution.rst @@ -3513,7 +3513,7 @@ However, incorrect assignments such as: .. code-block:: ada Distance := 5.0; - Distance := 5.0 * kg: + Distance := 5.0 * kg; are rejected with the following diagnoses: @@ -3556,7 +3556,7 @@ aspect. .. index:: Dimension Vector (for a dimensioned subtype) .. index:: Dimension aspect .. index:: Dimension_System aspect - + The ``Dimension`` aspect of a dimensioned subtype ``S`` defines a mapping from the base type's Unit_Names to integer (or, more generally, rational) values. This mapping is the *dimension vector* (also referred to as the @@ -3575,8 +3575,8 @@ means that the unit is not used. For example: end; Here ``DV(Acc)`` = ``DV(Acceleration)`` = -``(Meter=>1, Kilogram=>0, Second => -2, Ampere=>0, Kelvin=>0, Mole=>0, Candela => 0)``. -Symbolically, we can express this as ``Meter / Second**2``. +``(Meter=>1, Kilogram=>0, Second=>-2, Ampere=>0, Kelvin=>0, Mole=>0, Candela=>0)``. +Symbolically, we can express this as ``Meter / Second**2``. The dimension vector of an arithmetic expression is synthesized from the dimension vectors of its components, with compile-time dimensionality checks @@ -3593,7 +3593,7 @@ mathematical definitions for the vector operations that are used: * :samp:`DV({op expr})`, where *op* is a unary operator, is :samp:`DV({expr})` * :samp:`DV({expr1 op expr2})` where *op* is "+" or "-" is :samp:`DV({expr1})` - provided that :samp:`DV({expr1})` = :samp:`DV({expr2})`. + provided that :samp:`DV({expr1})` = :samp:`DV({expr2})`. If this condition is not met then the construct is illegal. * :samp:`DV({expr1} * {expr2})` is :samp:`DV({expr1})` + :samp:`DV({expr2})`, @@ -3624,7 +3624,7 @@ is equivalent to acc-10.0 > 0.0 and is thus illegal. Analogously a conditional expression -requires the same dimension vector for each branch. +requires the same dimension vector for each branch. The dimension vector of a type conversion :samp:`T({expr})` is defined as follows, based on the nature of ``T``: @@ -3648,7 +3648,7 @@ as follows, based on the nature of ``T``: Thus, if *expr* is of a dimensioned subtype of ``T``, the conversion may be regarded as a "view conversion" that preserves dimensionality. - This rule makes it possible to write generic code that can be instantiated + This rule makes it possible to write generic code that can be instantiated with compatible dimensioned subtypes. The generic unit will contain conversions that will consequently be present in instantiations, but conversions to the base type will preserve dimensionality and make it @@ -3663,10 +3663,10 @@ as follows, based on the nature of ``T``: The dimension vector for a type qualification :samp:`T'({expr})` is the same as for the type conversion :samp:`T({expr})`. -An assignment statement +An assignment statement .. code-block:: ada - + Source := Target; requires ``DV(Source)`` = ``DV(Target)``, and analogously for parameter diff --git a/gcc/ada/exp_imgv.adb b/gcc/ada/exp_imgv.adb index 0a400ec4313..78777075d8b 100644 --- a/gcc/ada/exp_imgv.adb +++ b/gcc/ada/exp_imgv.adb @@ -268,14 +268,14 @@ package body Exp_Imgv is Expr : constant Node_Id := Relocate_Node (First (Exprs)); Pref : constant Node_Id := Prefix (N); - function Is_User_Defined_Enumeration_Type - (Typ : Entity_Id) return Boolean; - -- Return True if Typ is a user-defined enumeration type - procedure Expand_User_Defined_Enumeration_Image; -- Expand attribute 'Image in user-defined enumeration types, avoiding -- string copy. + function Is_User_Defined_Enumeration_Type + (Typ : Entity_Id) return Boolean; + -- Return True if Typ is a user-defined enumeration type + ------------------------------------------- -- Expand_User_Defined_Enumeration_Image -- ------------------------------------------- @@ -307,7 +307,7 @@ package body Exp_Imgv is Object_Definition => New_Occurrence_Of (Standard_Natural, Loc), Constant_Present => True, - Expression => + Expression => Convert_To (Standard_Natural, Make_Attribute_Reference (Loc, Attribute_Name => Name_Pos, @@ -323,7 +323,7 @@ package body Exp_Imgv is Object_Definition => New_Occurrence_Of (Standard_Natural, Loc), Constant_Present => True, - Expression => + Expression => Convert_To (Standard_Natural, Make_Indexed_Component (Loc, Prefix => @@ -347,7 +347,7 @@ package body Exp_Imgv is Object_Definition => New_Occurrence_Of (Standard_Natural, Loc), Constant_Present => True, - Expression => + Expression => Convert_To (Standard_Natural, Make_Indexed_Component (Loc, Prefix => @@ -412,8 +412,8 @@ package body Exp_Imgv is Insert_Actions (N, Ins_List, Suppress => All_Checks); Rewrite (N, - Unchecked_Convert_To (S1_Id, - New_Occurrence_Of (P4_Id, Loc))); + Unchecked_Convert_To (S1_Id, New_Occurrence_Of (P4_Id, Loc))); + Analyze_And_Resolve (N, Standard_String); end Expand_User_Defined_Enumeration_Image; diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb index 211fea360cd..d4b9436959f 100644 --- a/gcc/ada/exp_spark.adb +++ b/gcc/ada/exp_spark.adb @@ -36,6 +36,7 @@ with Nmake; use Nmake; with Rtsfind; use Rtsfind; with Sem; use Sem; with Sem_Eval; use Sem_Eval; +with Sem_Prag; use Sem_Prag; with Sem_Res; use Sem_Res; with Sem_Util; use Sem_Util; with Sinfo; use Sinfo; @@ -368,11 +369,46 @@ package body Exp_SPARK is ------------------------------------- procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is + function In_Insignificant_Pragma (Nod : Node_Id) return Boolean; + -- Determine whether arbitrary node Nod appears within a significant + -- pragma for SPARK. + + ----------------------------- + -- In_Insignificant_Pragma -- + ----------------------------- + + function In_Insignificant_Pragma (Nod : Node_Id) return Boolean is + Par : Node_Id; + + begin + -- Climb the parent chain looking for an enclosing pragma + + Par := Nod; + while Present (Par) loop + if Nkind (Par) = N_Pragma then + return not Pragma_Significant_In_SPARK (Get_Pragma_Id (Par)); + + -- Prevent the search from going too far + + elsif Is_Body_Or_Package_Declaration (Par) then + exit; + end if; + + Par := Parent (Par); + end loop; + + return False; + end In_Insignificant_Pragma; + + -- Local variables + Loc : constant Source_Ptr := Sloc (N); Obj_Id : constant Entity_Id := Entity (N); Typ : constant Entity_Id := Etype (N); Ren : Node_Id; + -- Start of processing for Expand_SPARK_Potential_Renaming + begin -- Replace a reference to a renaming with the actual renamed object @@ -381,12 +417,20 @@ package body Exp_SPARK is if Present (Ren) then + -- Do not process a reference when it appears within a pragma of + -- no significance to SPARK. It is assumed that the replacement + -- will violate the semantics of the pragma and cause a spurious + -- error. + + if In_Insignificant_Pragma (N) then + return; + -- Instantiations and inlining of subprograms employ "prologues" -- which map actual to formal parameters by means of renamings. -- Replace a reference to a formal by the corresponding actual -- parameter. - if Nkind (Ren) in N_Entity then + elsif Nkind (Ren) in N_Entity then Rewrite (N, New_Occurrence_Of (Ren, Loc)); -- Otherwise the renamed object denotes a name diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index b493d53115a..c3377da4834 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -23,36 +23,36 @@ -- -- ------------------------------------------------------------------------------ -with Atree; use Atree; -with Back_End; use Back_End; +with Atree; use Atree; +with Back_End; use Back_End; with Checks; with Comperr; -with Csets; use Csets; -with Debug; use Debug; +with Csets; use Csets; +with Debug; use Debug; with Elists; -with Errout; use Errout; +with Errout; use Errout; with Exp_CG; with Fmap; -with Fname; use Fname; -with Fname.UF; use Fname.UF; +with Fname; use Fname; +with Fname.UF; use Fname.UF; with Frontend; -with Ghost; use Ghost; -with Gnatvsn; use Gnatvsn; +with Ghost; use Ghost; +with Gnatvsn; use Gnatvsn; with Inline; -with Lib; use Lib; -with Lib.Writ; use Lib.Writ; +with Lib; use Lib; +with Lib.Writ; use Lib.Writ; with Lib.Xref; -with Namet; use Namet; +with Namet; use Namet; with Nlists; -with Opt; use Opt; -with Osint; use Osint; -with Osint.C; use Osint.C; -with Output; use Output; +with Opt; use Opt; +with Osint; use Osint; +with Osint.C; use Osint.C; +with Output; use Output; with Par_SCO; with Prepcomp; -with Repinfo; use Repinfo; +with Repinfo; use Repinfo; with Restrict; -with Rident; use Rident; +with Rident; use Rident; with Rtsfind; with SCOs; with Sem; @@ -64,23 +64,23 @@ with Sem_Eval; with Sem_SPARK; use Sem_SPARK; with Sem_Type; with Set_Targ; -with Sinfo; use Sinfo; -with Sinput.L; use Sinput.L; -with Snames; use Snames; -with Sprint; use Sprint; +with Sinfo; use Sinfo; +with Sinput.L; use Sinput.L; +with Snames; use Snames; +with Sprint; use Sprint; with Stringt; -with Stylesw; use Stylesw; -with Targparm; use Targparm; +with Stylesw; use Stylesw; +with Targparm; use Targparm; with Tbuild; with Tree_Gen; -with Treepr; use Treepr; +with Treepr; use Treepr; with Ttypes; -with Types; use Types; -with Uintp; use Uintp; -with Uname; use Uname; +with Types; use Types; +with Uintp; use Uintp; +with Uname; use Uname; with Urealp; with Usage; -with Validsw; use Validsw; +with Validsw; use Validsw; with System.Assertions; with System.OS_Lib; diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi index a572de0543b..22d6f1469ec 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 , Sep 13, 2017 +GNAT User's Guide for Native Platforms , Sep 25, 2017 AdaCore @@ -22773,7 +22773,7 @@ However, incorrect assignments such as: @example Distance := 5.0; -Distance := 5.0 * kg: +Distance := 5.0 * kg; @end example @end quotation @@ -22854,7 +22854,7 @@ end; @end quotation Here @code{DV(Acc)} = @code{DV(Acceleration)} = -@code{(Meter=>1, Kilogram=>0, Second => -2, Ampere=>0, Kelvin=>0, Mole=>0, Candela => 0)}. +@code{(Meter=>1, Kilogram=>0, Second=>-2, Ampere=>0, Kelvin=>0, Mole=>0, Candela=>0)}. Symbolically, we can express this as @code{Meter / Second**2}. The dimension vector of an arithmetic expression is synthesized from the diff --git a/gcc/ada/libgnarl/s-taprop__linux.adb b/gcc/ada/libgnarl/s-taprop__linux.adb index 77fe26f0b72..1dfcf39dd81 100644 --- a/gcc/ada/libgnarl/s-taprop__linux.adb +++ b/gcc/ada/libgnarl/s-taprop__linux.adb @@ -191,6 +191,10 @@ package body System.Task_Primitives.Operations is -- Note well: If this function or related code is modified, it should be -- tested by hand, because automated testing doesn't exercise it. + ------------------------- + -- Get_Ceiling_Support -- + ------------------------- + function Get_Ceiling_Support return Boolean is Ceiling_Support : Boolean := False; begin @@ -271,22 +275,40 @@ package body System.Task_Primitives.Operations is ---------------------------------- function Compute_Base_Monotonic_Clock return Duration is - TS_Bef0, TS_Mon0, TS_Aft0 : aliased timespec; - TS_Bef, TS_Mon, TS_Aft : aliased timespec; - Bef, Mon, Aft : Duration; - Res_B, Res_M, Res_A : Interfaces.C.int; + Aft : Duration; + Bef : Duration; + Mon : Duration; + Res_A : Interfaces.C.int; + Res_B : Interfaces.C.int; + Res_M : Interfaces.C.int; + TS_Aft : aliased timespec; + TS_Aft0 : aliased timespec; + TS_Bef : aliased timespec; + TS_Bef0 : aliased timespec; + TS_Mon : aliased timespec; + TS_Mon0 : aliased timespec; + begin - Res_B := clock_gettime - (clock_id => OSC.CLOCK_REALTIME, tp => TS_Bef0'Unchecked_Access); + Res_B := + clock_gettime + (clock_id => OSC.CLOCK_REALTIME, + tp => TS_Bef0'Unchecked_Access); pragma Assert (Res_B = 0); - Res_M := clock_gettime - (clock_id => OSC.CLOCK_RT_Ada, tp => TS_Mon0'Unchecked_Access); + + Res_M := + clock_gettime + (clock_id => OSC.CLOCK_RT_Ada, + tp => TS_Mon0'Unchecked_Access); pragma Assert (Res_M = 0); - Res_A := clock_gettime - (clock_id => OSC.CLOCK_REALTIME, tp => TS_Aft0'Unchecked_Access); + + Res_A := + clock_gettime + (clock_id => OSC.CLOCK_REALTIME, + tp => TS_Aft0'Unchecked_Access); pragma Assert (Res_A = 0); for I in 1 .. 10 loop + -- Guard against a leap second that will cause CLOCK_REALTIME to jump -- backwards. In the extrenmely unlikely event we call clock_gettime -- before and after the jump the epoch, the result will be off @@ -296,25 +318,36 @@ package body System.Task_Primitives.Operations is -- Also try to calculate the most accurate epoch by taking the -- minimum difference of 10 tries. - Res_B := clock_gettime - (clock_id => OSC.CLOCK_REALTIME, tp => TS_Bef'Unchecked_Access); + Res_B := + clock_gettime + (clock_id => OSC.CLOCK_REALTIME, + tp => TS_Bef'Unchecked_Access); pragma Assert (Res_B = 0); - Res_M := clock_gettime - (clock_id => OSC.CLOCK_RT_Ada, tp => TS_Mon'Unchecked_Access); + + Res_M := + clock_gettime + (clock_id => OSC.CLOCK_RT_Ada, + tp => TS_Mon'Unchecked_Access); pragma Assert (Res_M = 0); - Res_A := clock_gettime - (clock_id => OSC.CLOCK_REALTIME, tp => TS_Aft'Unchecked_Access); + + Res_A := + clock_gettime + (clock_id => OSC.CLOCK_REALTIME, + tp => TS_Aft'Unchecked_Access); pragma Assert (Res_A = 0); - if (TS_Bef0.tv_sec /= TS_Aft0.tv_sec and then - TS_Bef.tv_sec = TS_Aft.tv_sec) - -- The calls to clock_gettime before the loop were no good - or else - (TS_Bef0.tv_sec = TS_Aft0.tv_sec and then - TS_Bef.tv_sec = TS_Aft.tv_sec and then - (TS_Aft.tv_nsec - TS_Bef.tv_nsec < - TS_Aft0.tv_nsec - TS_Bef0.tv_nsec)) - -- The most recent calls to clock_gettime were better + -- The calls to clock_gettime before the loop were no good + + if (TS_Bef0.tv_sec /= TS_Aft0.tv_sec + and then TS_Bef.tv_sec = TS_Aft.tv_sec) + + -- The most recent calls to clock_gettime were better + + or else + (TS_Bef0.tv_sec = TS_Aft0.tv_sec + and then TS_Bef.tv_sec = TS_Aft.tv_sec + and then (TS_Aft.tv_nsec - TS_Bef.tv_nsec + < TS_Aft0.tv_nsec - TS_Bef0.tv_nsec)) then TS_Bef0 := TS_Bef; TS_Aft0 := TS_Aft; @@ -326,8 +359,9 @@ package body System.Task_Primitives.Operations is Mon := To_Duration (TS_Mon0); Aft := To_Duration (TS_Aft0); - return Bef / 2 + Aft / 2 - Mon; -- Distribute the division, to avoid potential type overflow someday + + return Bef / 2 + Aft / 2 - Mon; end Compute_Base_Monotonic_Clock; -------------- diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 9a87c0eb562..44dc80100ad 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -1980,8 +1980,22 @@ package body Sem_Ch12 is if Needs_Freezing then Check_Generic_Parent; - Set_Has_Delayed_Freeze (Actual); - Append_Elmt (Actual, Actuals_To_Freeze); + + -- If the actual is a renaming of a proper + -- instance of the formal package, indicate + -- that it is the instance that must be frozen. + + if Nkind (Parent (Actual)) = + N_Package_Renaming_Declaration + then + Set_Has_Delayed_Freeze + (Renamed_Entity (Actual)); + Append_Elmt + (Renamed_Entity (Actual), Actuals_To_Freeze); + else + Set_Has_Delayed_Freeze (Actual); + Append_Elmt (Actual, Actuals_To_Freeze); + end if; end if; end if; end Explicit_Freeze_Check; diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index a352f3c8bde..04ed408f45c 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -12912,6 +12912,14 @@ package body Sem_Ch13 is Set_Must_Not_Freeze (Expr); Preanalyze_Spec_Expression (Expr, E); + -- Ditto for Storage_Size. Any other aspects that carry + -- expressions that should not freeze ??? This is only + -- relevant to the misuse of deferred constants. + + when Aspect_Storage_Size => + Set_Must_Not_Freeze (Expr); + Preanalyze_Spec_Expression (Expr, Any_Integer); + when others => if Present (Expr) then case Aspect_Argument (A_Id) is diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 417de9267df..59bbdb5f0ab 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -13219,7 +13219,7 @@ package body Sem_Prag is Analyze (N); raise Pragma_Exit; - -- No other possibilities + -- No other possibilities when others => raise Program_Error; @@ -27448,7 +27448,7 @@ package body Sem_Prag is -- Stop the compilation, as this leads to a multitude -- of misleading cascaded errors. - raise Program_Error; + raise Unrecoverable_Error; end if; -- The constituent is a valid state or object diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index ff4a1cba043..33dbe488ae1 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -175,6 +175,25 @@ package Sem_Prag is Pragma_Warnings => True, others => False); + -- The following table lists all pragmas which are significant in SPARK and + -- as a result get translated into verification conditions. The table is an + -- amalgamation of the pragmas listed in SPARK RM 16.1 and internally added + -- entries. + + Pragma_Significant_In_SPARK : constant array (Pragma_Id) of Boolean := + (Pragma_All_Calls_Remote => False, + Pragma_Asynchronous => False, + Pragma_Default_Storage_Pool => False, + Pragma_Discard_Names => False, + Pragma_Dispatching_Domain => False, + Pragma_Priority_Specific_Dispatching => False, + Pragma_Remote_Call_Interface => False, + Pragma_Remote_Types => False, + Pragma_Shared_Passive => False, + Pragma_Task_Dispatching_Policy => False, + Pragma_Warnings => False, + others => True); + ----------------- -- Subprograms -- ----------------- diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index ada86c2af74..5087fe62f67 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -1837,7 +1837,17 @@ package body Sem_Res is -- Start of processing for Replace_Actual_Discriminants begin - if not Expander_Active then + if Expander_Active then + null; + + -- Allow the replacement of concurrent discriminants in GNATprove even + -- though this is a light expansion activity. Note that generic units + -- are not modified. + + elsif GNATprove_Mode and not Inside_A_Generic then + null; + + else return; end if; @@ -1848,9 +1858,7 @@ package body Sem_Res is Tsk := Prefix (Prefix (Name (N))); end if; - if No (Tsk) then - return; - else + if Present (Tsk) then Replace_Discrs (Default); end if; end Replace_Actual_Discriminants; @@ -3561,6 +3569,7 @@ package body Sem_Res is Rewrite (Actval, Make_Raise_Constraint_Error (Loc, Reason => CE_Range_Check_Failed)); + Set_Raises_Constraint_Error (Actval); Set_Etype (Actval, Etype (F)); end if; @@ -3568,12 +3577,12 @@ package body Sem_Res is Assoc := Make_Parameter_Association (Loc, Explicit_Actual_Parameter => Actval, - Selector_Name => Make_Identifier (Loc, Chars (F))); + Selector_Name => Make_Identifier (Loc, Chars (F))); -- Case of insertion is first named actual - if No (Prev) or else - Nkind (Parent (Prev)) /= N_Parameter_Association + if No (Prev) + or else Nkind (Parent (Prev)) /= N_Parameter_Association then Set_Next_Named_Actual (Assoc, First_Named_Actual (N)); Set_First_Named_Actual (N, Actval); @@ -7474,13 +7483,10 @@ package body Sem_Res is Index := First (Expressions (Entry_Name)); Resolve (Index, Entry_Index_Type (Nam)); - -- Generate a reference for the index entity when the index is not a - -- literal. + -- Generate a reference for the index when it denotes an entity - if Nkind (Index) in N_Has_Entity - and then Nkind (Entity (Index)) in N_Entity - then - Generate_Reference (Entity (Index), Nam, ' '); + if Is_Entity_Name (Index) then + Generate_Reference (Entity (Index), Nam); end if; -- Up to this point the expression could have been the actual in a -- 2.30.2