From a1e1820b834993a57aa4dbb630e2a09b26667c04 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Tue, 27 Oct 2015 12:12:14 +0100 Subject: [PATCH] [multiple changes] 2015-10-27 Javier Miranda * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Improve previous patch. 2015-10-27 Hristian Kirtchev * sem_ch12.adb (Analyze_Formal_Package_Declaration): Code cleanup. Set and restore the value of global flag Ignore_Pragma_SPARK_Mode. A formal package declaration acts as a package instantation with respect to SPARK_Mode legality. 2015-10-27 Hristian Kirtchev * sem_prag.adb (Check_Constituent_Usage): Use logical operators rather than short circuit operators. Emit an error when a state with visible refinement is not refined. * snames.ads-tmpl: Add names for detecting predefined potentially blocking subprograms. 2015-10-27 Arnaud Charlet * exp_aggr.adb (Aggr_Assignment_OK_For_Backend): Revert previous change. (Expand_Array_Aggregate): Rewrite previous change here as done for other non GCC back-ends. (Build_Record_Aggr_Code): Add special case. From-SVN: r229414 --- gcc/ada/ChangeLog | 27 +++++++++++++++++++ gcc/ada/exp_aggr.adb | 41 +++++++++++++++++++--------- gcc/ada/sem_ch12.adb | 60 ++++++++++++++++++++++++++--------------- gcc/ada/sem_ch6.adb | 2 +- gcc/ada/sem_prag.adb | 13 +++++++-- gcc/ada/snames.ads-tmpl | 23 ++++++++++++++++ 6 files changed, 128 insertions(+), 38 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index ce4195eac36..9b17b2cc668 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,30 @@ +2015-10-27 Javier Miranda + + * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Improve previous patch. + +2015-10-27 Hristian Kirtchev + + * sem_ch12.adb (Analyze_Formal_Package_Declaration): Code cleanup. Set + and restore the value of global flag Ignore_Pragma_SPARK_Mode. A + formal package declaration acts as a package instantation with + respect to SPARK_Mode legality. + +2015-10-27 Hristian Kirtchev + + * sem_prag.adb (Check_Constituent_Usage): Use + logical operators rather than short circuit operators. Emit an + error when a state with visible refinement is not refined. + * snames.ads-tmpl: Add names for detecting + predefined potentially blocking subprograms. + +2015-10-27 Arnaud Charlet + + * exp_aggr.adb (Aggr_Assignment_OK_For_Backend): Revert previous + change. + (Expand_Array_Aggregate): Rewrite previous change here + as done for other non GCC back-ends. + (Build_Record_Aggr_Code): Add special case. + 2015-10-26 Hristian Kirtchev * sem_prag.adb (Add_Item_To_Name_Buffer): Update the comment on usage. diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb index 53f1c91cd17..dbc0d7afdf3 100644 --- a/gcc/ada/exp_aggr.adb +++ b/gcc/ada/exp_aggr.adb @@ -2924,13 +2924,33 @@ package body Exp_Aggr is end if; end if; - Instr := - Make_OK_Assignment_Statement (Loc, - Name => Comp_Expr, - Expression => Expr_Q); + if Generate_C_Code + and then Nkind (Expr_Q) = N_Aggregate + and then Is_Array_Type (Etype (Expr_Q)) + and then Present (First_Index (Etype (Expr_Q))) + then + declare + Expr_Q_Type : constant Node_Id := Etype (Expr_Q); + begin + Append_List_To (L, + Build_Array_Aggr_Code + (N => Expr_Q, + Ctype => Component_Type (Expr_Q_Type), + Index => First_Index (Expr_Q_Type), + Into => Comp_Expr, + Scalar_Comp => Is_Scalar_Type + (Component_Type (Expr_Q_Type)))); + end; + + else + Instr := + Make_OK_Assignment_Statement (Loc, + Name => Comp_Expr, + Expression => Expr_Q); - Set_No_Ctrl_Actions (Instr); - Append_To (L, Instr); + Set_No_Ctrl_Actions (Instr); + Append_To (L, Instr); + end if; -- Adjust the tag if tagged (because of possible view -- conversions), unless compiling for a VM where tags are @@ -4105,8 +4125,6 @@ package body Exp_Aggr is -- Backend processing by Gigi/gcc is possible only if all the following -- conditions are met: - -- 0. We are not generating C code - -- 1. N consists of a single OTHERS choice, possibly recursively -- 2. The array type is not packed @@ -4137,10 +4155,6 @@ package body Exp_Aggr is Nunits : Nat; begin - if Generate_C_Code then - return False; - end if; - -- Recurse as far as possible to find the innermost component type Ctyp := Etype (N); @@ -5476,7 +5490,8 @@ package body Exp_Aggr is if (In_Place_Assign_OK_For_Declaration or else Maybe_In_Place_OK) and then not AAMP_On_Target - and then not Generate_SCIL + and then not CodePeer_Mode + and then not Generate_C_Code and then not Possible_Bit_Aligned_Component (Target) and then not Is_Possibly_Unaligned_Slice (Target) and then Aggr_Assignment_OK_For_Backend (N) diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index eece74ff3d9..61803ed290e 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -2379,22 +2379,17 @@ package body Sem_Ch12 is ---------------------------------------- procedure Analyze_Formal_Package_Declaration (N : Node_Id) is - Loc : constant Source_Ptr := Sloc (N); - Pack_Id : constant Entity_Id := Defining_Identifier (N); - Formal : Entity_Id; - Gen_Id : constant Node_Id := Name (N); - Gen_Decl : Node_Id; - Gen_Unit : Entity_Id; - New_N : Node_Id; - Parent_Installed : Boolean := False; - Renaming : Node_Id; - Parent_Instance : Entity_Id; - Renaming_In_Par : Entity_Id; - Associations : Boolean := True; + Gen_Id : constant Node_Id := Name (N); + Loc : constant Source_Ptr := Sloc (N); + Pack_Id : constant Entity_Id := Defining_Identifier (N); + Formal : Entity_Id; + Gen_Decl : Node_Id; + Gen_Unit : Entity_Id; + Renaming : Node_Id; Vis_Prims_List : Elist_Id := No_Elist; -- List of primitives made temporarily visible in the instantiation - -- to match the visibility of the formal type + -- to match the visibility of the formal type. function Build_Local_Package return Node_Id; -- The formal package is rewritten so that its parameters are replaced @@ -2506,6 +2501,17 @@ package body Sem_Ch12 is return Pack_Decl; end Build_Local_Package; + -- Local variables + + Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode; + -- Save flag Ignore_Pragma_SPARK_Mode for restore on exit + + Associations : Boolean := True; + New_N : Node_Id; + Parent_Installed : Boolean := False; + Parent_Instance : Entity_Id; + Renaming_In_Par : Entity_Id; + -- Start of processing for Analyze_Formal_Package_Declaration begin @@ -2605,19 +2611,18 @@ package body Sem_Ch12 is Formal := New_Copy (Pack_Id); Create_Instantiation_Source (N, Gen_Unit, False, S_Adjustment); - begin - -- Make local generic without formals. The formals will be replaced - -- with internal declarations. + -- Make local generic without formals. The formals will be replaced with + -- internal declarations. + begin New_N := Build_Local_Package; - -- If there are errors in the parameter list, Analyze_Associations - -- raises Instantiation_Error. Patch the declaration to prevent - -- further exception propagation. + -- If there are errors in the parameter list, Analyze_Associations + -- raises Instantiation_Error. Patch the declaration to prevent further + -- exception propagation. exception when Instantiation_Error => - Enter_Name (Formal); Set_Ekind (Formal, E_Variable); Set_Etype (Formal, Any_Type); @@ -2669,6 +2674,15 @@ package body Sem_Ch12 is Append_Entity (Renaming_In_Par, Parent_Instance); end if; + -- A formal package declaration behaves as a package instantiation with + -- respect to SPARK_Mode "off". If the annotation is "off" or altogether + -- missing, set the global flag which signals Analyze_Pragma to ingnore + -- all SPARK_Mode pragmas within the generic_package_name. + + if SPARK_Mode /= On then + Ignore_Pragma_SPARK_Mode := True; + end if; + Analyze (Specification (N)); -- The formals for which associations are provided are not visible @@ -2714,8 +2728,8 @@ package body Sem_Ch12 is Set_Has_Completion (Formal, True); - -- Add semantic information to the original defining identifier. - -- for ASIS use. + -- Add semantic information to the original defining identifier for ASIS + -- use. Set_Ekind (Pack_Id, E_Package); Set_Etype (Pack_Id, Standard_Void_Type); @@ -2726,6 +2740,8 @@ package body Sem_Ch12 is if Has_Aspects (N) then Analyze_Aspect_Specifications (N, Pack_Id); end if; + + Ignore_Pragma_SPARK_Mode := Save_IPSM; end Analyze_Formal_Package_Declaration; --------------------------------- diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 519d7caffb2..85d864a2c0c 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -4062,7 +4062,7 @@ package body Sem_Ch6 is -- that carries the return value. if Present (Cloned_Body_For_C) then - Replace (N, + Rewrite (N, Build_Procedure_Body_Form (Spec_Id, Cloned_Body_For_C)); Analyze (N); end if; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 96f508f641e..8ac388e237f 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -24184,15 +24184,24 @@ package body Sem_Prag is -- A pair of one Input and one Output constituent is a valid -- completion. - elsif In_Seen and then Out_Seen then + elsif In_Seen and Out_Seen then null; -- A single Output constituent is a valid completion only when -- some of the other constituents are missing (SPARK RM 7.2.4(5)). - elsif Has_Missing and then Out_Seen then + elsif Out_Seen and Has_Missing then null; + -- The state lacks a completion + + elsif not In_Seen and not In_Out_Seen and not Out_Seen then + SPARK_Msg_NE + ("missing global refinement of state &", N, State_Id); + + -- Otherwise the state has a malformed completion where at least + -- one of the constituents has a different mode. + else SPARK_Msg_NE ("global refinement of state & redefines the mode of its " diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index 76d8028252c..ba4053dab51 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -261,6 +261,29 @@ package Snames is Name_Wide_Text_IO : constant Name_Id := N + $; Name_Wide_Wide_Text_IO : constant Name_Id := N + $; + -- Names for detecting predefined potentially blocking subprograms + + Name_Abort_Task : constant Name_Id := N + $; + Name_Bounded_IO : constant Name_Id := N + $; + Name_C_Streams : constant Name_Id := N + $; + Name_Complex_IO : constant Name_Id := N + $; + Name_Directories : constant Name_Id := N + $; + Name_Direct_IO : constant Name_Id := N + $; + Name_Dispatching : constant Name_Id := N + $; + Name_Editing : constant Name_Id := N + $; + Name_EDF : constant Name_Id := N + $; + Name_Reset_Standard_Files : constant Name_Id := N + $; + Name_Sequential_IO : constant Name_Id := N + $; + Name_Streams : constant Name_Id := N + $; + Name_Suspend_Until_True : constant Name_Id := N + $; + Name_Suspend_Until_True_And_Set_Deadline : constant Name_Id := N + $; + Name_Synchronous_Barriers : constant Name_Id := N + $; + Name_Task_Identification : constant Name_Id := N + $; + Name_Text_Streams : constant Name_Id := N + $; + Name_Unbounded_IO : constant Name_Id := N + $; + Name_Wait_For_Release : constant Name_Id := N + $; + Name_Yield : constant Name_Id := N + $; + -- Names of implementations of the distributed systems annex First_PCS_Name : constant Name_Id := N + $; -- 2.30.2