From 265ca04aba7ca04a86809b1adf88217c091d42e8 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Fri, 23 Oct 2015 12:49:44 +0200 Subject: [PATCH] [multiple changes] 2015-10-23 Ed Schonberg * sem_dim.adb (Analyze_Dimension_Extension_Or_Record_Aggregate): Handle properly a box-initialized aggregate component. 2015-10-23 Yannick Moy * sem_prag.adb (Analyze_Pragma): Reject Volatile_Function not placed on a function. 2015-10-23 Yannick Moy * a-extiin.ads, a-reatim.ads, a-interr.ads, a-exetim-mingw.ads, a-exetim-default.ads, a-exetim.ads, a-taside.ads: Add "Global => null" contract on subprograms. * lib-xref-spark_specific.adb: collect scopes for stubs of protected objects 2015-10-23 Arnaud Charlet * gnat1drv.adb (Adjust_Global_Switches): Enable Back_Annotate_Rep_Info to get size information from gigi. (Gnat1drv): Code clean ups. * frontend.adb (Frontend): Ditto. From-SVN: r229231 --- gcc/ada/ChangeLog | 25 +++++++ gcc/ada/a-exetim-default.ads | 36 +++++++--- gcc/ada/a-exetim-mingw.ads | 32 ++++++--- gcc/ada/a-exetim.ads | 36 +++++++--- gcc/ada/a-extiin.ads | 4 +- gcc/ada/a-interr.ads | 12 ++-- gcc/ada/a-reatim.ads | 103 ++++++++++++++++++---------- gcc/ada/a-taside.ads | 12 ++-- gcc/ada/gnat1drv.adb | 9 +++ gcc/ada/lib-xref-spark_specific.adb | 23 ++++++- gcc/ada/sem_dim.adb | 7 +- gcc/ada/sem_prag.adb | 5 ++ 12 files changed, 227 insertions(+), 77 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index b66d29ff12b..9a521162c7f 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,28 @@ +2015-10-23 Ed Schonberg + + * sem_dim.adb (Analyze_Dimension_Extension_Or_Record_Aggregate): + Handle properly a box-initialized aggregate component. + +2015-10-23 Yannick Moy + + * sem_prag.adb (Analyze_Pragma): Reject Volatile_Function not placed + on a function. + +2015-10-23 Yannick Moy + + * a-extiin.ads, a-reatim.ads, a-interr.ads, a-exetim-mingw.ads, + a-exetim-default.ads, a-exetim.ads, a-taside.ads: Add "Global => null" + contract on subprograms. + * lib-xref-spark_specific.adb: collect scopes for stubs of + protected objects + +2015-10-23 Arnaud Charlet + + * gnat1drv.adb (Adjust_Global_Switches): Enable + Back_Annotate_Rep_Info to get size information from gigi. + (Gnat1drv): Code clean ups. + * frontend.adb (Frontend): Ditto. + 2015-10-23 Arnaud Charlet * gnat1drv.adb (Adjust_Global_Switches): Adjust settings. diff --git a/gcc/ada/a-exetim-default.ads b/gcc/ada/a-exetim-default.ads index c1ccda5a694..5877fc535fe 100644 --- a/gcc/ada/a-exetim-default.ads +++ b/gcc/ada/a-exetim-default.ads @@ -57,34 +57,50 @@ is function "+" (Left : CPU_Time; - Right : Ada.Real_Time.Time_Span) return CPU_Time; + Right : Ada.Real_Time.Time_Span) return CPU_Time + with + Global => null; function "+" (Left : Ada.Real_Time.Time_Span; - Right : CPU_Time) return CPU_Time; + Right : CPU_Time) return CPU_Time + with + Global => null; function "-" (Left : CPU_Time; - Right : Ada.Real_Time.Time_Span) return CPU_Time; + Right : Ada.Real_Time.Time_Span) return CPU_Time + with + Global => null; function "-" (Left : CPU_Time; - Right : CPU_Time) return Ada.Real_Time.Time_Span; + Right : CPU_Time) return Ada.Real_Time.Time_Span + with + Global => null; - function "<" (Left, Right : CPU_Time) return Boolean; - function "<=" (Left, Right : CPU_Time) return Boolean; - function ">" (Left, Right : CPU_Time) return Boolean; - function ">=" (Left, Right : CPU_Time) return Boolean; + function "<" (Left, Right : CPU_Time) return Boolean with + Global => null; + function "<=" (Left, Right : CPU_Time) return Boolean with + Global => null; + function ">" (Left, Right : CPU_Time) return Boolean with + Global => null; + function ">=" (Left, Right : CPU_Time) return Boolean with + Global => null; procedure Split (T : CPU_Time; SC : out Ada.Real_Time.Seconds_Count; - TS : out Ada.Real_Time.Time_Span); + TS : out Ada.Real_Time.Time_Span) + with + Global => null; function Time_Of (SC : Ada.Real_Time.Seconds_Count; TS : Ada.Real_Time.Time_Span := Ada.Real_Time.Time_Span_Zero) - return CPU_Time; + return CPU_Time + with + Global => null; Interrupt_Clocks_Supported : constant Boolean := False; Separate_Interrupt_Clocks_Supported : constant Boolean := False; diff --git a/gcc/ada/a-exetim-mingw.ads b/gcc/ada/a-exetim-mingw.ads index 8dcd32018b3..8e1e764e50b 100644 --- a/gcc/ada/a-exetim-mingw.ads +++ b/gcc/ada/a-exetim-mingw.ads @@ -59,34 +59,48 @@ is function "+" (Left : CPU_Time; - Right : Ada.Real_Time.Time_Span) return CPU_Time; + Right : Ada.Real_Time.Time_Span) return CPU_Time + with + Global => null; function "+" (Left : Ada.Real_Time.Time_Span; - Right : CPU_Time) return CPU_Time; + Right : CPU_Time) return CPU_Time + with + Global => null; function "-" (Left : CPU_Time; - Right : Ada.Real_Time.Time_Span) return CPU_Time; + Right : Ada.Real_Time.Time_Span) return CPU_Time + with + Global => null; function "-" (Left : CPU_Time; Right : CPU_Time) return Ada.Real_Time.Time_Span; - function "<" (Left, Right : CPU_Time) return Boolean; - function "<=" (Left, Right : CPU_Time) return Boolean; - function ">" (Left, Right : CPU_Time) return Boolean; - function ">=" (Left, Right : CPU_Time) return Boolean; + function "<" (Left, Right : CPU_Time) return Boolean with + Global => null; + function "<=" (Left, Right : CPU_Time) return Boolean with + Global => null; + function ">" (Left, Right : CPU_Time) return Boolean with + Global => null; + function ">=" (Left, Right : CPU_Time) return Boolean with + Global => null; procedure Split (T : CPU_Time; SC : out Ada.Real_Time.Seconds_Count; - TS : out Ada.Real_Time.Time_Span); + TS : out Ada.Real_Time.Time_Span) + with + Global => null; function Time_Of (SC : Ada.Real_Time.Seconds_Count; TS : Ada.Real_Time.Time_Span := Ada.Real_Time.Time_Span_Zero) - return CPU_Time; + return CPU_Time + with + Global => null; Interrupt_Clocks_Supported : constant Boolean := False; Separate_Interrupt_Clocks_Supported : constant Boolean := False; diff --git a/gcc/ada/a-exetim.ads b/gcc/ada/a-exetim.ads index 54a9b41fe85..951c3ed09e9 100644 --- a/gcc/ada/a-exetim.ads +++ b/gcc/ada/a-exetim.ads @@ -48,34 +48,50 @@ is function "+" (Left : CPU_Time; - Right : Ada.Real_Time.Time_Span) return CPU_Time; + Right : Ada.Real_Time.Time_Span) return CPU_Time + with + Global => null; function "+" (Left : Ada.Real_Time.Time_Span; - Right : CPU_Time) return CPU_Time; + Right : CPU_Time) return CPU_Time + with + Global => null; function "-" (Left : CPU_Time; - Right : Ada.Real_Time.Time_Span) return CPU_Time; + Right : Ada.Real_Time.Time_Span) return CPU_Time + with + Global => null; function "-" (Left : CPU_Time; - Right : CPU_Time) return Ada.Real_Time.Time_Span; + Right : CPU_Time) return Ada.Real_Time.Time_Span + with + Global => null; - function "<" (Left, Right : CPU_Time) return Boolean; - function "<=" (Left, Right : CPU_Time) return Boolean; - function ">" (Left, Right : CPU_Time) return Boolean; - function ">=" (Left, Right : CPU_Time) return Boolean; + function "<" (Left, Right : CPU_Time) return Boolean with + Global => null; + function "<=" (Left, Right : CPU_Time) return Boolean with + Global => null; + function ">" (Left, Right : CPU_Time) return Boolean with + Global => null; + function ">=" (Left, Right : CPU_Time) return Boolean with + Global => null; procedure Split (T : CPU_Time; SC : out Ada.Real_Time.Seconds_Count; - TS : out Ada.Real_Time.Time_Span); + TS : out Ada.Real_Time.Time_Span) + with + Global => null; function Time_Of (SC : Ada.Real_Time.Seconds_Count; TS : Ada.Real_Time.Time_Span := Ada.Real_Time.Time_Span_Zero) - return CPU_Time; + return CPU_Time + with + Global => null; Interrupt_Clocks_Supported : constant Boolean := False; Separate_Interrupt_Clocks_Supported : constant Boolean := False; diff --git a/gcc/ada/a-extiin.ads b/gcc/ada/a-extiin.ads index 8e8563dcdf1..e35c32df37d 100644 --- a/gcc/ada/a-extiin.ads +++ b/gcc/ada/a-extiin.ads @@ -27,6 +27,8 @@ is Volatile_Function, Global => Ada.Real_Time.Clock_Time; - function Supported (Interrupt : Ada.Interrupts.Interrupt_ID) return Boolean; + function Supported (Interrupt : Ada.Interrupts.Interrupt_ID) return Boolean + with + Global => null; end Ada.Execution_Time.Interrupts; diff --git a/gcc/ada/a-interr.ads b/gcc/ada/a-interr.ads index 09a58687a32..0ce2ed66d95 100644 --- a/gcc/ada/a-interr.ads +++ b/gcc/ada/a-interr.ads @@ -55,27 +55,31 @@ package Ada.Interrupts is function Current_Handler (Interrupt : Interrupt_ID) return Parameterless_Handler with - SPARK_Mode => Off; + SPARK_Mode => Off, + Global => null; procedure Attach_Handler (New_Handler : Parameterless_Handler; Interrupt : Interrupt_ID) with - SPARK_Mode => Off; + SPARK_Mode => Off, + Global => null; procedure Exchange_Handler (Old_Handler : out Parameterless_Handler; New_Handler : Parameterless_Handler; Interrupt : Interrupt_ID) with - SPARK_Mode => Off; + SPARK_Mode => Off, + Global => null; procedure Detach_Handler (Interrupt : Interrupt_ID) with SPARK_Mode, Global => (In_Out => Ada.Task_Identification.Tasking_State); function Reference (Interrupt : Interrupt_ID) return System.Address with - SPARK_Mode => Off; + SPARK_Mode => Off, + Global => null; private pragma Inline (Is_Reserved); diff --git a/gcc/ada/a-reatim.ads b/gcc/ada/a-reatim.ads index ff73167d95d..98d97156a02 100644 --- a/gcc/ada/a-reatim.ads +++ b/gcc/ada/a-reatim.ads @@ -62,42 +62,69 @@ is Volatile_Function, Global => Clock_Time; - function "+" (Left : Time; Right : Time_Span) return Time; - function "+" (Left : Time_Span; Right : Time) return Time; - function "-" (Left : Time; Right : Time_Span) return Time; - function "-" (Left : Time; Right : Time) return Time_Span; - - function "<" (Left, Right : Time) return Boolean; - function "<=" (Left, Right : Time) return Boolean; - function ">" (Left, Right : Time) return Boolean; - function ">=" (Left, Right : Time) return Boolean; - - function "+" (Left, Right : Time_Span) return Time_Span; - function "-" (Left, Right : Time_Span) return Time_Span; - function "-" (Right : Time_Span) return Time_Span; - function "*" (Left : Time_Span; Right : Integer) return Time_Span; - function "*" (Left : Integer; Right : Time_Span) return Time_Span; - function "/" (Left, Right : Time_Span) return Integer; - function "/" (Left : Time_Span; Right : Integer) return Time_Span; - - function "abs" (Right : Time_Span) return Time_Span; - - function "<" (Left, Right : Time_Span) return Boolean; - function "<=" (Left, Right : Time_Span) return Boolean; - function ">" (Left, Right : Time_Span) return Boolean; - function ">=" (Left, Right : Time_Span) return Boolean; - - function To_Duration (TS : Time_Span) return Duration; - function To_Time_Span (D : Duration) return Time_Span; - - function Nanoseconds (NS : Integer) return Time_Span; - function Microseconds (US : Integer) return Time_Span; - function Milliseconds (MS : Integer) return Time_Span; - - function Seconds (S : Integer) return Time_Span; + function "+" (Left : Time; Right : Time_Span) return Time with + Global => null; + function "+" (Left : Time_Span; Right : Time) return Time with + Global => null; + function "-" (Left : Time; Right : Time_Span) return Time with + Global => null; + function "-" (Left : Time; Right : Time) return Time_Span with + Global => null; + + function "<" (Left, Right : Time) return Boolean with + Global => null; + function "<=" (Left, Right : Time) return Boolean with + Global => null; + function ">" (Left, Right : Time) return Boolean with + Global => null; + function ">=" (Left, Right : Time) return Boolean with + Global => null; + + function "+" (Left, Right : Time_Span) return Time_Span with + Global => null; + function "-" (Left, Right : Time_Span) return Time_Span with + Global => null; + function "-" (Right : Time_Span) return Time_Span with + Global => null; + function "*" (Left : Time_Span; Right : Integer) return Time_Span with + Global => null; + function "*" (Left : Integer; Right : Time_Span) return Time_Span with + Global => null; + function "/" (Left, Right : Time_Span) return Integer with + Global => null; + function "/" (Left : Time_Span; Right : Integer) return Time_Span with + Global => null; + + function "abs" (Right : Time_Span) return Time_Span with + Global => null; + + function "<" (Left, Right : Time_Span) return Boolean with + Global => null; + function "<=" (Left, Right : Time_Span) return Boolean with + Global => null; + function ">" (Left, Right : Time_Span) return Boolean with + Global => null; + function ">=" (Left, Right : Time_Span) return Boolean with + Global => null; + + function To_Duration (TS : Time_Span) return Duration with + Global => null; + function To_Time_Span (D : Duration) return Time_Span with + Global => null; + + function Nanoseconds (NS : Integer) return Time_Span with + Global => null; + function Microseconds (US : Integer) return Time_Span with + Global => null; + function Milliseconds (MS : Integer) return Time_Span with + Global => null; + + function Seconds (S : Integer) return Time_Span with + Global => null; pragma Ada_05 (Seconds); - function Minutes (M : Integer) return Time_Span; + function Minutes (M : Integer) return Time_Span with + Global => null; pragma Ada_05 (Minutes); type Seconds_Count is new Long_Long_Integer; @@ -109,8 +136,12 @@ is -- in the case of CodePeer with a target configuration file with a maximum -- integer size of 32, it allows analysis of this unit. - procedure Split (T : Time; SC : out Seconds_Count; TS : out Time_Span); - function Time_Of (SC : Seconds_Count; TS : Time_Span) return Time; + procedure Split (T : Time; SC : out Seconds_Count; TS : out Time_Span) + with + Global => null; + function Time_Of (SC : Seconds_Count; TS : Time_Span) return Time + with + Global => null; private pragma SPARK_Mode (Off); diff --git a/gcc/ada/a-taside.ads b/gcc/ada/a-taside.ads index 3a3df7c0d2d..353475ea146 100644 --- a/gcc/ada/a-taside.ads +++ b/gcc/ada/a-taside.ads @@ -49,10 +49,12 @@ is Null_Task_Id : constant Task_Id; - function "=" (Left, Right : Task_Id) return Boolean; + function "=" (Left, Right : Task_Id) return Boolean with + Global => null; pragma Inline ("="); - function Image (T : Task_Id) return String; + function Image (T : Task_Id) return String with + Global => null; function Current_Task return Task_Id with Volatile_Function, @@ -60,10 +62,12 @@ is pragma Inline (Current_Task); function Environment_Task return Task_Id with - SPARK_Mode => Off; + SPARK_Mode => Off, + Global => null; pragma Inline (Environment_Task); - procedure Abort_Task (T : Task_Id); + procedure Abort_Task (T : Task_Id) with + Global => null; pragma Inline (Abort_Task); -- Note: parameter is mode IN, not IN OUT, per AI-00101 diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index 88cc9c0b8b0..ba541e4bb03 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -27,6 +27,7 @@ with Atree; use Atree; with Back_End; use Back_End; with Checks; with Comperr; +with Cprint; with Csets; use Csets; with Debug; use Debug; with Elists; @@ -148,6 +149,7 @@ procedure Gnat1drv is Generate_C_Code := True; Modify_Tree_For_C := True; Unnest_Subprogram_Mode := True; + Back_Annotate_Rep_Info := True; -- Enable some restrictions systematically to simplify the generated -- code. Note that restriction checks are also disabled in C mode, @@ -1356,6 +1358,13 @@ begin Namet.Unlock; + -- Finally generate C source code if needed. Note that this needs to + -- happen after calling gigi to take advantage of the back annotation. + + if Generate_C_Code then + Cprint.Source_Dump; + end if; + -- Generate the call-graph output of dispatching calls Exp_CG.Generate_CG_Output; diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index a39671494fa..8d7615979fe 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -112,6 +112,10 @@ package body SPARK_Specific is (N : Node_Id; Process : Node_Processing; Inside_Stubs : Boolean); + procedure Traverse_Protected_Body + (N : Node_Id; + Process : Node_Processing; + Inside_Stubs : Boolean); procedure Traverse_Package_Body (N : Node_Id; Process : Node_Processing; @@ -1201,6 +1205,9 @@ package body SPARK_Specific is elsif Nkind (Lu) = N_Package_Body then Traverse_Package_Body (Lu, Process, Inside_Stubs); + elsif Nkind (Lu) = N_Protected_Body then + Traverse_Protected_Body (Lu, Process, Inside_Stubs); + -- All other cases of compilation units (e.g. renamings), are not -- declarations, or else generic declarations which are ignored. @@ -1298,8 +1305,7 @@ package body SPARK_Specific is (Private_Declarations (N), Process, Inside_Stubs); when N_Protected_Body => - Traverse_Declarations_Or_Statements - (Declarations (N), Process, Inside_Stubs); + Traverse_Protected_Body (N, Process, Inside_Stubs); when N_Protected_Body_Stub => if Present (Library_Unit (N)) then @@ -1475,6 +1481,19 @@ package body SPARK_Specific is (Private_Declarations (Spec), Process, Inside_Stubs); end Traverse_Package_Declaration; + ----------------------------- + -- Traverse_Protected_Body -- + ----------------------------- + + procedure Traverse_Protected_Body + (N : Node_Id; + Process : Node_Processing; + Inside_Stubs : Boolean) is + begin + Traverse_Declarations_Or_Statements + (Declarations (N), Process, Inside_Stubs); + end Traverse_Protected_Body; + ------------------------------ -- Traverse_Subprogram_Body -- ------------------------------ diff --git a/gcc/ada/sem_dim.adb b/gcc/ada/sem_dim.adb index f9448343e28..1706f5e96cc 100644 --- a/gcc/ada/sem_dim.adb +++ b/gcc/ada/sem_dim.adb @@ -1817,10 +1817,15 @@ package body Sem_Dim is if Has_Dimension_System (Base_Type (Comp_Typ)) then Expr := Expression (Comp); + -- A box-initialized component needs no checking. + + if No (Expr) and then Box_Present (Comp) then + null; + -- Issue an error if the dimensions of the component type and the -- dimensions of the component mismatch. - if Dimensions_Of (Expr) /= Dimensions_Of (Comp_Typ) then + elsif Dimensions_Of (Expr) /= Dimensions_Of (Comp_Typ) then -- Check if an error has already been encountered so far diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 58775ac47bd..d7b588352c1 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -21580,6 +21580,11 @@ package body Sem_Prag is Spec_Id := Corresponding_Spec_Of (Subp_Decl); Over_Id := Overridden_Operation (Spec_Id); + if not Ekind_In (Spec_Id, E_Function, E_Generic_Function) then + Pragma_Misplaced; + return; + end if; + -- A pragma that applies to a Ghost entity becomes Ghost for the -- purposes of legality checks and removal of ignored Ghost code. -- 2.30.2