OpenE2K
/
gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[multiple changes] 

2014-01-27  Robert Dewar  <dewar@adacore.com>

	* a-wichha.adb (Character_Set_Version): Change to output proper
	value.

2014-01-27  Hristian Kirtchev  <kirtchev@adacore.com>

	* einfo.adb (Is_Input_Only_State): Removed.
	(Is_Non_Volatile_State): Removed.
	(Is_Output_State): Removed.
	* einfo.ads (Is_Input_Only_State): Remove attribute and
	subprogram. Update related entity.
	(Is_Non_Volatile_State):
	Remove attribute and subprogram. Update related entity.
	(Is_Output_State): Removed attribute and subprogram. Update
	related entity.
	* exp_ch6.adb (Expand_Subprogram_Contract): Update comment on
	generated code.
	* sem_ch3.adb (Analyze_Declarations): Analyze the contract of
	an object, not just variables.
	(Analyze_Object_Contract): New routine.
	(Analyze_Variable_Contract): Removed.
	(Process_Discriminants): Detect an illegal use of volatile
	discriminant in SPARK mode.
	* sem_ch5.adb (Analyze_Iterator_Specification):
	Detect an illegal use of volatile loop variable.
	(Analyze_Loop_Parameter_Specification): Detect an illegal use
	of volatile loop variable.
	* sem_ch6.adb (Process_Formals): Update the volatile object
	detection. Detect an illegal formal of mode IN OUT or OUT in
	SPARK mode. Enhance the error messages with references.
	* sem_ch12.adb (Instantiate_Object): Update the volatile object
	detection. Enhance the error messages with references.
	* sem_prag.adb (Analyze_Abstract_State): Enhance the error
	messages with references.
	(Analyze_Contract_Case): Enhance the error messages with references.
	(Analyze_External_Property): Call Check_Duplicate_Property to process
	an external property.
	(Analyze_External_Property_In_Decl_Part): New routine.
	(Analyze_External_State_In_Decl_Part): Removed.
	(Analyze_Global_Item): Detect an illegal
	use of a volatile constant. Detect an illegal use
	of a variable with enabled Effective_Reads. Enhance
	the error messages with references. Remove obsolete
	checks concerning Input_Only and Output_Only states.
	(Analyze_Initialization_Item): Enhance the error messages
	with references.
	(Analyze_Initializes_In_Decl_Part): Do not
	collect the states and variables when the initialization list
	is null.
	(Analyze_Input_Item): Enhance the error messages with references.
	(Analyze_Input_Output): Enhance the error messages with references.
	(Analyze_Pragma): Enhance the error messages with references.
	(Analyze_Refinement_Clause): Code reformatting.
	(Analyze_Refined_Depends_In_Decl_Part):
	Rename global variable Global to Reg_Global and update all
	occurrences. Add local variables D7 and D8. Update the error
	messages with references. Update the call to Collect_Global_Items.
	(Analyze_Refined_Global_In_Decl_Part): Add local variables
	Has_Proof_In_State, Proof_In_Constits and Proof_In_Items. Update
	the call to Collect_Global_Items.  Account for a Proof_In state
	in null / useless refinement checks. Verify the coverage of
	Proof_In states.
	(Check_Dependency_Clause): Remove local variable
	Out_Constits. Remove the retrieval and removal of constituents
	for an Output_Only state. Remove the reporting of unused
	Output_Only state constituents.
	(Check_Duplicate_Mode): Enhance
	the error message with a reference.
	(Check_Duplicate_Property): New routine.
	(Check_Duplicate_Option): Enhance the error message with a reference.
	(Check_External_Properties): Enhance the error message with a reference.
	(Check_Function_Return): Enhance the error message with a reference.
	(Check_In_Out_States): Update
	comment on usage. Add a specialized error message for Proof_In
	constituents. Enhance the error message with a reference.
	(Check_Input_States): Update comment on usage. Account for
	possible Proof_In constituents. Enhance the error message
	with a areference.
	(Check_Matching_Constituent): Enhance the error message with a
	reference.
	(Check_Matching_State): Enchance the error message with a reference.
	(Check_Mode): Add local variable From_Global. Update the call to
	Find_Mode.  Emit more precise error messages concerning extra items
	(Check_Mode_Restriction_In_Enclosing_Context): Consider
	pragma Refined_Global.	Enhance the error message with a
	reference.
	(Check_Mode_Restriction_In_Function): Enhance the error message with
	a reference.
	(Check_Output_States): Update comment on usage. Add local variable
	Posted.  Account for possible Proof_In constituents. Produce a detailed
	list of missing constituents.
	(Check_Proof_In_States): New routine.
	(Check_Refined_Global_Item): Handle Proof_In
	constituents. Enchance the error message with a reference.
	(Collect_Global_Items): Add formal parameters Proof_In_Items
	and Has_Proof_In_State. Update the comment on usage. Account
	for Proof_In items.
	(Create_Or_Modify_Clause): Enchance
	the error message with a reference.
	(Find_Mode): Add
	formal parameter From_Global. Update the comment on usage.
	Detect when the mode is governed by pragma [Refined_]Global.
	(Output_Constituents): Removed.
	(Report_Extra_Constituents):
	Report extra Proof_In constituents.
	(Report_Unused_Constituents): Removed.
	(Usage_Error): Code reformatting. Enhance the error
	messages with reference.
	* sem_prag.ads (Analyze_External_Property_In_Decl_Part): New routine.
	(Analyze_External_State_In_Decl_Part): Removed.
	* sem_res.adb (Resolve_Actuals): Update the volatile object
	detection. Enhance the error message with a reference.
	(Resolve_Entity_Name): Update the volatile object
	detection. Enhance the error message with a reference.
	* sem_util.adb (Is_Refined_State): Add a guard to avoid a crash.
	(Is_SPARK_Volatile_Object): New routine.
	(Has_Volatile_Component): New routine.
	* sem_util.ads (Is_Delegate): Alphabetized.
	(Is_SPARK_Volatile_Object): New routine.
	(Has_Volatile_Component): New routine.
	* snames.ads-tmpl: Remove names Name_Input_Only and Name_Output_Only.

2014-01-27  Ed Schonberg  <schonberg@adacore.com>

	* sem_attr.adb: Resolve fully prefix of 'Update.

From-SVN: r207138
This commit is contained in:
Arnaud Charlet 2014-01-27 17:35:08 +01:00
parent 904e5ccd59
commit f1bd0415ad
16 changed files with 848 additions and 499 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

127
gcc/ada/ChangeLog
View File

@ -1,3 +1,130 @@
2014-01-27 Robert Dewar <dewar@adacore.com>
* a-wichha.adb (Character_Set_Version): Change to output proper
value.
2014-01-27 Hristian Kirtchev <kirtchev@adacore.com>
* einfo.adb (Is_Input_Only_State): Removed.
(Is_Non_Volatile_State): Removed.
(Is_Output_State): Removed.
* einfo.ads (Is_Input_Only_State): Remove attribute and
subprogram. Update related entity.
(Is_Non_Volatile_State):
Remove attribute and subprogram. Update related entity.
(Is_Output_State): Removed attribute and subprogram. Update
related entity.
* exp_ch6.adb (Expand_Subprogram_Contract): Update comment on
generated code.
* sem_ch3.adb (Analyze_Declarations): Analyze the contract of
an object, not just variables.
(Analyze_Object_Contract): New routine.
(Analyze_Variable_Contract): Removed.
(Process_Discriminants): Detect an illegal use of volatile
discriminant in SPARK mode.
* sem_ch5.adb (Analyze_Iterator_Specification):
Detect an illegal use of volatile loop variable.
(Analyze_Loop_Parameter_Specification): Detect an illegal use
of volatile loop variable.
* sem_ch6.adb (Process_Formals): Update the volatile object
detection. Detect an illegal formal of mode IN OUT or OUT in
SPARK mode. Enhance the error messages with references.
* sem_ch12.adb (Instantiate_Object): Update the volatile object
detection. Enhance the error messages with references.
* sem_prag.adb (Analyze_Abstract_State): Enhance the error
messages with references.
(Analyze_Contract_Case): Enhance the error messages with references.
(Analyze_External_Property): Call Check_Duplicate_Property to process
an external property.
(Analyze_External_Property_In_Decl_Part): New routine.
(Analyze_External_State_In_Decl_Part): Removed.
(Analyze_Global_Item): Detect an illegal
use of a volatile constant. Detect an illegal use
of a variable with enabled Effective_Reads. Enhance
the error messages with references. Remove obsolete
checks concerning Input_Only and Output_Only states.
(Analyze_Initialization_Item): Enhance the error messages
with references.
(Analyze_Initializes_In_Decl_Part): Do not
collect the states and variables when the initialization list
is null.
(Analyze_Input_Item): Enhance the error messages with references.
(Analyze_Input_Output): Enhance the error messages with references.
(Analyze_Pragma): Enhance the error messages with references.
(Analyze_Refinement_Clause): Code reformatting.
(Analyze_Refined_Depends_In_Decl_Part):
Rename global variable Global to Reg_Global and update all
occurrences. Add local variables D7 and D8. Update the error
messages with references. Update the call to Collect_Global_Items.
(Analyze_Refined_Global_In_Decl_Part): Add local variables
Has_Proof_In_State, Proof_In_Constits and Proof_In_Items. Update
the call to Collect_Global_Items. Account for a Proof_In state
in null / useless refinement checks. Verify the coverage of
Proof_In states.
(Check_Dependency_Clause): Remove local variable
Out_Constits. Remove the retrieval and removal of constituents
for an Output_Only state. Remove the reporting of unused
Output_Only state constituents.
(Check_Duplicate_Mode): Enhance
the error message with a reference.
(Check_Duplicate_Property): New routine.
(Check_Duplicate_Option): Enhance the error message with a reference.
(Check_External_Properties): Enhance the error message with a reference.
(Check_Function_Return): Enhance the error message with a reference.
(Check_In_Out_States): Update
comment on usage. Add a specialized error message for Proof_In
constituents. Enhance the error message with a reference.
(Check_Input_States): Update comment on usage. Account for
possible Proof_In constituents. Enhance the error message
with a areference.
(Check_Matching_Constituent): Enhance the error message with a
reference.
(Check_Matching_State): Enchance the error message with a reference.
(Check_Mode): Add local variable From_Global. Update the call to
Find_Mode. Emit more precise error messages concerning extra items
(Check_Mode_Restriction_In_Enclosing_Context): Consider
pragma Refined_Global. Enhance the error message with a
reference.
(Check_Mode_Restriction_In_Function): Enhance the error message with
a reference.
(Check_Output_States): Update comment on usage. Add local variable
Posted. Account for possible Proof_In constituents. Produce a detailed
list of missing constituents.
(Check_Proof_In_States): New routine.
(Check_Refined_Global_Item): Handle Proof_In
constituents. Enchance the error message with a reference.
(Collect_Global_Items): Add formal parameters Proof_In_Items
and Has_Proof_In_State. Update the comment on usage. Account
for Proof_In items.
(Create_Or_Modify_Clause): Enchance
the error message with a reference.
(Find_Mode): Add
formal parameter From_Global. Update the comment on usage.
Detect when the mode is governed by pragma [Refined_]Global.
(Output_Constituents): Removed.
(Report_Extra_Constituents):
Report extra Proof_In constituents.
(Report_Unused_Constituents): Removed.
(Usage_Error): Code reformatting. Enhance the error
messages with reference.
* sem_prag.ads (Analyze_External_Property_In_Decl_Part): New routine.
(Analyze_External_State_In_Decl_Part): Removed.
* sem_res.adb (Resolve_Actuals): Update the volatile object
detection. Enhance the error message with a reference.
(Resolve_Entity_Name): Update the volatile object
detection. Enhance the error message with a reference.
* sem_util.adb (Is_Refined_State): Add a guard to avoid a crash.
(Is_SPARK_Volatile_Object): New routine.
(Has_Volatile_Component): New routine.
* sem_util.ads (Is_Delegate): Alphabetized.
(Is_SPARK_Volatile_Object): New routine.
(Has_Volatile_Component): New routine.
* snames.ads-tmpl: Remove names Name_Input_Only and Name_Output_Only.
2014-01-27 Ed Schonberg <schonberg@adacore.com>
* sem_attr.adb: Resolve fully prefix of 'Update.
2014-01-27 Ben Brosgol <brosgol@adacore.com>
* gnat_rm.texi: Minor clarifications.

6
gcc/ada/a-wichha.adb
View File

@ -33,9 +33,13 @@ with Ada.Wide_Characters.Unicode; use Ada.Wide_Characters.Unicode;
package body Ada.Wide_Characters.Handling is
---------------------------
-- Character_Set_Version --
---------------------------
function Character_Set_Version return String is
begin
return "Unicode 6.2";
return "Unicode 4.0";
end Character_Set_Version;
---------------------

33
gcc/ada/einfo.adb
View File

@ -6912,28 +6912,6 @@ package body Einfo is
end if;
end Is_Ghost_Subprogram;
-------------------------
-- Is_Input_Only_State --
-------------------------
function Is_Input_Only_State (Id : E) return B is
begin
return
Ekind (Id) = E_Abstract_State
and then Has_Option (Id, Name_Input_Only);
end Is_Input_Only_State;
---------------------------
-- Is_Non_Volatile_State --
---------------------------
function Is_Non_Volatile_State (Id : E) return B is
begin
return
Ekind (Id) = E_Abstract_State
and then Has_Option (Id, Name_Non_Volatile);
end Is_Non_Volatile_State;
-------------------
-- Is_Null_State --
-------------------
@ -6944,17 +6922,6 @@ package body Einfo is
Ekind (Id) = E_Abstract_State and then Nkind (Parent (Id)) = N_Null;
end Is_Null_State;
---------------------
-- Is_Output_State --
---------------------
function Is_Output_Only_State (Id : E) return B is
begin
return
Ekind (Id) = E_Abstract_State
and then Has_Option (Id, Name_Output_Only);
end Is_Output_Only_State;
-----------------------------------
-- Is_Package_Or_Generic_Package --
-----------------------------------

18
gcc/ada/einfo.ads
View File

@ -2400,10 +2400,6 @@ package Einfo is
-- inherited by their instances. It is also set on the body entities
-- of inlined subprograms. See also Has_Pragma_Inline.
-- Is_Input_Only_State (synthesized)
-- Applies to all entities, true for abstract states that are subject to
-- option Input_Only.
-- Is_Instantiated (Flag126)
-- Defined in generic packages and generic subprograms. Set if the unit
-- is instantiated from somewhere in the extended main source unit. This
@ -2593,10 +2589,6 @@ package Einfo is
-- set right, at which point, these comments can be removed, and the
-- tests for static subtypes greatly simplified.
-- Is_Non_Volatile_State (synthesized)
-- Applies to all entities, true for abstract states that are subject to
-- option Non_Volatile.
-- Is_Null_Init_Proc (Flag178)
-- Defined in procedure entities. Set for generated init proc procedures
-- (used to initialize composite types), if the code for the procedure
@ -2637,10 +2629,6 @@ package Einfo is
-- Applies to all entities, true for ordinary fixed point types and
-- subtypes.
-- Is_Output_Only_State (synthesized)
-- Applies to all entities, true for abstract states that are subject to
-- option Output_Only.
-- Is_Package_Or_Generic_Package (synthesized)
-- Applies to all entities. True for packages and generic packages.
-- False for all other entities.
@ -5167,10 +5155,7 @@ package Einfo is
-- Has_Non_Null_Refinement (synth)
-- Has_Null_Refinement (synth)
-- Is_External_State (synth)
-- Is_Input_Only_State (synth)
-- Is_Null_State (synth)
-- Is_Output_Only_State (synth)
-- Is_Non_Volatile_State (synth)
-- E_Access_Protected_Subprogram_Type
-- Equivalent_Type (Node18)
@ -6787,10 +6772,7 @@ package Einfo is
function Is_Finalizer (Id : E) return B;
function Is_Ghost_Entity (Id : E) return B;
function Is_Ghost_Subprogram (Id : E) return B;
function Is_Input_Only_State (Id : E) return B;
function Is_Non_Volatile_State (Id : E) return B;
function Is_Null_State (Id : E) return B;
function Is_Output_Only_State (Id : E) return B;
function Is_Package_Or_Generic_Package (Id : E) return B;
function Is_Prival (Id : E) return B;
function Is_Protected_Component (Id : E) return B;

3
gcc/ada/exp_ch6.adb
View File

@ -9477,7 +9477,7 @@ package body Exp_Ch6 is
-- <postconditions from body>
-- <postconditions from spec>
-- <inherited postconditions>
-- <contract cases>
-- <contract case consequences>
-- <invariant check of function result (if applicable)>
-- <invariant and predicate checks of parameters>
-- end _Postconditions;
@ -9486,6 +9486,7 @@ package body Exp_Ch6 is
-- <preconditions from spec>
-- <preconditions from body>
-- <refined preconditions from body>
-- <contract case conditions>
-- <source declarations>
-- begin

4
gcc/ada/sem_attr.adb
View File

@ -6064,6 +6064,7 @@ package body Sem_Attr is
begin
Check_E1;
Check_Ada_2012_Attribute;
if not Is_Object_Reference (P) then
Error_Attr_P ("prefix of attribute % must denote an object");
@ -10477,8 +10478,11 @@ package body Sem_Attr is
-- Set the Etype of the aggregate to that of the prefix, even
-- though the aggregate may not be a proper representation of a
-- value of the type (missing or duplicated associations, etc.)
-- Complete resolution of the prefix. Note that in Ada 2012 it
-- can be a qualified expression that is e.g. an aggregate.
Set_Etype (Aggr, Typ);
Resolve (Prefix (N), Typ);
-- For an array type, resolve expressions with the component
-- type of the array.

4
gcc/ada/sem_ch12.adb
View File

@ -9846,11 +9846,11 @@ package body Sem_Ch12 is
if SPARK_Mode = On
and then Present (Actual)
and then Is_Volatile_Object (Actual)
and then Is_SPARK_Volatile_Object (Actual)
then
Error_Msg_N
("volatile object cannot act as actual in generic instantiation "
& "(SPARK RM 7.1.3(4))", Actual);
& "(SPARK RM 7.1.3(8))", Actual);
end if;
return List;

191
gcc/ada/sem_ch3.adb
View File

@ -91,10 +91,10 @@ 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
-- to be considered are:
procedure Analyze_Object_Contract (Obj_Id : Entity_Id);
-- Analyze all delayed aspects chained on the contract of object Obj_Id as
-- if they appeared at the end of the declarative region. The aspects to be
-- considered are:
-- Async_Readers
-- Async_Writers
-- Effective_Reads
@ -2478,10 +2478,8 @@ 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));
elsif Nkind (Decl) = N_Object_Declaration then
Analyze_Object_Contract (Defining_Entity (Decl));
end if;
Next (Decl);
@ -3071,6 +3069,106 @@ package body Sem_Ch3 is
end if;
end Analyze_Number_Declaration;
-----------------------------
-- Analyze_Object_Contract --
-----------------------------
procedure Analyze_Object_Contract (Obj_Id : Entity_Id) is
AR_Val : Boolean := False;
AW_Val : Boolean := False;
ER_Val : Boolean := False;
EW_Val : Boolean := False;
Items : Node_Id;
Nam : Name_Id;
Prag : Node_Id;
Seen : Boolean := False;
begin
if Ekind (Obj_Id) = E_Constant then
-- A constant cannot be volatile. This check is only relevant when
-- SPARK_Mode is on as it is not standard Ada legality rule. Do not
-- flag internally-generated constants that map generic formals to
-- actuals in instantiations.
if SPARK_Mode = On
and then Is_SPARK_Volatile_Object (Obj_Id)
and then No (Corresponding_Generic_Association (Parent (Obj_Id)))
then
Error_Msg_N
("constant cannot be volatile (SPARK RM 7.1.3(4))", Obj_Id);
end if;
else pragma Assert (Ekind (Obj_Id) = E_Variable);
-- The following checks are only relevant when SPARK_Mode is on as
-- they are not standard Ada legality rules.
if SPARK_Mode = On then
-- A non-volatile object cannot have volatile components
if not Is_SPARK_Volatile_Object (Obj_Id)
and then Has_Volatile_Component (Etype (Obj_Id))
then
Error_Msg_N
("non-volatile variable & cannot have volatile components "
& "(SPARK RM 7.1.3(6))", Obj_Id);
-- The declaration of a volatile object must appear at the library
-- level.
elsif Is_SPARK_Volatile_Object (Obj_Id)
and then not Is_Library_Level_Entity (Obj_Id)
then
Error_Msg_N
("volatile variable & must be declared at library level "
& "(SPARK RM 7.1.3(5))", Obj_Id);
end if;
end if;
-- Examine the contract
Items := Contract (Obj_Id);
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_Property_In_Decl_Part (Prag, AR_Val);
Seen := True;
elsif Nam = Name_Async_Writers then
Analyze_External_Property_In_Decl_Part (Prag, AW_Val);
Seen := True;
elsif Nam = Name_Effective_Reads then
Analyze_External_Property_In_Decl_Part (Prag, ER_Val);
Seen := True;
else pragma Assert (Nam = Name_Effective_Writes);
Analyze_External_Property_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 (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
end if;
end if;
end Analyze_Object_Contract;
--------------------------------
-- Analyze_Object_Declaration --
--------------------------------
@ -4889,73 +4987,6 @@ 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 declaration of a volatile variable must appear at the library
-- level. The check is only relevant when SPARK_Mode is on as it is not
-- standard Ada legality rule.
if SPARK_Mode = On
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 (SPARK RM "
& "7.1.3(3))", 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 --
--------------------------
@ -18076,6 +18107,16 @@ package body Sem_Ch3 is
end if;
end if;
-- A discriminant cannot be volatile. This check is only relevant
-- when SPARK_Mode is on as it is not standard Ada legality rule.
if SPARK_Mode = On
and then Is_SPARK_Volatile_Object (Defining_Identifier (Discr))
then
Error_Msg_N
("discriminant cannot be volatile (SPARK RM 7.1.3(6))", Discr);
end if;
Next (Discr);
end loop;

16
gcc/ada/sem_ch5.adb
View File

@ -1921,6 +1921,14 @@ package body Sem_Ch5 is
end loop;
end if;
end if;
-- A loop parameter cannot be volatile. This check is peformed only when
-- SPARK_Mode is on as it is not a standard Ada legality check.
if SPARK_Mode = On and then Is_SPARK_Volatile_Object (Ent) then
Error_Msg_N
("loop parameter cannot be volatile (SPARK RM 7.1.3(6))", Ent);
end if;
end Analyze_Iterator_Specification;
-------------------
@ -2550,6 +2558,14 @@ package body Sem_Ch5 is
end if;
end;
end if;
-- A loop parameter cannot be volatile. This check is peformed only when
-- SPARK_Mode is on as it is not a standard Ada legality check.
if SPARK_Mode = On and then Is_SPARK_Volatile_Object (Id) then
Error_Msg_N
("loop parameter cannot be volatile (SPARK RM 7.1.3(6))", Id);
end if;
end Analyze_Loop_Parameter_Specification;
----------------------------

23
gcc/ada/sem_ch6.adb
View File

@ -11233,17 +11233,26 @@ package body Sem_Ch6 is
Null_Exclusion_Static_Checks (Param_Spec);
end if;
-- A function cannot have a volatile formal parameter. The following
-- check is relevant when SPARK_Mode is on as it is not a standard
-- Ada legality rule.
-- The following checks are relevant when SPARK_Mode is on as these
-- are not standard Ada legality rules.
if SPARK_Mode = On
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 (SPARK RM "
& "7.1.3(6))", Formal);
-- A function cannot have a parameter of mode IN OUT or OUT
if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then
Error_Msg_N
("function cannot have parameter of mode `OUT` or `IN OUT` "
& "(SPARK RM 6.1)", Formal);
-- A function cannot have a volatile formal parameter
elsif Is_SPARK_Volatile_Object (Formal) then
Error_Msg_N
("function cannot have a volatile formal parameter (SPARK RM "
& "7.1.3(10))", Formal);
end if;
end if;
<<Continue>>

810
gcc/ada/sem_prag.adb
View File

File diff suppressed because it is too large Load Diff

2
gcc/ada/sem_prag.ads
View File

@ -60,7 +60,7 @@ 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
procedure Analyze_External_Property_In_Decl_Part
(N : Node_Id;
Expr_Val : out Boolean);
-- Perform full analysis of delayed pragmas Async_Readers, Async_Writers,

19
gcc/ada/sem_res.adb
View File

@ -4041,6 +4041,16 @@ package body Sem_Res is
then
Apply_Discriminant_Check (A, F_Typ);
-- For view conversions of a discriminated object, apply
-- check to object itself, the conversion alreay has the
-- proper type.
if Nkind (A) = N_Type_Conversion
and then Is_Constrained (Etype (Expression (A)))
then
Apply_Discriminant_Check (Expression (A), F_Typ);
end if;
elsif Is_Access_Type (F_Typ)
and then Is_Array_Type (Designated_Type (F_Typ))
and then Is_Constrained (Designated_Type (F_Typ))
@ -4254,7 +4264,7 @@ package body Sem_Res is
-- they are not standard Ada legality rule.
if SPARK_Mode = On
and then Is_Volatile_Object (A)
and then Is_SPARK_Volatile_Object (A)
then
-- A volatile object may act as an actual parameter when the
-- corresponding formal is of a non-scalar volatile type.
@ -4273,7 +4283,7 @@ package body Sem_Res is
else
Error_Msg_N
("volatile object cannot act as actual in a call (SPARK "
& "RM 7.1.3(8))", A);
& "RM 7.1.3(12))", A);
end if;
end if;
@ -6497,8 +6507,7 @@ package body Sem_Res is
-- standard Ada legality rules.
if SPARK_Mode = On
and then Ekind (E) = E_Variable
and then Is_Volatile_Object (E)
and then Is_SPARK_Volatile_Object (E)
and then
(Async_Writers_Enabled (E)
or else Effective_Reads_Enabled (E))
@ -6555,7 +6564,7 @@ package body Sem_Res is
if not Usage_OK then
Error_Msg_N
("volatile object cannot appear in this context (SPARK RM "
& "7.1.3(9))", N);
& "7.1.3(13))", N);
end if;
end if;
end Resolve_Entity_Name;

68
gcc/ada/sem_util.adb
View File

@ -3729,14 +3729,9 @@ package body Sem_Util is
else
Item_Id := Entity_Of (Item);
-- Defend against junk
if No (Item_Id) then
return False;
end if;
return
Ekind (Item_Id) = E_Abstract_State
Present (Item_Id)
and then Ekind (Item_Id) = E_Abstract_State
and then Has_Visible_Refinement (Item_Id);
end if;
end Is_Refined_State;
@ -8097,6 +8092,34 @@ package body Sem_Util is
end if;
end Has_Tagged_Component;
----------------------------
-- Has_Volatile_Component --
----------------------------
function Has_Volatile_Component (Typ : Entity_Id) return Boolean is
Comp : Entity_Id;
begin
if Has_Volatile_Components (Typ) then
return True;
elsif Is_Array_Type (Typ) then
return Is_Volatile (Component_Type (Typ));
elsif Is_Record_Type (Typ) then
Comp := First_Component (Typ);
while Present (Comp) loop
if Is_Volatile_Object (Comp) then
return True;
end if;
Comp := Next_Component (Comp);
end loop;
end if;
return False;
end Has_Volatile_Component;
-------------------------
-- Implementation_Kind --
-------------------------
@ -10827,6 +10850,37 @@ package body Sem_Util is
end if;
end Is_SPARK_Object_Reference;
------------------------------
-- Is_SPARK_Volatile_Object --
------------------------------
function Is_SPARK_Volatile_Object (N : Node_Id) return Boolean is
begin
if Nkind (N) = N_Defining_Identifier then
return Is_Volatile (N) or else Is_Volatile (Etype (N));
elsif Is_Entity_Name (N) then
return
Is_SPARK_Volatile_Object (Entity (N))
or else Is_Volatile (Etype (N));
elsif Nkind (N) = N_Expanded_Name then
return Is_SPARK_Volatile_Object (Entity (N));
elsif Nkind (N) = N_Indexed_Component then
return Is_SPARK_Volatile_Object (Prefix (N));
elsif Nkind (N) = N_Selected_Component then
return
Is_SPARK_Volatile_Object (Prefix (N))
or else
Is_SPARK_Volatile_Object (Selector_Name (N));
else
return False;
end if;
end Is_SPARK_Volatile_Object;
------------------
-- Is_Statement --
------------------

21
gcc/ada/sem_util.ads
View File

@ -886,6 +886,10 @@ package Sem_Util is
-- component is present. This function is used to check if "=" has to be
-- expanded into a bunch component comparisons.
function Has_Volatile_Component (Typ : Entity_Id) return Boolean;
-- Given an arbitrary type, determine whether it contains at least one
-- volatile component.
function Implementation_Kind (Subp : Entity_Id) return Name_Id;
-- Subp is a subprogram marked with pragma Implemented. Return the specific
-- implementation requirement which the pragma imposes. The return value is
@ -1015,6 +1019,11 @@ package Sem_Util is
-- First determine whether type T is an interface and then check whether
-- it is of protected, synchronized or task kind.
function Is_Delegate (T : Entity_Id) return Boolean;
-- Returns true if type T represents a delegate. A Delegate is the CIL
-- object used to represent access-to-subprogram types. This is only
-- relevant to CIL, will always return false for other targets.
function Is_Dependent_Component_Of_Mutable_Object
(Object : Node_Id) return Boolean;
-- Returns True if Object is the name of a subcomponent that depends on
@ -1165,6 +1174,13 @@ package Sem_Util is
function Is_SPARK_Object_Reference (N : Node_Id) return Boolean;
-- Determines if the tree referenced by N represents an object in SPARK
function Is_SPARK_Volatile_Object (N : Node_Id) return Boolean;
-- Determine whether an arbitrary node denotes a volatile object reference
-- according to the semantics of SPARK. To qualify as volatile, an object
-- must be subject to aspect/pragma Volatile or Atomic or have a [sub]type
-- subject to the same attributes. Note that volatile components do not
-- render an object volatile.
function Is_Statement (N : Node_Id) return Boolean;
pragma Inline (Is_Statement);
-- Check if the node N is a statement node. Note that this includes
@ -1215,11 +1231,6 @@ package Sem_Util is
-- Determine whether an operator is one of the intrinsics defined
-- in the DEC system extension.
function Is_Delegate (T : Entity_Id) return Boolean;
-- Returns true if type T represents a delegate. A Delegate is the CIL
-- object used to represent access-to-subprogram types. This is only
-- relevant to CIL, will always return false for other targets.
function Is_Variable
(N : Node_Id;
Use_Original_Node : Boolean := True) return Boolean;

2
gcc/ada/snames.ads-tmpl
View File

@ -724,7 +724,6 @@ package Snames is
Name_In_Out : constant Name_Id := N + $;
Name_Increases : constant Name_Id := N + $;
Name_Info : constant Name_Id := N + $;
Name_Input_Only : constant Name_Id := N + $;
Name_Internal : constant Name_Id := N + $;
Name_Link_Name : constant Name_Id := N + $;
Name_Lowercase : constant Name_Id := N + $;
@ -761,7 +760,6 @@ package Snames is
Name_Non_Volatile : constant Name_Id := N + $;
Name_On : constant Name_Id := N + $;
Name_Optional : constant Name_Id := N + $;
Name_Output_Only : constant Name_Id := N + $;
Name_Policy : constant Name_Id := N + $;
Name_Parameter_Types : constant Name_Id := N + $;
Name_Part_Of : constant Name_Id := N + $;