+2014-11-20 Robert Dewar <dewar@adacore.com>
+
+ * sem_prag.adb (Analyze_Pragma, case Elaborate): Forbid pragma
+ Elaborate in SPARK mode.
+
+2014-11-20 Bob Duff <duff@adacore.com>
+
+ * 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 <schonberg@adacore.com>
+
+ * exp_aggr.adb (Init_Hidden_Discriminants): Code clean up.
+
2014-11-20 Robert Dewar <dewar@adacore.com>
* errout.adb (Error_Msg): Don't suppress continuation msgs for
-------------------------------
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);
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
Next_Elmt (Discr_Val);
end loop;
+ In_Aggr_Type := False;
Btype := Base_Type (Parent_Type);
end loop;
end Init_Hidden_Discriminants;
-- 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";
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;
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;
-------------------
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;
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);
-- 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,
-- 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
-- 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
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
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;
-- 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.
-- 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.
-- 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.
-- 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.
-- 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.
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;
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
-- 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
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 --
-- 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;
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 --
------------------------------
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;
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
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
(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);
(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);
(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);
(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);
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);