From 9fd9d2beb0212955c62cdfcf7401eaabd45b2462 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 29 Aug 2011 16:15:28 +0200 Subject: [PATCH] [multiple changes] 2011-08-29 Yannick Moy * 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 * gnat1drv.adb: Minor rewrite. 2011-08-29 Bob Duff * 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. From-SVN: r178240 --- gcc/ada/ChangeLog | 22 ++++++++++++++ gcc/ada/gnat1drv.adb | 4 +-- gcc/ada/s-taskin.ads | 8 +++--- gcc/ada/s-tasuti.adb | 14 +++++---- gcc/ada/sem_ch3.adb | 68 ++++++++++++++++++++++++++------------------ gcc/ada/sem_util.adb | 14 +++++++++ gcc/ada/sem_util.ads | 5 ++++ 7 files changed, 95 insertions(+), 40 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index f98d49f27ab4..6ebe68778a2d 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,25 @@ +2011-08-29 Yannick Moy + + * 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 + + * gnat1drv.adb: Minor rewrite. + +2011-08-29 Bob Duff + + * 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 * exp_ch5.adb, sem_ch3.adb, a-cihama.adb, a-cihama.ads, exp_ch7.adb, diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index cf85e4ee909b..ffb3e24cdef6 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -478,8 +478,8 @@ procedure Gnat1drv is -- 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; diff --git a/gcc/ada/s-taskin.ads b/gcc/ada/s-taskin.ads index 074c86b6a4ad..40772c94d095 100644 --- a/gcc/ada/s-taskin.ads +++ b/gcc/ada/s-taskin.ads @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -566,7 +566,7 @@ package System.Tasking is -- 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 @@ -942,13 +942,13 @@ package System.Tasking is -- 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. diff --git a/gcc/ada/s-tasuti.adb b/gcc/ada/s-tasuti.adb index 8e818be9ce9c..a6b362ee2aa7 100644 --- a/gcc/ada/s-tasuti.adb +++ b/gcc/ada/s-tasuti.adb @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -504,12 +504,14 @@ package body System.Tasking.Utilities is (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); diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 91abe52248ad..0c2c043a5456 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -4741,26 +4741,20 @@ package body Sem_Ch3 is 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 @@ -4775,11 +4769,10 @@ package body Sem_Ch3 is 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; @@ -4799,34 +4792,29 @@ package body Sem_Ch3 is 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); @@ -4915,6 +4903,30 @@ package body Sem_Ch3 is (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 diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 7589b659f8ca..b4dac3cfc5e9 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -8507,6 +8507,20 @@ package body Sem_Util is 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 -- ------------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 7acc4345757f..b3844d896085 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -969,6 +969,11 @@ package Sem_Util is -- 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 -- 2.47.2