+2011-08-29 Yannick Moy <moy@adacore.com>
+
+ * sem_ch3.adb (Array_Type_Declaration): Create declarations for Itypes
+ created in Alfa mode, instead of inserting artificial declarations of
+ non-Itypes in the tree.
+ * sem_util.adb, sem_util.ads (Itype_Has_Declaration): New function to
+ know if an Itype has a corresponding declaration, as defined in
+ itypes.ads.
+
+2011-08-29 Yannick Moy <moy@adacore.com>
+
+ * gnat1drv.adb: Minor rewrite.
+
+2011-08-29 Bob Duff <duff@adacore.com>
+
+ * s-tasuti.adb (Make_Passive): Work around race condition in
+ Make_Independent, which can cause Wait_Count to be zero. So instead of
+ asserting that Wait_Count > 0, and then decrementing it, decrement it
+ only if Wait_Count > 0.
+ * s-taskin.ads (Wait_Count, Alive_Count, Awake_Count): All of these
+ should be nonnegative, so declare them Natural instead of Integer.
+
2011-08-29 Robert Dewar <dewar@adacore.com>
* exp_ch5.adb, sem_ch3.adb, a-cihama.adb, a-cihama.ads, exp_ch7.adb,
-- We would prefer to suppress the expansion of tagged types and
-- dispatching calls, so that one day GNATprove can handle them
- -- directly. Unfortunately, this is causing problems on H513-015, so
- -- keep this expansion for the time being. ???
+ -- directly. Unfortunately, this is causing problems in some cases,
+ -- so keep this expansion for the time being.
Tagged_Type_Expansion := True;
end if;
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
-- --
-- GNARL 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- --
-- Protection: Set by Activator before Self is activated, and only read
-- and modified by Self after that.
- Wait_Count : Integer;
+ Wait_Count : Natural;
-- This count is used by a task that is waiting for other tasks. At all
-- other times, the value should be zero. It is used differently in
-- several different states. Since a task cannot be in more than one of
-- not write this field until the master is complete, the
-- synchronization should be adequate to prevent races.
- Alive_Count : Integer := 0;
+ Alive_Count : Natural := 0;
-- Number of tasks directly dependent on this task (including itself)
-- that are still "alive", i.e. not terminated.
--
-- Protection: Self.L
- Awake_Count : Integer := 0;
+ Awake_Count : Natural := 0;
-- Number of tasks directly dependent on this task (including itself)
-- still "awake", i.e., are not terminated and not waiting on a
-- terminate alternative.
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2009, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
-- --
-- GNARL 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- --
(Debug.Trace
(Self_ID, "Make_Passive: Phase 1, parent waiting", 'M'));
- -- If parent is in Master_Completion_Sleep, it
- -- cannot be on a terminate alternative, hence
- -- it cannot have Awake_Count of zero.
+ -- If parent is in Master_Completion_Sleep, it cannot be on a
+ -- terminate alternative, hence it cannot have Wait_Count of
+ -- zero. ???Except that the race condition in Make_Independent can
+ -- cause Wait_Count to be zero, so we need to check for that.
- pragma Assert (P.Common.Wait_Count > 0);
- P.Common.Wait_Count := P.Common.Wait_Count - 1;
+ if P.Common.Wait_Count > 0 then
+ P.Common.Wait_Count := P.Common.Wait_Count - 1;
+ end if;
if P.Common.Wait_Count = 0 then
Wakeup (P, Master_Completion_Sleep);
Make_Index (Index, P, Related_Id, Nb_Index);
- -- In formal verification mode, create an explicit subtype for every
- -- index if not already a subtype_mark, and replace the existing type
- -- of index by this new type. Having a declaration for all type
+ -- In formal verification mode, create an explicit declaration for
+ -- Itypes created for index types. Having a declaration for all type
-- entities facilitates the task of the formal verification back-end.
+ -- Notice that this declaration is not attached to the tree.
if ALFA_Mode
- and then not Nkind_In (Index, N_Identifier, N_Expanded_Name)
+ and then Is_Itype (Etype (Index))
then
declare
Loc : constant Source_Ptr := Sloc (Def);
- New_E : Entity_Id;
- Decl : Entity_Id;
Sub_Ind : Node_Id;
+ Decl : Entity_Id;
begin
- New_E :=
- New_External_Entity
- (E_Void, Current_Scope, Sloc (P), Related_Id, 'D',
- Nb_Index, 'T');
-
if Nkind (Index) = N_Subtype_Indication then
Sub_Ind := Relocate_Node (Index);
else
Decl :=
Make_Subtype_Declaration (Loc,
- Defining_Identifier => New_E,
+ Defining_Identifier => Etype (Index),
Subtype_Indication => Sub_Ind);
- Insert_Action (Parent (Def), Decl);
- Set_Etype (Index, New_E);
+ Analyze (Decl);
end;
end if;
if Present (Component_Typ) then
- -- In formal verification mode, create an explicit subtype for the
- -- component type if not already a subtype_mark. Having a declaration
- -- for all type entities facilitates the task of the formal
- -- verification back-end.
+ Element_Type := Process_Subtype (Component_Typ, P, Related_Id, 'C');
+
+ -- In formal verification mode, create an explicit declaration for
+ -- the Itype created for a component type. Having a declaration for
+ -- all type entities facilitates the task of the formal verification
+ -- back-end. Notice that this declaration is not attached to the
+ -- tree.
if ALFA_Mode
- and then Nkind (Component_Typ) = N_Subtype_Indication
+ and then Is_Itype (Element_Type)
then
declare
Loc : constant Source_Ptr := Sloc (Def);
Decl : Entity_Id;
begin
- Element_Type :=
- New_External_Entity
- (E_Void, Current_Scope, Sloc (P), Related_Id, 'C', 0, 'T');
-
Decl :=
Make_Subtype_Declaration (Loc,
Defining_Identifier => Element_Type,
Subtype_Indication => Relocate_Node (Component_Typ));
- Insert_Action (Parent (Def), Decl);
+ Analyze (Decl);
end;
-
- else
- Element_Type :=
- Process_Subtype (Component_Typ, P, Related_Id, 'C');
end if;
Set_Etype (Component_Typ, Element_Type);
(Implicit_Base, Finalize_Storage_Only
(Element_Type));
+ -- In ALFA mode, generate a declaration for Itype T, so that the
+ -- formal verification back-end can use it.
+
+ if ALFA_Mode
+ and then Is_Itype (T)
+ then
+ declare
+ Loc : constant Source_Ptr := Sloc (Def);
+ Decl : Node_Id;
+
+ begin
+ Decl := Make_Full_Type_Declaration (Loc,
+ Defining_Identifier => T,
+ Type_Definition =>
+ Make_Constrained_Array_Definition (Loc,
+ Discrete_Subtype_Definitions =>
+ New_Copy_List (Discrete_Subtype_Definitions (Def)),
+ Component_Definition =>
+ Relocate_Node (Component_Definition (Def))));
+
+ Analyze (Decl);
+ end;
+ end if;
+
-- Unconstrained array case
else
end if;
end Is_Volatile_Object;
+ ---------------------------
+ -- Itype_Has_Declaration --
+ ---------------------------
+
+ function Itype_Has_Declaration (Id : Entity_Id) return Boolean is
+ begin
+ pragma Assert (Is_Itype (Id));
+ return Present (Parent (Id))
+ and then Nkind_In (Parent (Id),
+ N_Full_Type_Declaration,
+ N_Subtype_Declaration)
+ and then Defining_Entity (Parent (Id)) = Id;
+ end Itype_Has_Declaration;
+
-------------------------
-- Kill_Current_Values --
-------------------------
-- for something actually declared as volatile, not for an object that gets
-- treated as volatile (see Einfo.Treat_As_Volatile).
+ function Itype_Has_Declaration (Id : Entity_Id) return Boolean;
+ -- Applies to Itypes. True if the Itype is attached to a declaration for
+ -- the type through its Parent field, which may or not be present in the
+ -- tree.
+
procedure Kill_Current_Values (Last_Assignment_Only : Boolean := False);
-- This procedure is called to clear all constant indications from all
-- entities in the current scope and in any parent scopes if the current
projects / thirdparty / gcc.git / commitdiff
