From ddce04b8b9370d128bc890e27de8888c84250c5b Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 20 Nov 2014 15:47:19 +0100 Subject: [PATCH] [multiple changes] 2014-11-20 Robert Dewar * sem_prag.adb (Analyze_Pragma, case Elaborate): Forbid pragma Elaborate in SPARK mode. 2014-11-20 Bob Duff * s-taskin.adb, s-tassta.adb (Initialize_ATCB): If Domain is null, then initialize T.Common.Domain to that of the activating task (not the parent task!), as required by RM-D.16.1. T.Common.Domain should never be null; so Assert. Remove similar code from Create_Task in s-tassta.adb. * s-mudido-affinity.adb: Remove checks for Domain = null, because it can't be null. * s-taskin.ads, s-taspri-dummy.ads, s-taspri-mingw.ads, s-taspri-posix.ads, s-taspri-posix-noaltstack.ads, s-taspri-solaris.ads, s-taspri-vxworks.ads: Mark limited types as explicitly limited for clarity. 2014-11-20 Ed Schonberg * exp_aggr.adb (Init_Hidden_Discriminants): Code clean up. From-SVN: r217863 --- gcc/ada/ChangeLog | 23 ++++++++++ gcc/ada/exp_aggr.adb | 21 ++++++--- gcc/ada/s-mudido-affinity.adb | 13 +++--- gcc/ada/s-taskin.adb | 33 +++++++------- gcc/ada/s-taskin.ads | 13 +++--- gcc/ada/s-taspri-dummy.ads | 2 +- gcc/ada/s-taspri-mingw.ads | 2 +- gcc/ada/s-taspri-posix-noaltstack.ads | 2 +- gcc/ada/s-taspri-posix.ads | 2 +- gcc/ada/s-taspri-solaris.ads | 2 +- gcc/ada/s-taspri-vxworks.ads | 2 +- gcc/ada/s-tassta.adb | 12 ----- gcc/ada/sem_prag.adb | 64 +++++++++++++++++++-------- 13 files changed, 120 insertions(+), 71 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 0ccf7eae1fd..457d7f95288 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,26 @@ +2014-11-20 Robert Dewar + + * sem_prag.adb (Analyze_Pragma, case Elaborate): Forbid pragma + Elaborate in SPARK mode. + +2014-11-20 Bob Duff + + * s-taskin.adb, s-tassta.adb (Initialize_ATCB): If Domain + is null, then initialize T.Common.Domain to that of the + activating task (not the parent task!), as required by RM-D.16.1. + T.Common.Domain should never be null; so Assert. Remove similar + code from Create_Task in s-tassta.adb. + * s-mudido-affinity.adb: Remove checks for Domain = null, + because it can't be null. + * s-taskin.ads, s-taspri-dummy.ads, s-taspri-mingw.ads, + s-taspri-posix.ads, s-taspri-posix-noaltstack.ads, + s-taspri-solaris.ads, s-taspri-vxworks.ads: Mark limited types as + explicitly limited for clarity. + +2014-11-20 Ed Schonberg + + * exp_aggr.adb (Init_Hidden_Discriminants): Code clean up. + 2014-11-20 Robert Dewar * errout.adb (Error_Msg): Don't suppress continuation msgs for diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb index ac67a5724e2..d9a43ff8d28 100644 --- a/gcc/ada/exp_aggr.adb +++ b/gcc/ada/exp_aggr.adb @@ -2108,21 +2108,27 @@ package body Exp_Aggr is ------------------------------- procedure Init_Hidden_Discriminants (Typ : Entity_Id; List : List_Id) is - Btype : Entity_Id; - Parent_Type : Entity_Id; - Disc : Entity_Id; - Discr_Val : Elmt_Id; + Btype : Entity_Id; + Parent_Type : Entity_Id; + Disc : Entity_Id; + Discr_Val : Elmt_Id; + In_Aggr_Type : Boolean; begin -- The constraints on the hidden discriminants, if present, are kept -- in the Stored_Constraint list of the type itself, or in that of - -- the base type. + -- the base type. If not in the constraints of the aggregate itself, + -- we examine ancestors to find discriminants that are not renamed + -- by other discriminants but constrained explicitly. + + In_Aggr_Type := True; Btype := Base_Type (Typ); while Is_Derived_Type (Btype) and then (Present (Stored_Constraint (Btype)) or else - Present (Stored_Constraint (Typ))) + (In_Aggr_Type + and then Present (Stored_Constraint (Typ)))) loop Parent_Type := Etype (Btype); @@ -2149,7 +2155,7 @@ package body Exp_Aggr is Discr_Val := First_Elmt (Stored_Constraint (Typ)); end if; - while Present (Discr_Val) loop + while Present (Discr_Val) and Present (Disc) loop -- Only those discriminants of the parent that are not -- renamed by discriminants of the derived type need to @@ -2176,6 +2182,7 @@ package body Exp_Aggr is Next_Elmt (Discr_Val); end loop; + In_Aggr_Type := False; Btype := Base_Type (Parent_Type); end loop; end Init_Hidden_Discriminants; diff --git a/gcc/ada/s-mudido-affinity.adb b/gcc/ada/s-mudido-affinity.adb index 475d245539c..05e27719082 100644 --- a/gcc/ada/s-mudido-affinity.adb +++ b/gcc/ada/s-mudido-affinity.adb @@ -85,8 +85,7 @@ package body System.Multiprocessors.Dispatching_Domains is -- System_Dispatching_Domain, or if CPU is not one of the processors of -- Domain (and is not Not_A_Specific_CPU). - if Target.Common.Domain /= null and then - Dispatching_Domain (Target.Common.Domain) /= System_Dispatching_Domain + if Dispatching_Domain (Target.Common.Domain) /= System_Dispatching_Domain then raise Dispatching_Domain_Error with "task already in user-defined dispatching domain"; @@ -201,9 +200,7 @@ package body System.Multiprocessors.Dispatching_Domains is T := ST.All_Tasks_List; while T /= null loop - if T.Common.Domain = null or else - T.Common.Domain = ST.System_Domain - then + if T.Common.Domain = ST.System_Domain then Set_Task_Affinity (T); end if; @@ -275,7 +272,11 @@ package body System.Multiprocessors.Dispatching_Domains is Ada.Task_Identification.Current_Task) return Dispatching_Domain is begin - return Dispatching_Domain (Convert_Ids (T).Common.Domain); + return Result : constant Dispatching_Domain := + Dispatching_Domain (Convert_Ids (T).Common.Domain) + do + pragma Assert (Result /= null); + end return; end Get_Dispatching_Domain; ------------------- diff --git a/gcc/ada/s-taskin.adb b/gcc/ada/s-taskin.adb index 1643e5c56e6..7ed47697a7b 100644 --- a/gcc/ada/s-taskin.adb +++ b/gcc/ada/s-taskin.adb @@ -110,13 +110,16 @@ package body System.Tasking is return; end if; - -- Wouldn't the following be better done using an assignment of an - -- aggregate so that we could be sure no components were forgotten??? - T.Common.Parent := Parent; T.Common.Base_Priority := Base_Priority; T.Common.Base_CPU := Base_CPU; - T.Common.Domain := Domain; + + -- The Domain defaults to that of the activator + + T.Common.Domain := + (if Domain = null then Self_ID.Common.Domain else Domain); + pragma Assert (T.Common.Domain /= null); + T.Common.Current_Priority := 0; T.Common.Protected_Action_Nesting := 0; T.Common.Call := null; @@ -218,18 +221,18 @@ package body System.Tasking is T := STPO.New_ATCB (0); Initialize_ATCB - (Self_ID => null, + (Self_ID => null, Task_Entry_Point => null, - Task_Arg => Null_Address, - Parent => Null_Task, - Elaborated => null, - Base_Priority => Base_Priority, - Base_CPU => Base_CPU, - Domain => System_Domain, - Task_Info => Task_Info.Unspecified_Task_Info, - Stack_Size => 0, - T => T, - Success => Success); + Task_Arg => Null_Address, + Parent => Null_Task, + Elaborated => null, + Base_Priority => Base_Priority, + Base_CPU => Base_CPU, + Domain => System_Domain, + Task_Info => Task_Info.Unspecified_Task_Info, + Stack_Size => 0, + T => T, + Success => Success); pragma Assert (Success); STPO.Initialize (T); diff --git a/gcc/ada/s-taskin.ads b/gcc/ada/s-taskin.ads index a89fe6b2a41..b12af37ea7e 100644 --- a/gcc/ada/s-taskin.ads +++ b/gcc/ada/s-taskin.ads @@ -504,7 +504,7 @@ package System.Tasking is -- Section used by all GNARL implementations (regular and restricted) - type Common_ATCB is record + type Common_ATCB is limited record State : Task_States; pragma Atomic (State); -- Encodes some basic information about the state of a task, @@ -721,7 +721,7 @@ package System.Tasking is -- present in the Restricted_Ada_Task_Control_Block structure. type Restricted_Ada_Task_Control_Block (Entry_Num : Task_Entry_Index) is - record + limited record Common : Common_ATCB; -- The common part between various tasking implementations @@ -954,7 +954,7 @@ package System.Tasking is -- than 64-bits explicitly to allow codepeer to analyze this unit when -- a target configuration file forces the maximum integer size to 32. - type Ada_Task_Control_Block (Entry_Num : Task_Entry_Index) is record + type Ada_Task_Control_Block (Entry_Num : Task_Entry_Index) is limited record Common : Common_ATCB; -- The common part between various tasking implementations @@ -1179,10 +1179,9 @@ package System.Tasking is T : Task_Id; Success : out Boolean); -- Initialize fields of the TCB for task T, and link into global TCB - -- structures. Call this only with abort deferred and holding - -- RTS_Lock. Self_ID is the calling task (normally the activator of - -- T). Success is set to indicate whether the TCB was successfully - -- initialized. Need more documentation ??? + -- structures. Call this only with abort deferred and holding RTS_Lock. + -- Self_ID is the calling task (normally the activator of T). Success is + -- set to indicate whether the TCB was successfully initialized. private diff --git a/gcc/ada/s-taspri-dummy.ads b/gcc/ada/s-taspri-dummy.ads index 271f5d1c301..a6adf196dcd 100644 --- a/gcc/ada/s-taspri-dummy.ads +++ b/gcc/ada/s-taspri-dummy.ads @@ -46,7 +46,7 @@ package System.Task_Primitives is type Task_Body_Access is access procedure; - type Private_Data is record + type Private_Data is limited record Thread : aliased Integer; CV : aliased Integer; L : aliased RTS_Lock; diff --git a/gcc/ada/s-taspri-mingw.ads b/gcc/ada/s-taspri-mingw.ads index a4306254144..64b115f3393 100644 --- a/gcc/ada/s-taspri-mingw.ads +++ b/gcc/ada/s-taspri-mingw.ads @@ -97,7 +97,7 @@ private -- Condition variable used to queue threads until condition is signaled end record; - type Private_Data is record + type Private_Data is limited record Thread : aliased Win32.HANDLE; pragma Atomic (Thread); -- Thread field may be updated by two different threads of control. diff --git a/gcc/ada/s-taspri-posix-noaltstack.ads b/gcc/ada/s-taspri-posix-noaltstack.ads index a7708b2b300..aadcfbf5bfe 100644 --- a/gcc/ada/s-taspri-posix-noaltstack.ads +++ b/gcc/ada/s-taspri-posix-noaltstack.ads @@ -97,7 +97,7 @@ private -- Condition variable used to queue threads until condition is signaled end record; - type Private_Data is record + type Private_Data is limited record Thread : aliased System.OS_Interface.pthread_t; pragma Atomic (Thread); -- Thread field may be updated by two different threads of control. diff --git a/gcc/ada/s-taspri-posix.ads b/gcc/ada/s-taspri-posix.ads index 7eb0781569d..a492a1782e8 100644 --- a/gcc/ada/s-taspri-posix.ads +++ b/gcc/ada/s-taspri-posix.ads @@ -96,7 +96,7 @@ private -- Condition variable used to queue threads until condition is signaled end record; - type Private_Data is record + type Private_Data is limited record Thread : aliased System.OS_Interface.pthread_t; pragma Atomic (Thread); -- Thread field may be updated by two different threads of control. diff --git a/gcc/ada/s-taspri-solaris.ads b/gcc/ada/s-taspri-solaris.ads index 6b2df7ff31f..1d5c7dba838 100644 --- a/gcc/ada/s-taspri-solaris.ads +++ b/gcc/ada/s-taspri-solaris.ads @@ -124,7 +124,7 @@ private -- Note that task support on gdb relies on the fact that the first two -- fields of Private_Data are Thread and LWP. - type Private_Data is record + type Private_Data is limited record Thread : aliased System.OS_Interface.thread_t; pragma Atomic (Thread); -- Thread field may be updated by two different threads of control. diff --git a/gcc/ada/s-taspri-vxworks.ads b/gcc/ada/s-taspri-vxworks.ads index 4e3eba5fc45..833bf9822f2 100644 --- a/gcc/ada/s-taspri-vxworks.ads +++ b/gcc/ada/s-taspri-vxworks.ads @@ -98,7 +98,7 @@ private -- Condition variable used to queue threads until condition is signaled end record; - type Private_Data is record + type Private_Data is limited record Thread : aliased System.OS_Interface.t_id := 0; pragma Atomic (Thread); -- Thread field may be updated by two different threads of control. diff --git a/gcc/ada/s-tassta.adb b/gcc/ada/s-tassta.adb index da76c6559e5..9f9383a2e1d 100644 --- a/gcc/ada/s-tassta.adb +++ b/gcc/ada/s-tassta.adb @@ -662,18 +662,6 @@ package body System.Tasking.Stages is T.Common.Task_Image_Len := Len; end if; - -- The task inherits the dispatching domain of the parent only if no - -- specific domain has been defined in the spec of the task (using the - -- dispatching domain pragma or aspect). - - if T.Common.Domain /= null then - null; - elsif T.Common.Activator /= null then - T.Common.Domain := T.Common.Activator.Common.Domain; - else - T.Common.Domain := System.Tasking.System_Domain; - end if; - Unlock (Self_ID); Unlock_RTS; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 94bbf9397e6..18048bc5a35 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -13125,7 +13125,9 @@ package body Sem_Prag is Citem : Node_Id; begin - SPARK_Msg_N ("pragma Elaborate not allowed", N); + if SPARK_Mode = On then + Error_Msg_N ("pragma Elaborate not allowed in SPARK mode", N); + end if; -- Pragma must be in context items list of a compilation unit @@ -13207,7 +13209,15 @@ package body Sem_Prag is -- Give a warning if operating in static mode with one of the -- gnatwl/-gnatwE (elaboration warnings enabled) switches set. - if Elab_Warnings and not Dynamic_Elaboration_Checks then + if Elab_Warnings + and not Dynamic_Elaboration_Checks + + -- pragma Elaborate not allowed in SPARK mode anyway. We + -- already complained about it, no point in generating any + -- further complaint. + + and SPARK_Mode /= On + then Error_Msg_N ("?l?use of pragma Elaborate may not be safe", N); Error_Msg_N @@ -13343,8 +13353,13 @@ package body Sem_Prag is GNAT_Pragma; Check_Arg_Count (1); Check_Arg_Is_One_Of (Arg1, Name_Static, Name_Dynamic); + + -- Set flag accordingly (ignore attempt at dynamic elaboration + -- checks in SPARK mode). + Dynamic_Elaboration_Checks := - (Chars (Get_Pragma_Arg (Arg1)) = Name_Dynamic); + (Chars (Get_Pragma_Arg (Arg1)) = Name_Dynamic) + and then SPARK_Mode /= On; --------------- -- Eliminate -- @@ -19541,6 +19556,8 @@ package body Sem_Prag is -- pragma SPARK_Mode [(On | Off)]; when Pragma_SPARK_Mode => Do_SPARK_Mode : declare + Mode_Id : SPARK_Mode_Type; + procedure Check_Pragma_Conformance (Context_Pragma : Node_Id; Entity_Pragma : Node_Id; @@ -19565,6 +19582,11 @@ package body Sem_Prag is procedure Check_Library_Level_Entity (E : Entity_Id); -- Verify that pragma is applied to library-level entity E + procedure Set_SPARK_Flags; + -- Sets SPARK_Mode from Mode_Id and SPARK_Mode_Pragma from N, + -- and ensures that Dynamic_Elaboration_Checks are off if the + -- call sets SPARK_Mode On. + ------------------------------ -- Check_Pragma_Conformance -- ------------------------------ @@ -19642,12 +19664,25 @@ package body Sem_Prag is end if; end Check_Library_Level_Entity; + --------------------- + -- Set_SPARK_Flags -- + --------------------- + + procedure Set_SPARK_Flags is + begin + SPARK_Mode := Mode_Id; + SPARK_Mode_Pragma := N; + + if SPARK_Mode = On then + Dynamic_Elaboration_Checks := False; + end if; + end Set_SPARK_Flags; + -- Local variables Body_Id : Entity_Id; Context : Node_Id; Mode : Name_Id; - Mode_Id : SPARK_Mode_Type; Spec_Id : Entity_Id; Stmt : Node_Id; @@ -19691,8 +19726,7 @@ package body Sem_Prag is raise Pragma_Exit; end if; - SPARK_Mode_Pragma := N; - SPARK_Mode := Mode_Id; + Set_SPARK_Flags; -- The pragma acts as a configuration pragma in a compilation unit @@ -19703,8 +19737,7 @@ package body Sem_Prag is and then List_Containing (N) = Context_Items (Context) then Check_Valid_Configuration_Pragma; - SPARK_Mode_Pragma := N; - SPARK_Mode := Mode_Id; + Set_SPARK_Flags; -- Otherwise the placement of the pragma within the tree dictates -- its associated construct. Inspect the declarative list where @@ -19789,8 +19822,7 @@ package body Sem_Prag is (Context_Pragma => SPARK_Pragma (Spec_Id), Entity_Pragma => Empty, Entity => Empty); - SPARK_Mode_Pragma := N; - SPARK_Mode := Mode_Id; + Set_SPARK_Flags; Set_SPARK_Pragma (Spec_Id, N); Set_SPARK_Pragma_Inherited (Spec_Id, False); @@ -19808,8 +19840,7 @@ package body Sem_Prag is (Context_Pragma => Empty, Entity_Pragma => SPARK_Pragma (Spec_Id), Entity => Spec_Id); - SPARK_Mode_Pragma := N; - SPARK_Mode := Mode_Id; + Set_SPARK_Flags; Set_SPARK_Aux_Pragma (Spec_Id, N); Set_SPARK_Aux_Pragma_Inherited (Spec_Id, False); @@ -19828,8 +19859,7 @@ package body Sem_Prag is (Context_Pragma => SPARK_Pragma (Body_Id), Entity_Pragma => SPARK_Aux_Pragma (Spec_Id), Entity => Spec_Id); - SPARK_Mode_Pragma := N; - SPARK_Mode := Mode_Id; + Set_SPARK_Flags; Set_SPARK_Pragma (Body_Id, N); Set_SPARK_Pragma_Inherited (Body_Id, False); @@ -19853,8 +19883,7 @@ package body Sem_Prag is (Context_Pragma => Empty, Entity_Pragma => SPARK_Pragma (Body_Id), Entity => Body_Id); - SPARK_Mode_Pragma := N; - SPARK_Mode := Mode_Id; + Set_SPARK_Flags; Set_SPARK_Aux_Pragma (Body_Id, N); Set_SPARK_Aux_Pragma_Inherited (Body_Id, False); @@ -19916,8 +19945,7 @@ package body Sem_Prag is Entity => Empty); end if; - SPARK_Mode_Pragma := N; - SPARK_Mode := Mode_Id; + Set_SPARK_Flags; Set_SPARK_Pragma (Body_Id, N); Set_SPARK_Pragma_Inherited (Body_Id, False);