diff options
| author | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-01-21 17:16:43 +0100 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-01-21 17:16:43 +0100 |
| commit | 6c3c671e4d2659884d01f384723910b0966d2c6d (patch) | |
| tree | 8ed9f54f33935952c4e9823fa9733894c38423dc /gcc | |
| parent | 084c220328b5738ed943d513cc8f646cfa167dea (diff) | |
| download | gcc-6c3c671e4d2659884d01f384723910b0966d2c6d.zip gcc-6c3c671e4d2659884d01f384723910b0966d2c6d.tar.gz gcc-6c3c671e4d2659884d01f384723910b0966d2c6d.tar.bz2 | |
[multiple changes]
2014-01-21 Hristian Kirtchev <kirtchev@adacore.com>
* aspects.adb Add entries for Async_Readers, Async_Writers,
Effective_Reads and Effective_Writes in table Canonical_Aspect.
* aspects.ads Add entries for Async_Readers, Async_Writers,
Effective_Reads and Effective_Writes in tables Aspect_Id,
Aspect_Names, Aspect_Delay and Implementation_Defined_Aspect.
* atree.adb (Ekind_In): New version with 8 parameters.
(Node34): New routine.
(Set_Node34): New routine.
* atree.ads (Ekind_In): New version with 8 parameters.
(Node34): New routine.
(Set_Node34): New routine.
* einfo.adb Contract is now Node34.
(Contract): Update the assertion and node usage.
(Get_Pragma): Include pragmas Async_Readers, Async_Writers,
Effective_Reads and Effective_Writes.
(Set_Contract): Update the assertion and node usage.
(Write_Field24_Name): Remove the output for a contract.
(Write_Field34_Name): Add output for a contract.
* einfo.ads Contract is now Node34. Update the comment on
attribute usage and related node structures.
(Get_Pragma): Update the comment on usage.
* par-prag.adb (Prag): Pragmas Async_Readers, Async_Writers,
Effective_Reads and Effective_Writes do not require special
processing by the parser.
* sem_ch3.adb (Analyze_Variable_Contract): New routine.
(Analyze_Declarations): Analyze the contract of a variable at
the end of the declarative region.
(Analyze_Object_Declaration): Create a contract for a variable.
* sem_ch6.adb (Analyze_Subprogram_Contract): Update the retrieval
of classification pragmas.
(Process_Formals): Detect an illegal
use of a volatile object as a formal in a function.
* sem_ch12.adb (Instantiate_Object): Detect an illegal use of
a volatile object as an actual in generic instantiation.
* sem_prag.adb Add entries for Async_Readers, Async_Writers,
Effective_Reads and Effective_Writes in table Sig_Flags.
(Analyze_External_State_In_Decl_Part): New routine.
(Analyze_Global_Item): Detect an illegal use of a volatile object
as a global item of a function.
(Analyze_Pragma): Reimplement
pragma Abstract_State. Add support for pragmas Async_Readers,
Async_Writers, Effective_Reads and Effective_Writes.
(Check_External_Properties): New routine.
* sem_prag.ads (Analyze_External_State_In_Decl_Part): New routine.
(Check_External_Properties): New routine.
* sem_res.adb (Resolve_Actuals): Detect an illegal use of a
volatile object as an actual in a call.
(Resolve_Entity_Name):
Add local variables Par, Prev and Usage_OK. Detect illegal
contexts of volatile objects.
* sem_util.adb (Add_Contract_Item): Add support for
pragmas associated with the contract of a variable.
(Async_Readers_Enabled): New routine.
(Async_Writers_Enabled): New routine.
(Effective_Reads_Enabled): New routine.
(Effective_Writes_Enabled): New routine.
(Has_Enabled_Property):
New routine.
(Is_Unchecked_Conversion_Instance): New routine.
(Is_Volatile_Object): Add support for entities that may denote
a volatile object.
* sem_util.ads (Add_Contract_Item): Update the
comment on usage.
(Async_Readers_Enabled): New routine.
(Async_Writers_Enabled): New routine.
(Effective_Reads_Enabled): New routine.
(Effective_Writes_Enabled): New routine.
(Is_Unchecked_Conversion_Instance): New routine.
* sinfo.ads Update the comment on the structure of N_Contract.
* snames.ads-tmpl Add predefined names for Async_Readers,
Async_Writers, Effective_Reads and Effective_Writes. Add
pragma ids for Async_Readers, Async_Writers, Effective_Reads
and Effective_Writes.
2014-01-21 Robert Dewar <dewar@adacore.com>
* exp_ch4.adb (Eval_Op_Expon): Use CRT_Safe_Compile_Time_Known_Value
* sem_eval.adb (Compile_Time_Known_Value): Remove special
handling of CRT mode (CRT_Safe_Compile_Time_Known_Value): New
function (Eval_Op_Expon): Add CRT_Safe in call to Test_Foldable
(Test_Foldable): Add CRT_Safe parameter
* sem_eval.ads (Compile_Time_Known_Value): Remove special
handling of CRT mode.
(CRT_Safe_Compile_Time_Known_Value): New function.
From-SVN: r206886
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 87 | ||||
| -rw-r--r-- | gcc/ada/aspects.adb | 4 | ||||
| -rw-r--r-- | gcc/ada/aspects.ads | 16 | ||||
| -rw-r--r-- | gcc/ada/atree.adb | 49 | ||||
| -rw-r--r-- | gcc/ada/atree.ads | 28 | ||||
| -rw-r--r-- | gcc/ada/einfo.adb | 36 | ||||
| -rw-r--r-- | gcc/ada/einfo.ads | 29 | ||||
| -rw-r--r-- | gcc/ada/exp_ch4.adb | 10 | ||||
| -rw-r--r-- | gcc/ada/par-prag.adb | 4 | ||||
| -rw-r--r-- | gcc/ada/sem_ch12.adb | 10 | ||||
| -rw-r--r-- | gcc/ada/sem_ch3.adb | 87 | ||||
| -rw-r--r-- | gcc/ada/sem_ch6.adb | 14 | ||||
| -rw-r--r-- | gcc/ada/sem_eval.adb | 94 | ||||
| -rw-r--r-- | gcc/ada/sem_eval.ads | 48 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 549 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.ads | 18 | ||||
| -rw-r--r-- | gcc/ada/sem_res.adb | 99 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 205 | ||||
| -rw-r--r-- | gcc/ada/sem_util.ads | 28 | ||||
| -rw-r--r-- | gcc/ada/sinfo.ads | 4 | ||||
| -rw-r--r-- | gcc/ada/snames.ads-tmpl | 8 |
21 files changed, 1207 insertions, 220 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index dacb968..2fbcd79 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,90 @@ +2014-01-21 Hristian Kirtchev <kirtchev@adacore.com> + + * aspects.adb Add entries for Async_Readers, Async_Writers, + Effective_Reads and Effective_Writes in table Canonical_Aspect. + * aspects.ads Add entries for Async_Readers, Async_Writers, + Effective_Reads and Effective_Writes in tables Aspect_Id, + Aspect_Names, Aspect_Delay and Implementation_Defined_Aspect. + * atree.adb (Ekind_In): New version with 8 parameters. + (Node34): New routine. + (Set_Node34): New routine. + * atree.ads (Ekind_In): New version with 8 parameters. + (Node34): New routine. + (Set_Node34): New routine. + * einfo.adb Contract is now Node34. + (Contract): Update the assertion and node usage. + (Get_Pragma): Include pragmas Async_Readers, Async_Writers, + Effective_Reads and Effective_Writes. + (Set_Contract): Update the assertion and node usage. + (Write_Field24_Name): Remove the output for a contract. + (Write_Field34_Name): Add output for a contract. + * einfo.ads Contract is now Node34. Update the comment on + attribute usage and related node structures. + (Get_Pragma): Update the comment on usage. + * par-prag.adb (Prag): Pragmas Async_Readers, Async_Writers, + Effective_Reads and Effective_Writes do not require special + processing by the parser. + * sem_ch3.adb (Analyze_Variable_Contract): New routine. + (Analyze_Declarations): Analyze the contract of a variable at + the end of the declarative region. + (Analyze_Object_Declaration): Create a contract for a variable. + * sem_ch6.adb (Analyze_Subprogram_Contract): Update the retrieval + of classification pragmas. + (Process_Formals): Detect an illegal + use of a volatile object as a formal in a function. + * sem_ch12.adb (Instantiate_Object): Detect an illegal use of + a volatile object as an actual in generic instantiation. + * sem_prag.adb Add entries for Async_Readers, Async_Writers, + Effective_Reads and Effective_Writes in table Sig_Flags. + (Analyze_External_State_In_Decl_Part): New routine. + (Analyze_Global_Item): Detect an illegal use of a volatile object + as a global item of a function. + (Analyze_Pragma): Reimplement + pragma Abstract_State. Add support for pragmas Async_Readers, + Async_Writers, Effective_Reads and Effective_Writes. + (Check_External_Properties): New routine. + * sem_prag.ads (Analyze_External_State_In_Decl_Part): New routine. + (Check_External_Properties): New routine. + * sem_res.adb (Resolve_Actuals): Detect an illegal use of a + volatile object as an actual in a call. + (Resolve_Entity_Name): + Add local variables Par, Prev and Usage_OK. Detect illegal + contexts of volatile objects. + * sem_util.adb (Add_Contract_Item): Add support for + pragmas associated with the contract of a variable. + (Async_Readers_Enabled): New routine. + (Async_Writers_Enabled): New routine. + (Effective_Reads_Enabled): New routine. + (Effective_Writes_Enabled): New routine. + (Has_Enabled_Property): + New routine. + (Is_Unchecked_Conversion_Instance): New routine. + (Is_Volatile_Object): Add support for entities that may denote + a volatile object. + * sem_util.ads (Add_Contract_Item): Update the + comment on usage. + (Async_Readers_Enabled): New routine. + (Async_Writers_Enabled): New routine. + (Effective_Reads_Enabled): New routine. + (Effective_Writes_Enabled): New routine. + (Is_Unchecked_Conversion_Instance): New routine. + * sinfo.ads Update the comment on the structure of N_Contract. + * snames.ads-tmpl Add predefined names for Async_Readers, + Async_Writers, Effective_Reads and Effective_Writes. Add + pragma ids for Async_Readers, Async_Writers, Effective_Reads + and Effective_Writes. + +2014-01-21 Robert Dewar <dewar@adacore.com> + + * exp_ch4.adb (Eval_Op_Expon): Use CRT_Safe_Compile_Time_Known_Value + * sem_eval.adb (Compile_Time_Known_Value): Remove special + handling of CRT mode (CRT_Safe_Compile_Time_Known_Value): New + function (Eval_Op_Expon): Add CRT_Safe in call to Test_Foldable + (Test_Foldable): Add CRT_Safe parameter + * sem_eval.ads (Compile_Time_Known_Value): Remove special + handling of CRT mode. + (CRT_Safe_Compile_Time_Known_Value): New function. + 2014-01-21 Robert Dewar <dewar@adacore.com> * sem_prag.adb (Analyze_Pragma, case SPARK_Mode): Fix problem diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb index 4e17352..64a239a 100644 --- a/gcc/ada/aspects.adb +++ b/gcc/ada/aspects.adb @@ -472,6 +472,8 @@ package body Aspects is Aspect_Address => Aspect_Address, Aspect_Alignment => Aspect_Alignment, Aspect_All_Calls_Remote => Aspect_All_Calls_Remote, + Aspect_Async_Readers => Aspect_Async_Readers, + Aspect_Async_Writers => Aspect_Async_Writers, Aspect_Asynchronous => Aspect_Asynchronous, Aspect_Atomic => Aspect_Atomic, Aspect_Atomic_Components => Aspect_Atomic_Components, @@ -492,6 +494,8 @@ package body Aspects is Aspect_Discard_Names => Aspect_Discard_Names, Aspect_Dispatching_Domain => Aspect_Dispatching_Domain, Aspect_Dynamic_Predicate => Aspect_Predicate, + Aspect_Effective_Reads => Aspect_Effective_Reads, + Aspect_Effective_Writes => Aspect_Effective_Writes, Aspect_Elaborate_Body => Aspect_Elaborate_Body, Aspect_Export => Aspect_Export, Aspect_External_Name => Aspect_External_Name, diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads index 2f31863..c5d7632 100644 --- a/gcc/ada/aspects.ads +++ b/gcc/ada/aspects.ads @@ -161,10 +161,14 @@ package Aspects is Aspect_Ada_2005, -- GNAT Aspect_Ada_2012, -- GNAT + Aspect_Async_Readers, -- GNAT + Aspect_Async_Writers, -- GNAT Aspect_Asynchronous, Aspect_Atomic, Aspect_Atomic_Components, Aspect_Discard_Names, + Aspect_Effective_Reads, -- GNAT + Aspect_Effective_Writes, -- GNAT Aspect_Export, Aspect_Favor_Top_Level, -- GNAT Aspect_Independent, @@ -215,11 +219,15 @@ package Aspects is (Aspect_Abstract_State => True, Aspect_Ada_2005 => True, Aspect_Ada_2012 => True, + Aspect_Async_Readers => True, + Aspect_Async_Writers => True, Aspect_Compiler_Unit => True, Aspect_Contract_Cases => True, Aspect_Depends => True, Aspect_Dimension => True, Aspect_Dimension_System => True, + Aspect_Effective_Reads => True, + Aspect_Effective_Writes => True, Aspect_Favor_Top_Level => True, Aspect_Global => True, Aspect_Inline_Always => True, @@ -368,6 +376,8 @@ package Aspects is Aspect_Address => Name_Address, Aspect_Alignment => Name_Alignment, Aspect_All_Calls_Remote => Name_All_Calls_Remote, + Aspect_Async_Readers => Name_Async_Readers, + Aspect_Async_Writers => Name_Async_Writers, Aspect_Asynchronous => Name_Asynchronous, Aspect_Atomic => Name_Atomic, Aspect_Atomic_Components => Name_Atomic_Components, @@ -388,6 +398,8 @@ package Aspects is Aspect_Discard_Names => Name_Discard_Names, Aspect_Dispatching_Domain => Name_Dispatching_Domain, Aspect_Dynamic_Predicate => Name_Dynamic_Predicate, + Aspect_Effective_Reads => Name_Effective_Reads, + Aspect_Effective_Writes => Name_Effective_Writes, Aspect_Elaborate_Body => Name_Elaborate_Body, Aspect_External_Name => Name_External_Name, Aspect_External_Tag => Name_External_Tag, @@ -575,6 +587,8 @@ package Aspects is (No_Aspect => Always_Delay, Aspect_Address => Always_Delay, Aspect_All_Calls_Remote => Always_Delay, + Aspect_Async_Readers => Always_Delay, + Aspect_Async_Writers => Always_Delay, Aspect_Asynchronous => Always_Delay, Aspect_Attach_Handler => Always_Delay, Aspect_Compiler_Unit => Always_Delay, @@ -588,6 +602,8 @@ package Aspects is Aspect_Discard_Names => Always_Delay, Aspect_Dispatching_Domain => Always_Delay, Aspect_Dynamic_Predicate => Always_Delay, + Aspect_Effective_Reads => Always_Delay, + Aspect_Effective_Writes => Always_Delay, Aspect_Elaborate_Body => Always_Delay, Aspect_External_Name => Always_Delay, Aspect_External_Tag => Always_Delay, diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb index 44cad86..86820b4 100644 --- a/gcc/ada/atree.adb +++ b/gcc/ada/atree.adb @@ -1009,6 +1009,28 @@ package body Atree is end Ekind_In; function Ekind_In + (T : Entity_Kind; + V1 : Entity_Kind; + V2 : Entity_Kind; + V3 : Entity_Kind; + V4 : Entity_Kind; + V5 : Entity_Kind; + V6 : Entity_Kind; + V7 : Entity_Kind; + V8 : Entity_Kind) return Boolean + is + begin + return T = V1 or else + T = V2 or else + T = V3 or else + T = V4 or else + T = V5 or else + T = V6 or else + T = V7 or else + T = V8; + end Ekind_In; + + function Ekind_In (E : Entity_Id; V1 : Entity_Kind; V2 : Entity_Kind) return Boolean @@ -1077,6 +1099,21 @@ package body Atree is return Ekind_In (Ekind (E), V1, V2, V3, V4, V5, V6, V7); end Ekind_In; + function Ekind_In + (E : Entity_Id; + V1 : Entity_Kind; + V2 : Entity_Kind; + V3 : Entity_Kind; + V4 : Entity_Kind; + V5 : Entity_Kind; + V6 : Entity_Kind; + V7 : Entity_Kind; + V8 : Entity_Kind) return Boolean + is + begin + return Ekind_In (Ekind (E), V1, V2, V3, V4, V5, V6, V7, V8); + end Ekind_In; + ------------------------ -- Set_Reporting_Proc -- ------------------------ @@ -2601,6 +2638,12 @@ package body Atree is return Node_Id (Nodes.Table (N + 5).Field9); end Node33; + function Node34 (N : Node_Id) return Node_Id is + begin + pragma Assert (Nkind (N) in N_Entity); + return Node_Id (Nodes.Table (N + 5).Field10); + end Node34; + function List1 (N : Node_Id) return List_Id is begin pragma Assert (N <= Nodes.Last); @@ -5348,6 +5391,12 @@ package body Atree is Nodes.Table (N + 5).Field9 := Union_Id (Val); end Set_Node33; + procedure Set_Node34 (N : Node_Id; Val : Node_Id) is + begin + pragma Assert (Nkind (N) in N_Entity); + Nodes.Table (N + 5).Field10 := Union_Id (Val); + end Set_Node34; + procedure Set_List1 (N : Node_Id; Val : List_Id) is begin pragma Assert (N <= Nodes.Last); diff --git a/gcc/ada/atree.ads b/gcc/ada/atree.ads index 94fd5b2..d5b3bca 100644 --- a/gcc/ada/atree.ads +++ b/gcc/ada/atree.ads @@ -755,6 +755,17 @@ package Atree is V7 : Entity_Kind) return Boolean; function Ekind_In + (E : Entity_Id; + V1 : Entity_Kind; + V2 : Entity_Kind; + V3 : Entity_Kind; + V4 : Entity_Kind; + V5 : Entity_Kind; + V6 : Entity_Kind; + V7 : Entity_Kind; + V8 : Entity_Kind) return Boolean; + + function Ekind_In (T : Entity_Kind; V1 : Entity_Kind; V2 : Entity_Kind) return Boolean; @@ -799,6 +810,17 @@ package Atree is V6 : Entity_Kind; V7 : Entity_Kind) return Boolean; + function Ekind_In + (T : Entity_Kind; + V1 : Entity_Kind; + V2 : Entity_Kind; + V3 : Entity_Kind; + V4 : Entity_Kind; + V5 : Entity_Kind; + V6 : Entity_Kind; + V7 : Entity_Kind; + V8 : Entity_Kind) return Boolean; + pragma Inline (Ekind_In); -- Inline all above functions @@ -1212,6 +1234,9 @@ package Atree is function Node33 (N : Node_Id) return Node_Id; pragma Inline (Node33); + function Node34 (N : Node_Id) return Node_Id; + pragma Inline (Node34); + function List1 (N : Node_Id) return List_Id; pragma Inline (List1); @@ -2515,6 +2540,9 @@ package Atree is procedure Set_Node33 (N : Node_Id; Val : Node_Id); pragma Inline (Set_Node33); + procedure Set_Node34 (N : Node_Id; Val : Node_Id); + pragma Inline (Set_Node34); + procedure Set_List1 (N : Node_Id; Val : List_Id); pragma Inline (Set_List1); diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 45088b2..65d54bb 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -214,7 +214,6 @@ package body Einfo is -- Stored_Constraint Elist23 -- Related_Expression Node24 - -- Contract Node24 -- Interface_Alias Node25 -- Interfaces Elist25 @@ -252,7 +251,7 @@ package body Einfo is -- SPARK_Aux_Pragma Node33 - -- (unused) Node34 + -- Contract Node34 -- (unused) Node35 @@ -1079,10 +1078,11 @@ package body Einfo is E_Generic_Package, E_Package, E_Package_Body, - E_Subprogram_Body) + E_Subprogram_Body, + E_Variable) or else Is_Generic_Subprogram (Id) or else Is_Subprogram (Id)); - return Node24 (Id); + return Node34 (Id); end Contract; function Entry_Parameters_Type (Id : E) return E is @@ -3727,10 +3727,11 @@ package body Einfo is E_Package, E_Package_Body, E_Subprogram_Body, + E_Variable, E_Void) or else Is_Generic_Subprogram (Id) or else Is_Subprogram (Id)); - Set_Node24 (Id, V); + Set_Node34 (Id, V); end Set_Contract; procedure Set_Entry_Parameters_Type (Id : E; V : E) is @@ -6395,7 +6396,11 @@ package body Einfo is function Get_Pragma (E : Entity_Id; Id : Pragma_Id) return Node_Id is Is_CDG : constant Boolean := Id = Pragma_Abstract_State or else + Id = Pragma_Async_Readers or else + Id = Pragma_Async_Writers or else Id = Pragma_Depends or else + Id = Pragma_Effective_Reads or else + Id = Pragma_Effective_Writes or else Id = Pragma_Global or else Id = Pragma_Initial_Condition or else Id = Pragma_Initializes or else @@ -9216,16 +9221,6 @@ package body Einfo is Type_Kind => Write_Str ("Related_Expression"); - when E_Entry | - E_Entry_Family | - E_Generic_Package | - E_Package | - E_Package_Body | - E_Subprogram_Body | - Generic_Subprogram_Kind | - Subprogram_Kind => - Write_Str ("Contract"); - when others => Write_Str ("Field24???"); end case; @@ -9468,6 +9463,17 @@ package body Einfo is procedure Write_Field34_Name (Id : Entity_Id) is begin case Ekind (Id) is + when E_Entry | + E_Entry_Family | + E_Generic_Package | + E_Package | + E_Package_Body | + E_Subprogram_Body | + E_Variable | + Generic_Subprogram_Kind | + Subprogram_Kind => + Write_Str ("Contract"); + when others => Write_Str ("Field34??"); end case; diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index fc710da..7599574 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -1027,11 +1027,11 @@ package Einfo is -- accept statement for a member of the family, and in the prefix of -- 'COUNT when it applies to a family member. --- Contract (Node24) +-- Contract (Node34) -- Defined in entry, entry family, package, package body, subprogram and --- subprogram body entities as well as their respective generic forms. --- Points to the contract of the entity, holding various assertion items --- and data classifiers. +-- subprogram body entities as well as their respective generic forms. A +-- contract is also applicable to a variable. Points to the contract of +-- the entity, holding various assertion items and data classifiers. -- Entry_Parameters_Type (Node15) -- Defined in entries. Points to the access-to-record type that is @@ -5369,9 +5369,9 @@ package Einfo is -- Accept_Address (Elist21) -- Scope_Depth_Value (Uint22) -- Protection_Object (Node23) (protected kind) - -- Contract (Node24) -- PPC_Wrapper (Node25) -- Extra_Formals (Node28) + -- Contract (Node34) -- Default_Expressions_Processed (Flag108) -- Entry_Accepted (Flag152) -- Is_AST_Entry (Flag132) (for entry only) @@ -5472,7 +5472,6 @@ package Einfo is -- Generic_Renamings (Elist23) (for an instance) -- Inner_Instances (Elist23) (generic case only) -- Protection_Object (Node23) (for concurrent kind) - -- Contract (Node24) -- Interface_Alias (Node25) -- Overridden_Operation (Node26) -- Wrapped_Entity (Node27) (non-generic case only) @@ -5481,6 +5480,7 @@ package Einfo is -- Corresponding_Equality (Node30) (implicit /= only) -- Thunk_Entity (Node31) (thunk case only) -- SPARK_Pragma (Node32) + -- Contract (Node34) -- Body_Needed_For_SAL (Flag40) -- Elaboration_Entity_Required (Flag174) -- Default_Expressions_Processed (Flag108) @@ -5631,9 +5631,9 @@ package Einfo is -- Alias (Node18) -- Extra_Accessibility_Of_Result (Node19) -- Last_Entity (Node20) - -- Contract (Node24) -- Overridden_Operation (Node26) -- Subprograms_For_Type (Node29) + -- Contract (Node34) -- Has_Invariants (Flag232) -- Has_Postconditions (Flag240) -- Is_Machine_Code_Subprogram (Flag137) @@ -5676,13 +5676,13 @@ package Einfo is -- Generic_Renamings (Elist23) (for an instance) -- Inner_Instances (Elist23) (generic case only) -- Limited_View (Node23) (non-generic/instance) - -- Contract (Node24) -- Abstract_States (Elist25) -- Package_Instantiation (Node26) -- Current_Use_Clause (Node27) -- Finalizer (Node28) (non-generic case only) -- SPARK_Aux_Pragma (Node33) -- SPARK_Pragma (Node32) + -- Contract (Node34) -- Delay_Subprogram_Descriptors (Flag50) -- Body_Needed_For_SAL (Flag40) -- Discard_Names (Flag88) @@ -5715,10 +5715,10 @@ package Einfo is -- Spec_Entity (Node19) -- Last_Entity (Node20) -- Scope_Depth_Value (Uint22) - -- Contract (Node24) -- Finalizer (Node28) (non-generic case only) -- SPARK_Aux_Pragma (Node33) -- SPARK_Pragma (Node32) + -- Contract (Node34) -- Delay_Subprogram_Descriptors (Flag50) -- Has_Anonymous_Master (Flag253) -- SPARK_Aux_Pragma_Inherited (Flag266) @@ -5760,7 +5760,6 @@ package Einfo is -- Generic_Renamings (Elist23) (for an instance) -- Inner_Instances (Elist23) (generic case only) -- Protection_Object (Node23) (for concurrent kind) - -- Contract (Node24) -- Interface_Alias (Node25) -- Overridden_Operation (Node26) (never for init proc) -- Wrapped_Entity (Node27) (non-generic case only) @@ -5768,6 +5767,7 @@ package Einfo is -- Static_Initialization (Node30) (init_proc only) -- Thunk_Entity (Node31) (thunk case only) -- SPARK_Pragma (Node32) + -- Contract (Node34) -- Body_Needed_For_SAL (Flag40) -- Delay_Cleanups (Flag114) -- Discard_Names (Flag88) @@ -5938,10 +5938,10 @@ package Einfo is -- Corresponding_Protected_Entry (Node18) -- Last_Entity (Node20) -- Scope_Depth_Value (Uint22) - -- Contract (Node24) -- Extra_Formals (Node28) -- SPARK_Pragma (Node32) -- SPARK_Pragma_Inherited (Flag265) + -- Contract (Node34) -- Scope_Depth (synth) -- E_Subprogram_Type @@ -6001,6 +6001,7 @@ package Einfo is -- Last_Assignment (Node26) -- Related_Type (Node27) -- Initialization_Statements (Node28) + -- Contract (Node34) -- Has_Alignment_Clause (Flag46) -- Has_Atomic_Components (Flag86) -- Has_Biased_Representation (Flag139) @@ -7494,8 +7495,13 @@ package Einfo is -- with the given pragma Id. If found, the value returned is the N_Pragma -- node, otherwise Empty is returned. The following contract pragmas that -- appear in N_Contract nodes are also handled by this routine: + -- Abstract_State + -- Async_Readers + -- Async_Writers -- Contract_Cases -- Depends + -- Effective_Reads + -- Effective_Writes -- Global -- Initial_Condition -- Initializes @@ -7503,6 +7509,7 @@ package Einfo is -- Postcondition -- Refined_Depends -- Refined_Global + -- Refined_State function Get_Record_Representation_Clause (E : Entity_Id) return Node_Id; -- Searches the Rep_Item chain for a given entity E, for a record diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb index aa39586..03dc4fd 100644 --- a/gcc/ada/exp_ch4.adb +++ b/gcc/ada/exp_ch4.adb @@ -7352,7 +7352,12 @@ package body Exp_Ch4 is -- Test for case of known right argument where we can replace the -- exponentiation by an equivalent expression using multiplication. - if Compile_Time_Known_Value (Exp) then + -- Note: use CRT_Safe version of Compile_Time_Known_Value because in + -- configurable run-time mode, we may not have the exponentiation + -- routine available, and we don't want the legality of the program + -- to depend on how clever the compiler is in knowing values. + + if CRT_Safe_Compile_Time_Known_Value (Exp) then Expv := Expr_Value (Exp); -- We only fold small non-negative exponents. You might think we @@ -7454,7 +7459,8 @@ package body Exp_Ch4 is -- result if the shift causes an overflow before the modular reduction. if Nkind (Base) = N_Integer_Literal - and then Intval (Base) = 2 + and then CRT_Safe_Compile_Time_Known_Value (Base) + and then Expr_Value (Base) = Uint_2 and then Is_Integer_Type (Root_Type (Exptyp)) and then Esize (Root_Type (Exptyp)) <= Esize (Standard_Integer) and then Is_Unsigned_Type (Exptyp) diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index 8e86743..0d70800 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -1109,6 +1109,8 @@ begin when Pragma_Abort_Defer | Pragma_Abstract_State | + Pragma_Async_Readers | + Pragma_Async_Writers | Pragma_Assertion_Policy | Pragma_Assume | Pragma_Assume_No_Invalid_Values | @@ -1153,6 +1155,8 @@ begin Pragma_Disable_Atomic_Synchronization | Pragma_Discard_Names | Pragma_Dispatching_Domain | + Pragma_Effective_Reads | + Pragma_Effective_Writes | Pragma_Eliminate | Pragma_Elaborate | Pragma_Elaborate_All | diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index d90d58c..1f030d9 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -9840,6 +9840,16 @@ package body Sem_Ch12 is ("actual must exclude null to match generic formal#", Actual); end if; + -- The following check is only relevant in formal verification mode as + -- it is not a standard Ada legality rule. A volatile object cannot be + -- used as an actual in a generic instantiation. + + if GNATprove_Mode and then Is_Volatile_Object (Actual) then + Error_Msg_N + ("volatile object cannot act as actual in generic instantiation", + Actual); + end if; + return List; end Instantiate_Object; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index c1b9435..f40d1cf 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -91,6 +91,15 @@ package body Sem_Ch3 is -- abstract interface types implemented by a record type or a derived -- record type. + procedure Analyze_Variable_Contract (Var_Id : Entity_Id); + -- Analyze all delayed aspects chained on the contract of variable Var_Id + -- as if they appeared at the end of the declarative region. The aspects in + -- consideration are: + -- Async_Readers + -- Async_Writers + -- Effective_Reads + -- Effective_Writes + procedure Build_Derived_Type (N : Node_Id; Parent_Type : Entity_Id; @@ -2353,8 +2362,9 @@ package body Sem_Ch3 is end if; end if; - -- Analyze the contracts of a subprogram declaration or a body now due - -- to delayed visibility requirements of aspects. + -- Analyze the contracts of subprogram declarations, subprogram bodies + -- and variables now due to the delayed visibility requirements of their + -- aspects. Decl := First (L); while Present (Decl) loop @@ -2363,6 +2373,11 @@ package body Sem_Ch3 is elsif Nkind (Decl) = N_Subprogram_Declaration then Analyze_Subprogram_Contract (Defining_Entity (Decl)); + + elsif Nkind (Decl) = N_Object_Declaration + and then Ekind (Defining_Entity (Decl)) = E_Variable + then + Analyze_Variable_Contract (Defining_Entity (Decl)); end if; Next (Decl); @@ -3698,6 +3713,8 @@ package body Sem_Ch3 is if Present (E) then Set_Has_Initial_Value (Id, True); end if; + + Set_Contract (Id, Make_Contract (Sloc (Id))); end if; -- Initialize alignment and size and capture alignment setting @@ -4769,6 +4786,72 @@ package body Sem_Ch3 is end if; end Analyze_Subtype_Indication; + ------------------------------- + -- Analyze_Variable_Contract -- + ------------------------------- + + procedure Analyze_Variable_Contract (Var_Id : Entity_Id) is + Items : constant Node_Id := Contract (Var_Id); + AR_Val : Boolean := False; + AW_Val : Boolean := False; + ER_Val : Boolean := False; + EW_Val : Boolean := False; + Nam : Name_Id; + Prag : Node_Id; + Seen : Boolean := False; + + begin + -- The following check is only relevant in formal verification mode as + -- it is not standard Ada legality rule. The declaration of a volatile + -- variable must appear at the library level. + + if GNATprove_Mode + and then Is_Volatile_Object (Var_Id) + and then not Is_Library_Level_Entity (Var_Id) + then + Error_Msg_N + ("volatile variable & must be declared at library level", Var_Id); + end if; + + -- Examine the contract + + if Present (Items) then + + -- Analyze classification pragmas + + Prag := Classifications (Items); + while Present (Prag) loop + Nam := Pragma_Name (Prag); + + if Nam = Name_Async_Readers then + Analyze_External_State_In_Decl_Part (Prag, AR_Val); + Seen := True; + + elsif Nam = Name_Async_Writers then + Analyze_External_State_In_Decl_Part (Prag, AW_Val); + Seen := True; + + elsif Nam = Name_Effective_Reads then + Analyze_External_State_In_Decl_Part (Prag, ER_Val); + Seen := True; + + else pragma Assert (Nam = Name_Effective_Writes); + Analyze_External_State_In_Decl_Part (Prag, EW_Val); + Seen := True; + end if; + + Prag := Next_Pragma (Prag); + end loop; + end if; + + -- Once all external properties have been processed, verify their mutual + -- interaction. + + if Seen then + Check_External_Properties (Var_Id, AR_Val, AW_Val, ER_Val, EW_Val); + end if; + end Analyze_Variable_Contract; + -------------------------- -- Analyze_Variant_Part -- -------------------------- diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 078b771..91efb6f 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -3503,7 +3503,7 @@ package body Sem_Ch6 is -- Analyze classification pragmas - Prag := Classifications (Contract (Subp)); + Prag := Classifications (Items); while Present (Prag) loop Nam := Pragma_Name (Prag); @@ -11117,6 +11117,18 @@ package body Sem_Ch6 is Null_Exclusion_Static_Checks (Param_Spec); end if; + -- The following check is only relevant in formal verification mode + -- as it is not a standard Ada legality rule. A function cannot have + -- a volatile formal parameter. + + if GNATprove_Mode + and then Is_Volatile_Object (Formal) + and then Ekind_In (Scope (Formal), E_Function, E_Generic_Function) + then + Error_Msg_N + ("function cannot have a volatile formal parameter", Formal); + end if; + <<Continue>> Next (Param_Spec); end loop; diff --git a/gcc/ada/sem_eval.adb b/gcc/ada/sem_eval.adb index d69c341..8f7eff4 100644 --- a/gcc/ada/sem_eval.adb +++ b/gcc/ada/sem_eval.adb @@ -227,13 +227,17 @@ package body Sem_Eval is -- Is_Static_Expression flag from the operands. procedure Test_Expression_Is_Foldable - (N : Node_Id; - Op1 : Node_Id; - Op2 : Node_Id; - Stat : out Boolean; - Fold : out Boolean); + (N : Node_Id; + Op1 : Node_Id; + Op2 : Node_Id; + Stat : out Boolean; + Fold : out Boolean; + CRT_Safe : Boolean := False); -- Same processing, except applies to an expression N with two operands - -- Op1 and Op2. The result is static only if both operands are static. + -- Op1 and Op2. The result is static only if both operands are static. If + -- CRT_Safe is set True, then CRT_Safe_Compile_Time_Known_Value is used + -- for the tests that the two operands are known at compile time. See + -- spec of this routine for further details. function Test_In_Range (N : Node_Id; @@ -1287,10 +1291,7 @@ package body Sem_Eval is -- Compile_Time_Known_Value -- ------------------------------ - function Compile_Time_Known_Value - (Op : Node_Id; - Ignore_CRT : Boolean := False) return Boolean - is + function Compile_Time_Known_Value (Op : Node_Id) return Boolean is K : constant Node_Kind := Nkind (Op); CV_Ent : CV_Entry renames CV_Cache (Nat (Op) mod CV_Cache_Size); @@ -1309,31 +1310,6 @@ package body Sem_Eval is return False; end if; - -- If this is not a static expression or a null literal, and we are in - -- configurable run-time mode, then we consider it not known at compile - -- time. This avoids anomalies where whether something is allowed with a - -- given configurable run-time library depends on how good the compiler - -- is at optimizing and knowing that things are constant when they are - -- nonstatic. This check is suppressed if Ignore_CRT is True - - if (Configurable_Run_Time_Mode and not Ignore_CRT) - and then K /= N_Null - and then not Is_Static_Expression (Op) - then - -- We make an exception for expressions that evaluate to True/False, - -- to suppress spurious checks in ZFP mode. So far we have not seen - -- any negative consequences of this exception. - - if Is_Entity_Name (Op) - and then Ekind (Entity (Op)) = E_Enumeration_Literal - and then Etype (Entity (Op)) = Standard_Boolean - then - null; - else - return False; - end if; - end if; - -- If we have an entity name, then see if it is the name of a constant -- and if so, test the corresponding constant value, or the name of -- an enumeration literal, which is always a constant. @@ -1487,6 +1463,21 @@ package body Sem_Eval is end if; end Compile_Time_Known_Value_Or_Aggr; + --------------------------------------- + -- CRT_Safe_Compile_Time_Known_Value -- + --------------------------------------- + + function CRT_Safe_Compile_Time_Known_Value (Op : Node_Id) return Boolean is + begin + if (Configurable_Run_Time_Mode or No_Run_Time_Mode) + and then not Is_OK_Static_Expression (Op) + then + return False; + else + return Compile_Time_Known_Value (Op); + end if; + end CRT_Safe_Compile_Time_Known_Value; + ----------------- -- Eval_Actual -- ----------------- @@ -1542,6 +1533,8 @@ package body Sem_Eval is return; end if; + -- Otherwise attempt to fold + if Is_Universal_Numeric_Type (Etype (Left)) and then Is_Universal_Numeric_Type (Etype (Right)) @@ -2537,12 +2530,19 @@ package body Sem_Eval is begin -- If not foldable we are done - Test_Expression_Is_Foldable (N, Left, Right, Stat, Fold); + Test_Expression_Is_Foldable + (N, Left, Right, Stat, Fold, CRT_Safe => True); + + -- Return if not foldable if not Fold then return; end if; + if Configurable_Run_Time_Mode and not Stat then + return; + end if; + -- Fold exponentiation operation declare @@ -5214,11 +5214,12 @@ package body Sem_Eval is -- Two operand case procedure Test_Expression_Is_Foldable - (N : Node_Id; - Op1 : Node_Id; - Op2 : Node_Id; - Stat : out Boolean; - Fold : out Boolean) + (N : Node_Id; + Op1 : Node_Id; + Op2 : Node_Id; + Stat : out Boolean; + Fold : out Boolean; + CRT_Safe : Boolean := False) is Rstat : constant Boolean := Is_Static_Expression (Op1) and then Is_Static_Expression (Op2); @@ -5281,8 +5282,15 @@ package body Sem_Eval is elsif not Rstat then Check_Non_Static_Context (Op1); Check_Non_Static_Context (Op2); - Fold := Compile_Time_Known_Value (Op1) - and then Compile_Time_Known_Value (Op2); + + if CRT_Safe then + Fold := CRT_Safe_Compile_Time_Known_Value (Op1) + and then CRT_Safe_Compile_Time_Known_Value (Op2); + else + Fold := Compile_Time_Known_Value (Op1) + and then Compile_Time_Known_Value (Op2); + end if; + return; -- Else result is static and foldable. Both operands are static, and diff --git a/gcc/ada/sem_eval.ads b/gcc/ada/sem_eval.ads index c3a5e30..aee03d9 100644 --- a/gcc/ada/sem_eval.ads +++ b/gcc/ada/sem_eval.ads @@ -224,23 +224,21 @@ package Sem_Eval is -- Determine whether two types T1, T2, which have the same base type, -- are statically matching subtypes (RM 4.9.1(1-2)). - function Compile_Time_Known_Value - (Op : Node_Id; - Ignore_CRT : Boolean := False) return Boolean; + function Compile_Time_Known_Value (Op : Node_Id) return Boolean; -- Returns true if Op is an expression not raising Constraint_Error whose -- value is known at compile time and for which a call to Expr_Value can -- be used to determine this value. This is always true if Op is a static -- expression, but can also be true for expressions which are technically - -- non-static but which are in fact known at compile time. Some possible - -- examples of such expressions might be the static lower bound of a - -- non-static range or the value of a constant object whose initial - -- value is itself compile time known in the sense of this routine. Note - -- that this routine is defended against unanalyzed expressions. Such - -- expressions will not cause a blowup, they may cause pessimistic (i.e. - -- False) results to be returned. In general we take a pessimistic view. - -- False does not mean the value could not be known at compile time, but - -- True means that absolutely definition it is known at compile time and - -- it is safe to call Expr_Value on the expression Op. + -- non-static but which are in fact known at compile time. Some examples of + -- such expressions are the static lower bound of a non-static range or the + -- value of a constant object whose initial value is itself compile time + -- known in the sense of this routine. Note that this routine is defended + -- against unanalyzed expressions. Such expressions will not cause a + -- blowup, they may cause pessimistic (i.e. False) results to be returned. + -- In general we take a pessimistic view. False does not mean the value + -- could not be known at compile time, but True means that absolutely + -- definition it is known at compile time and it is safe to call + -- Expr_Value on the expression Op. -- -- Note that we don't define precisely the set of expressions that return -- True. Callers should not make any assumptions regarding the value that @@ -250,9 +248,11 @@ package Sem_Eval is -- efficiency optimization purposes. The code generated can often be more -- efficient with compile time known values, e.g. range analysis for the -- purpose of removing checks is more effective if we know precise bounds. - -- - -- The Ignore_CRT parameter has to do with the special case of configurable - -- runtime mode. Consider the following example: + + function CRT_Safe_Compile_Time_Known_Value (Op : Node_Id) return Boolean; + -- In the case of configurable run-times, there may be an issue calling + -- Compile_Time_Known_Value with non-static expressions where the legality + -- of the program is not well-defined. Consider this example: -- -- X := B ** C; -- @@ -266,18 +266,10 @@ package Sem_Eval is -- then what we say is that exponentiation is permitted if the exponent is -- officially static and has a value in the range 0 .. 4. -- - -- However, in the normal case, we want efficient code in the case where - -- a non-static exponent is known at compile time. To take care of this, - -- the normal default behavior is that in configurable run-time mode most - -- expressions are considered known at compile time ONLY in the case where - -- they are officially static. An exception is boolean objects which may - -- be considered known at compile time even in configurable run-time mode. - -- - -- That loses optimization opportunities, and it would be better to look - -- case by case at each use of Compile_Time_Known_Value to see if this - -- configurable run-time mode special processing is needed. The Ignore_CRT - -- parameter can be set to True to ignore this special handling in cases - -- where it is known to be safe to do so. + -- In a case like this, we use CRT_Safe_Compile_Time_Known_Value to avoid + -- this effect. This routine will return False for a non-static expression + -- if we are in configurable run-time mode, even if the expression would + -- normally be considered compile-time known. function Compile_Time_Known_Value_Or_Aggr (Op : Node_Id) return Boolean; -- Similar to Compile_Time_Known_Value, but also returns True if the value diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 0633f72..8148c46 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -1637,6 +1637,53 @@ package body Sem_Prag is end if; end Analyze_Depends_In_Decl_Part; + ----------------------------------------- + -- Analyze_External_State_In_Decl_Part -- + ----------------------------------------- + + procedure Analyze_External_State_In_Decl_Part + (N : Node_Id; + Expr_Val : out Boolean) + is + Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N)); + Obj : constant Node_Id := Get_Pragma_Arg (Arg1); + Expr : constant Node_Id := Get_Pragma_Arg (Next (Arg1)); + + begin + Error_Msg_Name_1 := Pragma_Name (N); + + -- The Async / Effective pragmas must apply to a volatile object other + -- than a formal subprogram parameter. + + if Is_Volatile_Object (Obj) then + if Is_Entity_Name (Obj) + and then Present (Entity (Obj)) + and then Is_Formal (Entity (Obj)) + then + Error_Msg_N + ("external state % cannot apply to a formal parameter", N); + end if; + else + Error_Msg_N ("external state % must apply to a volatile object", N); + end if; + + -- Ensure that the expression (if present) is static Boolean. A missing + -- argument defaults the value to True. + + Expr_Val := True; + + if Present (Expr) then + Analyze_And_Resolve (Expr, Standard_Boolean); + + if Is_Static_Expression (Expr) then + Expr_Val := Is_True (Expr_Value (Expr)); + else + Error_Msg_Name_1 := Pragma_Name (N); + Error_Msg_N ("expression of % must be static", Expr); + end if; + end if; + end Analyze_External_State_In_Decl_Part; + --------------------------------- -- Analyze_Global_In_Decl_Part -- --------------------------------- @@ -1830,6 +1877,16 @@ package body Sem_Prag is Check_Mode_Restriction_In_Enclosing_Context (Item, Item_Id); end if; + -- A volatile object cannot appear as a global item of a function + + if Is_Volatile_Object (Item) + and then Ekind_In (Spec_Id, E_Function, E_Generic_Function) + then + Error_Msg_N + ("volatile object cannot act as global item of a function", + Item); + end if; + -- The same entity might be referenced through various way. Check -- the entity of the item rather than the item itself. @@ -9429,29 +9486,49 @@ package body Sem_Prag is -- ABSTRACT_STATE_LIST ::= -- null -- | STATE_NAME_WITH_OPTIONS - -- | (STATE_NAME_WITH_OPTIONS {, STATE_NAME_WITH_OPTIONS}) + -- | (STATE_NAME_WITH_OPTIONS {, STATE_NAME_WITH_OPTIONS} ) -- STATE_NAME_WITH_OPTIONS ::= - -- state_NAME - -- | (state_NAME with OPTION_LIST) + -- STATE_NAME + -- | (STATE_NAME with OPTION_LIST) -- OPTION_LIST ::= OPTION {, OPTION} - -- OPTION ::= SIMPLE_OPTION | NAME_VALUE_OPTION + -- OPTION ::= + -- SIMPLE_OPTION + -- | NAME_VALUE_OPTION + + -- SIMPLE_OPTION ::= identifier + + -- NAME_VALUE_OPTION ::= + -- Part_Of => ABSTRACT_STATE + -- | External [=> EXTERNAL_PROPERTY_LIST] - -- SIMPLE_OPTION ::= - -- External | Non_Volatile | Input_Only | Output_Only + -- EXTERNAL_PROPERTY_LIST ::= + -- EXTERNAL_PROPERTY + -- | (EXTERNAL_PROPERTY {, EXTERNAL_PROPERTY} ) - -- NAME_VALUE_OPTION ::= Part_Of => abstract_state_NAME + -- EXTERNAL_PROPERTY ::= + -- Async_Readers [=> boolean_EXPRESSION] + -- | Async_Writers [=> boolean_EXPRESSION] + -- | Effective_Reads [=> boolean_EXPRESSION] + -- | Effective_Writes [=> boolean_EXPRESSION] + + -- STATE_NAME ::= defining_identifier + + -- ABSTRACT_STATE ::= name when Pragma_Abstract_State => Abstract_State : declare - Pack_Id : Entity_Id; -- Flags used to verify the consistency of states Non_Null_Seen : Boolean := False; Null_Seen : Boolean := False; + Pack_Id : Entity_Id; + -- The entity of the related package when pragma Abstract_State + -- appears. + procedure Analyze_Abstract_State (State : Node_Id); -- Verify the legality of a single state declaration. Create and -- decorate a state abstraction entity and introduce it into the @@ -9462,6 +9539,37 @@ package body Sem_Prag is ---------------------------- procedure Analyze_Abstract_State (State : Node_Id) is + + -- Flags used to verify the consistency of options + + AR_Seen : Boolean := False; + AW_Seen : Boolean := False; + ER_Seen : Boolean := False; + EW_Seen : Boolean := False; + External_Seen : Boolean := False; + Part_Of_Seen : Boolean := False; + + -- Flags used to store the static value of all external states' + -- expressions. + + AR_Val : Boolean := False; + AW_Val : Boolean := False; + ER_Val : Boolean := False; + EW_Val : Boolean := False; + + procedure Analyze_External_Option (Opt : Node_Id); + -- Verify the legality of option External + + procedure Analyze_External_Property + (Prop : Node_Id; + Expr : Node_Id := Empty); + -- Verify the legailty of a single external property. Prop + -- denotes the external property. Expr is the expression used + -- to set the property. + + procedure Analyze_Part_Of_Option (Opt : Node_Id); + -- Verify the legality of option Part_Of + procedure Check_Duplicate_Option (Opt : Node_Id; Status : in out Boolean); @@ -9469,6 +9577,163 @@ package body Sem_Prag is -- seen while processing a state. This routine verifies that -- Opt is not a duplicate property and sets the flag Status. + ----------------------------- + -- Analyze_External_Option -- + ----------------------------- + + procedure Analyze_External_Option (Opt : Node_Id) is + Errors : constant Nat := Serious_Errors_Detected; + Prop : Node_Id; + Props : Node_Id := Empty; + + begin + Check_Duplicate_Option (Opt, External_Seen); + + if Nkind (Opt) = N_Component_Association then + Props := Expression (Opt); + end if; + + -- External state with properties + + if Present (Props) then + + -- Multiple properties appear as an aggregate + + if Nkind (Props) = N_Aggregate then + + -- Simple property form + + Prop := First (Expressions (Props)); + while Present (Prop) loop + Analyze_External_Property (Prop); + Next (Prop); + end loop; + + -- Property with expression form + + Prop := First (Component_Associations (Props)); + while Present (Prop) loop + Analyze_External_Property + (Prop => First (Choices (Prop)), + Expr => Expression (Prop)); + + Next (Prop); + end loop; + + -- Single property + + else + Analyze_External_Property (Props); + end if; + + -- An external state defined without any properties defaults + -- all properties to True. + + else + AR_Val := True; + AW_Val := True; + ER_Val := True; + EW_Val := True; + end if; + + -- Once all external properties have been processed, verify + -- their mutual interaction. Do not perform the check when + -- at least one of the properties is illegal as this will + -- produce a bogus error. + + if Errors = Serious_Errors_Detected then + Check_External_Properties + (State, AR_Val, AW_Val, ER_Val, EW_Val); + end if; + end Analyze_External_Option; + + ------------------------------- + -- Analyze_External_Property -- + ------------------------------- + + procedure Analyze_External_Property + (Prop : Node_Id; + Expr : Node_Id := Empty) + is + Expr_Val : Boolean; + + begin + -- The external property must be one of the predefined four + -- reader / writer choices. + + if Nkind (Prop) /= N_Identifier + or else not Nam_In (Chars (Prop), Name_Async_Readers, + Name_Async_Writers, + Name_Effective_Reads, + Name_Effective_Writes) + then + Error_Msg_N ("invalid external state property", Prop); + return; + end if; + + -- Ensure that the expression of the external state property + -- is static Boolean (if applicable). + + if Present (Expr) then + Analyze_And_Resolve (Expr, Standard_Boolean); + + if Is_Static_Expression (Expr) then + Expr_Val := Is_True (Expr_Value (Expr)); + else + Error_Msg_N + ("expression of external state property must be " + & "static", Expr); + end if; + + -- The lack of expression defaults the property to True + + else + Expr_Val := True; + end if; + + if Chars (Prop) = Name_Async_Readers then + Check_Duplicate_Option (Prop, AR_Seen); + AR_Val := Expr_Val; + + elsif Chars (Prop) = Name_Async_Writers then + Check_Duplicate_Option (Prop, AW_Seen); + AW_Val := Expr_Val; + + elsif Chars (Prop) = Name_Effective_Reads then + Check_Duplicate_Option (Prop, ER_Seen); + ER_Val := Expr_Val; + + else + Check_Duplicate_Option (Prop, EW_Seen); + EW_Val := Expr_Val; + end if; + end Analyze_External_Property; + + ---------------------------- + -- Analyze_Part_Of_Option -- + ---------------------------- + + procedure Analyze_Part_Of_Option (Opt : Node_Id) is + Par_State : constant Node_Id := Expression (Opt); + + begin + Check_Duplicate_Option (Opt, Part_Of_Seen); + + Analyze (Par_State); + + -- The expression of option Part_Of must denote an abstract + -- state. + + if not Is_Entity_Name (Par_State) + or else No (Entity (Par_State)) + or else Ekind (Entity (Par_State)) /= E_Abstract_State + then + Error_Msg_N + ("option Part_Of must denote an abstract state", + Par_State); + end if; + end Analyze_Part_Of_Option; + ---------------------------- -- Check_Duplicate_Option -- ---------------------------- @@ -9489,20 +9754,11 @@ package body Sem_Prag is Errors : constant Nat := Serious_Errors_Detected; Loc : constant Source_Ptr := Sloc (State); - Assoc : Node_Id; - Id : Entity_Id; Is_Null : Boolean := False; - Name : Name_Id; Opt : Node_Id; - Par_State : Node_Id; - - -- Flags used to verify the consistency of options - - External_Seen : Boolean := False; - Input_Seen : Boolean := False; - Non_Volatile_Seen : Boolean := False; - Output_Seen : Boolean := False; - Part_Of_Seen : Boolean := False; + Opt_Nam : Node_Id; + State_Id : Entity_Id; + State_Nam : Name_Id; -- Start of processing for Analyze_Abstract_State @@ -9517,7 +9773,7 @@ package body Sem_Prag is -- Null states appear as internally generated entities elsif Nkind (State) = N_Null then - Name := New_Internal_Name ('S'); + State_Nam := New_Internal_Name ('S'); Is_Null := True; Null_Seen := True; @@ -9533,7 +9789,7 @@ package body Sem_Prag is -- Simple state declaration elsif Nkind (State) = N_Identifier then - Name := Chars (State); + State_Nam := Chars (State); Non_Null_Seen := True; -- State declaration with various options. This construct @@ -9541,7 +9797,7 @@ package body Sem_Prag is elsif Nkind (State) = N_Extension_Aggregate then if Nkind (Ancestor_Part (State)) = N_Identifier then - Name := Chars (Ancestor_Part (State)); + State_Nam := Chars (Ancestor_Part (State)); Non_Null_Seen := True; else Error_Msg_N @@ -9549,101 +9805,47 @@ package body Sem_Prag is Ancestor_Part (State)); end if; - -- Process options External, Input_Only, Output_Only and - -- Volatile. Ensure that none of them appear more than once. + -- Catch an attempt to introduce a simple option which is + -- currently not allowed. An exception to this is External + -- defined without any properties. Opt := First (Expressions (State)); while Present (Opt) loop - if Nkind (Opt) = N_Identifier then - if Chars (Opt) = Name_External then - Check_Duplicate_Option (Opt, External_Seen); - elsif Chars (Opt) = Name_Input_Only then - Check_Duplicate_Option (Opt, Input_Seen); - elsif Chars (Opt) = Name_Output_Only then - Check_Duplicate_Option (Opt, Output_Seen); - elsif Chars (Opt) = Name_Non_Volatile then - Check_Duplicate_Option (Opt, Non_Volatile_Seen); - - -- Ensure that the abstract state component of option - -- Part_Of has not been omitted. - - elsif Chars (Opt) = Name_Part_Of then - Error_Msg_N - ("option Part_Of requires an abstract state", - Opt); - else - Error_Msg_N ("invalid state option", Opt); - end if; + if Nkind (Opt) = N_Identifier + and then Chars (Opt) = Name_External + then + Analyze_External_Option (Opt); else - Error_Msg_N ("invalid state option", Opt); + Error_Msg_N + ("simple option not allowed in state declaration", + Opt); end if; Next (Opt); end loop; - -- External may appear on its own or with exactly one option - -- Input_Only or Output_Only, but not both. - - if External_Seen - and then Input_Seen - and then Output_Seen - then - Error_Msg_N - ("option External requires exactly one option " - & "Input_Only or Output_Only", State); - end if; + -- Options External and Part_Of appear as component + -- associations. - -- Either Input_Only or Output_Only require External + Opt := First (Component_Associations (State)); + while Present (Opt) loop + Opt_Nam := First (Choices (Opt)); - if (Input_Seen or Output_Seen) - and then not External_Seen - then - Error_Msg_N - ("options Input_Only and Output_Only require option " - & "External", State); - end if; + if Nkind (Opt_Nam) = N_Identifier then + if Chars (Opt_Nam) = Name_External then + Analyze_External_Option (Opt); - -- Option Part_Of appears as a component association + elsif Chars (Opt_Nam) = Name_Part_Of then + Analyze_Part_Of_Option (Opt); - Assoc := First (Component_Associations (State)); - while Present (Assoc) loop - Opt := First (Choices (Assoc)); - while Present (Opt) loop - if Nkind (Opt) = N_Identifier - and then Chars (Opt) = Name_Part_Of - then - Check_Duplicate_Option (Opt, Part_Of_Seen); else Error_Msg_N ("invalid state option", Opt); end if; - - Next (Opt); - end loop; - - -- Part_Of must denote a parent state. Ensure that the - -- tree is not malformed by checking the expression of - -- the component association. - - Par_State := Expression (Assoc); - pragma Assert (Present (Par_State)); - - Analyze (Par_State); - - -- Part_Of specified a legal state, this automatically - -- makes the state a constituent. - - if Is_Entity_Name (Par_State) - and then Present (Entity (Par_State)) - and then Ekind (Entity (Par_State)) = E_Abstract_State - then - null; else - Error_Msg_N - ("option Part_Of must denote an abstract state", - Par_State); + Error_Msg_N ("invalid state option", Opt); end if; - Next (Assoc); + Next (Opt); end loop; -- Any other attempt to declare a state is erroneous @@ -9662,27 +9864,29 @@ package body Sem_Prag is -- The generated state abstraction reuses the same characters -- from the original state declaration. Decorate the entity. - Id := Make_Defining_Identifier (Loc, New_External_Name (Name)); - Set_Comes_From_Source (Id, not Is_Null); - Set_Parent (Id, State); - Set_Ekind (Id, E_Abstract_State); - Set_Etype (Id, Standard_Void_Type); - Set_Refined_State (Id, Empty); - Set_Refinement_Constituents (Id, New_Elmt_List); + State_Id := + Make_Defining_Identifier (Loc, New_External_Name (State_Nam)); + + Set_Comes_From_Source (State_Id, not Is_Null); + Set_Parent (State_Id, State); + Set_Ekind (State_Id, E_Abstract_State); + Set_Etype (State_Id, Standard_Void_Type); + Set_Refined_State (State_Id, Empty); + Set_Refinement_Constituents (State_Id, New_Elmt_List); -- Every non-null state must be nameable and resolvable the -- same way a constant is. if not Is_Null then Push_Scope (Pack_Id); - Enter_Name (Id); + Enter_Name (State_Id); Pop_Scope; end if; -- Verify whether the state introduces an illegal hidden state -- within a package subject to a null abstract state. - Check_No_Hidden_State (Id); + Check_No_Hidden_State (State_Id); -- Associate the state with its related package @@ -9690,7 +9894,7 @@ package body Sem_Prag is Set_Abstract_States (Pack_Id, New_Elmt_List); end if; - Append_Elmt (Id, Abstract_States (Pack_Id)); + Append_Elmt (State_Id, Abstract_States (Pack_Id)); end Analyze_Abstract_State; -- Local variables @@ -9733,7 +9937,6 @@ package body Sem_Prag is State := First (Expressions (State)); while Present (State) loop Analyze_Abstract_State (State); - Next (State); end loop; @@ -10455,6 +10658,73 @@ package body Sem_Prag is end if; end AST_Entry; + ------------------------------------------------------------------ + -- Async_Readers/Async_Writers/Effective_Reads/Effective_Writes -- + ------------------------------------------------------------------ + + -- pragma Asynch_Readers ( identifier [, boolean_EXPRESSION] ); + -- pragma Asynch_Writers ( identifier [, boolean_EXPRESSION] ); + -- pragma Effective_Reads ( identifier [, boolean_EXPRESSION] ); + -- pragma Effective_Writes ( identifier [, boolean_EXPRESSION] ); + + when Pragma_Async_Readers | + Pragma_Async_Writers | + Pragma_Effective_Reads | + Pragma_Effective_Writes => + Async_Effective : declare + Duplic : Node_Id; + Obj_Id : Entity_Id; + + begin + GNAT_Pragma; + Check_No_Identifiers; + Check_At_Least_N_Arguments (1); + Check_At_Most_N_Arguments (2); + Check_Arg_Is_Local_Name (Arg1); + + Arg1 := Get_Pragma_Arg (Arg1); + + -- Perform minimal verification to ensure that the argument is at + -- least a variable. Subsequent finer grained checks will be done + -- at the end of the declarative region the contains the pragma. + + if Is_Entity_Name (Arg1) and then Present (Entity (Arg1)) then + Obj_Id := Entity (Get_Pragma_Arg (Arg1)); + + -- It is not efficient to examine preceding statements in order + -- to detect duplicate pragmas as Boolean aspects may appear + -- anywhere between the related object declaration and its + -- freeze point. As an alternative, inspect the contents of the + -- variable contract. + + if Ekind (Obj_Id) = E_Variable then + Duplic := Get_Pragma (Obj_Id, Prag_Id); + + if Present (Duplic) then + Error_Msg_Name_1 := Pname; + Error_Msg_Sloc := Sloc (Duplic); + Error_Msg_N ("pragma % duplicates pragma declared #", N); + + -- Chain the pragma on the contract for further processing. + -- This also aids in detecting duplicates. + + else + Add_Contract_Item (N, Obj_Id); + end if; + + -- The minimum legality requirements have been met, do not + -- fall through to the error message. + + return; + end if; + end if; + + -- If we get here, then the pragma applies to a non-object + -- construct, issue a generic error. + + Error_Pragma ("pragma % must apply to a volatile object"); + end Async_Effective; + ------------------ -- Asynchronous -- ------------------ @@ -18208,7 +18478,6 @@ package body Sem_Prag is Set_SPARK_Pragma_Inherited (Spec_Id, False); Set_SPARK_Aux_Pragma (Spec_Id, N); Set_SPARK_Aux_Pragma_Inherited (Spec_Id, True); - return; -- The pragma applies to a subprogram declaration @@ -22244,6 +22513,56 @@ package body Sem_Prag is return False; end Appears_In; + ------------------------------- + -- Check_External_Properties -- + ------------------------------- + + procedure Check_External_Properties + (Item : Node_Id; + AR : Boolean; + AW : Boolean; + ER : Boolean; + EW : Boolean) + is + begin + -- All properties enabled + + if AR and then AW and then ER and then EW then + null; + + -- Async_Readers + Effective_Writes + -- Async_Readers + Async_Writers + Effective_Writes + + elsif AR and then EW and then not ER then + null; + + -- Async_Writers + Effective_Reads + -- Async_Readers + Async_Writers + Effective_Reads + + elsif AW and then ER and then not EW then + null; + + -- Async_Readers + Async_Writers + + elsif AR and then AW and then not ER and then not EW then + null; + + -- Async_Readers + + elsif AR and then not AW and then not ER and then not EW then + null; + + -- Async_Writers + + elsif AW and then not AR and then not ER and then not EW then + null; + + else + Error_Msg_N + ("illegal combination of external state properties", Item); + end if; + end Check_External_Properties; + ---------------- -- Check_Kind -- ---------------- @@ -22995,18 +23314,20 @@ package body Sem_Prag is Pragma_Ada_12 => -1, Pragma_Ada_2012 => -1, Pragma_All_Calls_Remote => -1, - Pragma_Allow_Integer_Address => 0, + Pragma_Allow_Integer_Address => 0, Pragma_Annotate => -1, Pragma_Assert => -1, Pragma_Assert_And_Cut => -1, Pragma_Assertion_Policy => 0, Pragma_Assume => -1, Pragma_Assume_No_Invalid_Values => 0, - Pragma_Attribute_Definition => +3, + Pragma_Async_Readers => 0, + Pragma_Async_Writers => 0, Pragma_Asynchronous => -1, Pragma_Atomic => 0, Pragma_Atomic_Components => 0, Pragma_Attach_Handler => -1, + Pragma_Attribute_Definition => +3, Pragma_Check => 99, Pragma_Check_Float_Overflow => 0, Pragma_Check_Name => 0, @@ -23038,6 +23359,8 @@ package body Sem_Prag is Pragma_Disable_Atomic_Synchronization => -1, Pragma_Discard_Names => 0, Pragma_Dispatching_Domain => -1, + Pragma_Effective_Reads => 0, + Pragma_Effective_Writes => 0, Pragma_Elaborate => -1, Pragma_Elaborate_All => -1, Pragma_Elaborate_Body => -1, diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index 8dcee63..bb57d99 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -60,6 +60,13 @@ package Sem_Prag is -- Perform full analysis of delayed pragma Depends. This routine is also -- capable of performing basic analysis of pragma Refined_Depends. + procedure Analyze_External_State_In_Decl_Part + (N : Node_Id; + Expr_Val : out Boolean); + -- Perform full analysis of delayed pragmas Async_Readers, Async_Writers, + -- Effective_Reads and Effective_Writes. Flag Expr_Val contains the Boolean + -- argument of the pragma or a default True if no argument is present. + procedure Analyze_Global_In_Decl_Part (N : Node_Id); -- Perform full analysis of delayed pragma Global. This routine is also -- capable of performing basic analysis of pragma Refind_Global. @@ -121,6 +128,17 @@ package Sem_Prag is -- whether -gnata was used, if so, then the call has no effect, otherwise -- Is_Ignored (but not Is_Disabled) is set True. + procedure Check_External_Properties + (Item : Node_Id; + AR : Boolean; + AW : Boolean; + ER : Boolean; + EW : Boolean); + -- Flags AR, AW, ER and EW denote the static values of external properties + -- Async_Readers, Async_Writers, Effective_Reads and Effective_Writes. Item + -- is the related variable or state. Ensure the legality of the permutation + -- and if this is not the case, issue an error. + function Delay_Config_Pragma_Analyze (N : Node_Id) return Boolean; -- N is a pragma appearing in a configuration pragma file. Most such -- pragmas are analyzed when the file is read, before parsing and analyzing diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 3dca78e..e86ca31 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -4249,6 +4249,32 @@ package body Sem_Res is Check_Unset_Reference (A); end if; + -- The following checks are only relevant in formal verification + -- mode as they are not standard Ada legality rule. + + if GNATprove_Mode + and then Is_Volatile_Object (A) + then + -- A volatile object may act as an actual parameter when the + -- corresponding formal is of a non-scalar volatile type. + + if Is_Volatile (Etype (F)) + and then not Is_Scalar_Type (Etype (F)) + then + null; + + -- A volatile object may act as an actual parameter in a call + -- to an instance of Unchecked_Conversion. + + elsif Is_Unchecked_Conversion_Instance (Nam) then + null; + + else + Error_Msg_N + ("volatile object cannot act as actual in a call", A); + end if; + end if; + Next_Actual (A); -- Case where actual is not present @@ -6322,7 +6348,12 @@ package body Sem_Res is -- Used to resolve identifiers and expanded names procedure Resolve_Entity_Name (N : Node_Id; Typ : Entity_Id) is - E : constant Entity_Id := Entity (N); + E : constant Entity_Id := Entity (N); + Par : Node_Id; + Prev : Node_Id; + + Usage_OK : Boolean := False; + -- Flag set when the use of a volatile object agrees with its context begin -- If garbage from errors, set to Any_Type and return @@ -6425,6 +6456,72 @@ package body Sem_Res is Eval_Entity_Name (N); end if; + + -- The following checks are only relevant in formal verification mode as + -- they are not standard Ada legality rule. A volatile object subject to + -- enabled properties Async_Writers or Effective_Reads must appear in a + -- specific context. + + if GNATprove_Mode + and then Ekind (E) = E_Variable + and then Is_Volatile_Object (E) + and then + (Async_Writers_Enabled (E) + or else Effective_Reads_Enabled (E)) + then + Par := Parent (N); + Prev := N; + while Present (Par) loop + + -- The variable can appear on either side of an assignment + + if Nkind (Par) = N_Assignment_Statement then + Usage_OK := True; + exit; + + -- The variable is part of the initialization expression of an + -- object. Ensure that the climb of the parent chain came from the + -- expression side and not from the name side. + + elsif Nkind (Par) = N_Object_Declaration + and then Present (Expression (Par)) + and then Prev = Expression (Par) + then + Usage_OK := True; + exit; + + -- The variable appears as an actual parameter in a call to an + -- instance of Unchecked_Conversion whose result is renamed. + + elsif Nkind (Par) = N_Function_Call + and then Is_Unchecked_Conversion_Instance (Entity (Name (Par))) + and then Nkind (Parent (Par)) = N_Object_Renaming_Declaration + then + Usage_OK := True; + exit; + + -- Assume that references to volatile objects that appear as + -- actual parameters in a procedure call are always legal. The + -- full legality check is done when the actuals are resolved. + + elsif Nkind (Par) = N_Procedure_Call_Statement then + Usage_OK := True; + exit; + + -- Prevent the search from going too far + + elsif Is_Body_Or_Package_Declaration (Par) then + exit; + end if; + + Prev := Par; + Par := Parent (Par); + end loop; + + if not Usage_OK then + Error_Msg_N ("volatile object cannot appear in this context", N); + end if; + end if; end Resolve_Entity_Name; ------------------- diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 15c6a25..6ba2a16 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -113,6 +113,13 @@ package body Sem_Util is -- components in the selected variant to determine whether all of them -- have a default. + function Has_Enabled_Property + (Extern : Node_Id; + Prop_Nam : Name_Id) return Boolean; + -- Subsidiary to routines Async_xxx_Enabled and Effective_xxx_Enabled. + -- Given pragma External, determine whether it contains a property denoted + -- by its name Prop_Nam and if it does, whether its expression is True. + function Has_Null_Extension (T : Entity_Id) return Boolean; -- T is a derived tagged type. Check whether the type extension is null. -- If the parent type is fully initialized, T can be treated as such. @@ -342,6 +349,27 @@ package body Sem_Util is else raise Program_Error; end if; + + -- Contract items related to variables. The applicable pragmas are: + -- Async_Readers + -- Async_Writers + -- Effective_Reads + -- Effective_Writes + + elsif Ekind (Id) = E_Variable then + if Nam_In (Nam, Name_Async_Readers, + Name_Async_Writers, + Name_Effective_Reads, + Name_Effective_Writes) + then + Set_Next_Pragma (Prag, Classifications (Items)); + Set_Classifications (Items, Prag); + + -- The pragma is not a proper contract item + + else + raise Program_Error; + end if; end if; end Add_Contract_Item; @@ -525,6 +553,40 @@ package body Sem_Util is end if; end Apply_Compile_Time_Constraint_Error; + --------------------------- + -- Async_Readers_Enabled -- + --------------------------- + + function Async_Readers_Enabled (Id : Entity_Id) return Boolean is + begin + if Ekind (Id) = E_Abstract_State then + return + Has_Enabled_Property + (Extern => Get_Pragma (Id, Pragma_External), + Prop_Nam => Name_Async_Readers); + + else pragma Assert (Ekind (Id) = E_Variable); + return Present (Get_Pragma (Id, Pragma_Async_Readers)); + end if; + end Async_Readers_Enabled; + + --------------------------- + -- Async_Writers_Enabled -- + --------------------------- + + function Async_Writers_Enabled (Id : Entity_Id) return Boolean is + begin + if Ekind (Id) = E_Abstract_State then + return + Has_Enabled_Property + (Extern => Get_Pragma (Id, Pragma_External), + Prop_Nam => Name_Async_Writers); + + else pragma Assert (Ekind (Id) = E_Variable); + return Present (Get_Pragma (Id, Pragma_Async_Writers)); + end if; + end Async_Writers_Enabled; + -------------------------------------- -- Available_Full_View_Of_Component -- -------------------------------------- @@ -4730,6 +4792,40 @@ package body Sem_Util is end if; end Effective_Extra_Accessibility; + ----------------------------- + -- Effective_Reads_Enabled -- + ----------------------------- + + function Effective_Reads_Enabled (Id : Entity_Id) return Boolean is + begin + if Ekind (Id) = E_Abstract_State then + return + Has_Enabled_Property + (Extern => Get_Pragma (Id, Pragma_External), + Prop_Nam => Name_Effective_Reads); + + else pragma Assert (Ekind (Id) = E_Variable); + return Present (Get_Pragma (Id, Pragma_Effective_Reads)); + end if; + end Effective_Reads_Enabled; + + ------------------------------ + -- Effective_Writes_Enabled -- + ------------------------------ + + function Effective_Writes_Enabled (Id : Entity_Id) return Boolean is + begin + if Ekind (Id) = E_Abstract_State then + return + Has_Enabled_Property + (Extern => Get_Pragma (Id, Pragma_External), + Prop_Nam => Name_Effective_Writes); + + else pragma Assert (Ekind (Id) = E_Variable); + return Present (Get_Pragma (Id, Pragma_Effective_Writes)); + end if; + end Effective_Writes_Enabled; + ------------------------------ -- Enclosing_Comp_Unit_Node -- ------------------------------ @@ -7062,6 +7158,76 @@ package body Sem_Util is return False; end Has_Discriminant_Dependent_Constraint; + -------------------------- + -- Has_Enabled_Property -- + -------------------------- + + function Has_Enabled_Property + (Extern : Node_Id; + Prop_Nam : Name_Id) return Boolean + is + Prop : Node_Id; + Props : Node_Id := Empty; + + begin + -- The related abstract state or variable do not have an Extern pragma, + -- the property in question cannot be set. + + if No (Extern) then + return False; + + elsif Nkind (Extern) = N_Component_Association then + Props := Expression (Extern); + end if; + + -- External state with properties + + if Present (Props) then + + -- Multiple properties appear as an aggregate + + if Nkind (Props) = N_Aggregate then + + -- Simple property form + + Prop := First (Expressions (Props)); + while Present (Prop) loop + if Chars (Prop) = Prop_Nam then + return True; + end if; + + Next (Prop); + end loop; + + -- Property with expression form + + Prop := First (Component_Associations (Props)); + while Present (Prop) loop + if Chars (Prop) = Prop_Nam then + return Is_True (Expr_Value (Expression (Prop))); + end if; + + Next (Prop); + end loop; + + -- Pragma Extern contains properties, but not the one we want + + return False; + + -- Single property + + else + return Chars (Prop) = Prop_Nam; + end if; + + -- An external state defined without any properties defaults all + -- properties to True; + + else + return True; + end if; + end Has_Enabled_Property; + -------------------- -- Has_Infinities -- -------------------- @@ -10669,6 +10835,31 @@ package body Sem_Util is return (U /= 0); end Is_True; + -------------------------------------- + -- Is_Unchecked_Conversion_Instance -- + -------------------------------------- + + function Is_Unchecked_Conversion_Instance (Id : Entity_Id) return Boolean is + Gen_Par : Entity_Id; + + begin + -- Look for a function whose generic parent is the predefined intrinsic + -- function Unchecked_Conversion. + + if Ekind (Id) = E_Function then + Gen_Par := Generic_Parent (Parent (Id)); + + return + Present (Gen_Par) + and then Chars (Gen_Par) = Name_Unchecked_Conversion + and then Is_Intrinsic_Subprogram (Gen_Par) + and then Is_Predefined_File_Name + (Unit_File_Name (Get_Source_Unit (Gen_Par))); + end if; + + return False; + end Is_Unchecked_Conversion_Instance; + ------------------------------- -- Is_Universal_Numeric_Type -- ------------------------------- @@ -11017,12 +11208,12 @@ package body Sem_Util is function Is_Volatile_Object (N : Node_Id) return Boolean is - function Object_Has_Volatile_Components (N : Node_Id) return Boolean; - -- Determines if given object has volatile components - function Is_Volatile_Prefix (N : Node_Id) return Boolean; -- If prefix is an implicit dereference, examine designated type + function Object_Has_Volatile_Components (N : Node_Id) return Boolean; + -- Determines if given object has volatile components + ------------------------ -- Is_Volatile_Prefix -- ------------------------ @@ -11077,7 +11268,13 @@ package body Sem_Util is -- Start of processing for Is_Volatile_Object begin - if Is_Volatile (Etype (N)) + if Nkind (N) = N_Defining_Identifier then + return Is_Volatile (N) or else Is_Volatile (Etype (N)); + + elsif Nkind (N) = N_Expanded_Name then + return Is_Volatile_Object (Entity (N)); + + elsif Is_Volatile (Etype (N)) or else (Is_Entity_Name (N) and then Is_Volatile (Entity (N))) then return True; diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 4c6dde9..ba76ca6 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -47,8 +47,12 @@ package Sem_Util is -- Add pragma Prag to the contract of an entry, a package [body] or a -- subprogram [body] denoted by Id. The following are valid pragmas: -- Abstract_States + -- Async_Readers + -- Async_Writers -- Contract_Cases -- Depends + -- Effective_Reads + -- Effective_Writes -- Global -- Initial_Condition -- Initializes @@ -120,6 +124,16 @@ package Sem_Util is -- not end with a ? (this is used when the caller wants to parameterize -- whether an error or warning is given. + function Async_Readers_Enabled (Id : Entity_Id) return Boolean; + -- Given the entity of an abstract state or a variable, determine whether + -- Id is subject to external property Async_Readers and if it is, the + -- related expression evaluates to True. + + function Async_Writers_Enabled (Id : Entity_Id) return Boolean; + -- Given the entity of an abstract state or a variable, determine whether + -- Id is subject to external property Async_Writers and if it is, the + -- related expression evaluates to True. + function Available_Full_View_Of_Component (T : Entity_Id) return Boolean; -- If at the point of declaration an array type has a private or limited -- component, several array operations are not avaiable on the type, and @@ -485,6 +499,16 @@ package Sem_Util is -- Same as Einfo.Extra_Accessibility except thtat object renames -- are looked through. + function Effective_Reads_Enabled (Id : Entity_Id) return Boolean; + -- Given the entity of an abstract state or a variable, determine whether + -- Id is subject to external property Effective_Reads and if it is, the + -- related expression evaluates to True. + + function Effective_Writes_Enabled (Id : Entity_Id) return Boolean; + -- Given the entity of an abstract state or a variable, determine whether + -- Id is subject to external property Effective_Writes and if it is, the + -- related expression evaluates to True. + function Enclosing_Comp_Unit_Node (N : Node_Id) return Node_Id; -- Returns the enclosing N_Compilation_Unit Node that is the root of a -- subtree containing N. @@ -1164,6 +1188,10 @@ package Sem_Util is -- operand (i.e. is either 0 for False, or 1 for True). This function tests -- if it is True (i.e. non-zero). + function Is_Unchecked_Conversion_Instance (Id : Entity_Id) return Boolean; + -- Determine whether an arbitrary entity denotes an instance of function + -- Ada.Unchecked_Conversion. + function Is_Universal_Numeric_Type (T : Entity_Id) return Boolean; pragma Inline (Is_Universal_Numeric_Type); -- True if T is Universal_Integer or Universal_Real diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index e036c5f..866332e 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -7240,7 +7240,11 @@ package Sinfo is -- establish dependencies between subprogram or package inputs and -- outputs. Currently the following pragmas appear in this list: -- Abstract_States + -- Async_Readers + -- Async_Writers -- Depends + -- Effective_Reads + -- Effective_Writes -- Global -- Initial_Condition -- Initializes diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index 576d89e..fe4000a 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -460,6 +460,8 @@ package Snames is Name_Assert : constant Name_Id := N + $; -- Ada 05 Name_Assert_And_Cut : constant Name_Id := N + $; -- GNAT + Name_Async_Readers : constant Name_Id := N + $; -- GNAT + Name_Async_Writers : constant Name_Id := N + $; -- GNAT Name_Asynchronous : constant Name_Id := N + $; Name_Atomic : constant Name_Id := N + $; Name_Atomic_Components : constant Name_Id := N + $; @@ -486,6 +488,8 @@ package Snames is Name_Debug : constant Name_Id := N + $; -- GNAT Name_Depends : constant Name_Id := N + $; -- GNAT + Name_Effective_Reads : constant Name_Id := N + $; -- GNAT + Name_Effective_Writes : constant Name_Id := N + $; -- GNAT Name_Elaborate : constant Name_Id := N + $; -- Ada 83 Name_Elaborate_All : constant Name_Id := N + $; Name_Elaborate_Body : constant Name_Id := N + $; @@ -1788,6 +1792,8 @@ package Snames is Pragma_All_Calls_Remote, Pragma_Assert, Pragma_Assert_And_Cut, + Pragma_Async_Readers, + Pragma_Async_Writers, Pragma_Asynchronous, Pragma_Atomic, Pragma_Atomic_Components, @@ -1807,6 +1813,8 @@ package Snames is Pragma_CPP_Vtable, Pragma_Debug, Pragma_Depends, + Pragma_Effective_Reads, + Pragma_Effective_Writes, Pragma_Elaborate, Pragma_Elaborate_All, Pragma_Elaborate_Body, |