[multiple changes]
2013-10-13 Ed Schonberg <schonberg@adacore.com> * sem_ch3.adb: in Ada 2012 access_to_function types can have in-out parameters. (Derived_Type_Declaration): SPARK restriction must be flagged on the original node, since it may have been written as a subtype declaration. (Analyze_Subtype_Declaration): Do not enter name of entity in declaration if it is the current entity, because it may have been inserted in a previous analysis and it appears in the else_part of an if-statement that is rewritten during expansion. 2013-10-13 Yannick Moy <moy@adacore.com> * exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Remove procedure. (Expand_SPARK): Remove call to Expand_SPARK_N_Attribute_Reference and Expand_SPARK_N_Simple_Return_Statement. (Expand_SPARK_N_Simple_Return_Statement, Expand_SPARK_Simple_Function_Return): Remove procedures. From-SVN: r203502
This commit is contained in:
parent
409274f155
commit
cf895a0159
|
@ -1,3 +1,23 @@
|
||||||
|
2013-10-13 Ed Schonberg <schonberg@adacore.com>
|
||||||
|
|
||||||
|
* sem_ch3.adb: in Ada 2012 access_to_function types can have
|
||||||
|
in-out parameters.
|
||||||
|
(Derived_Type_Declaration): SPARK restriction
|
||||||
|
must be flagged on the original node, since it may have been
|
||||||
|
written as a subtype declaration.
|
||||||
|
(Analyze_Subtype_Declaration): Do not enter name of
|
||||||
|
entity in declaration if it is the current entity, because it may
|
||||||
|
have been inserted in a previous analysis and it appears in the
|
||||||
|
else_part of an if-statement that is rewritten during expansion.
|
||||||
|
|
||||||
|
2013-10-13 Yannick Moy <moy@adacore.com>
|
||||||
|
|
||||||
|
* exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Remove procedure.
|
||||||
|
(Expand_SPARK): Remove call to Expand_SPARK_N_Attribute_Reference and
|
||||||
|
Expand_SPARK_N_Simple_Return_Statement.
|
||||||
|
(Expand_SPARK_N_Simple_Return_Statement,
|
||||||
|
Expand_SPARK_Simple_Function_Return): Remove procedures.
|
||||||
|
|
||||||
2013-10-13 Vincent Celier <celier@adacore.com>
|
2013-10-13 Vincent Celier <celier@adacore.com>
|
||||||
|
|
||||||
* gnat_ugn.texi: Minor editing.
|
* gnat_ugn.texi: Minor editing.
|
||||||
|
|
|
@ -25,19 +25,15 @@
|
||||||
|
|
||||||
with Atree; use Atree;
|
with Atree; use Atree;
|
||||||
with Einfo; use Einfo;
|
with Einfo; use Einfo;
|
||||||
with Exp_Attr; use Exp_Attr;
|
|
||||||
with Exp_Ch4; use Exp_Ch4;
|
with Exp_Ch4; use Exp_Ch4;
|
||||||
with Exp_Ch6; use Exp_Ch6;
|
with Exp_Ch6; use Exp_Ch6;
|
||||||
with Exp_Dbug; use Exp_Dbug;
|
with Exp_Dbug; use Exp_Dbug;
|
||||||
with Exp_Util; use Exp_Util;
|
with Exp_Util; use Exp_Util;
|
||||||
with Rtsfind; use Rtsfind;
|
|
||||||
with Sem_Aux; use Sem_Aux;
|
with Sem_Aux; use Sem_Aux;
|
||||||
with Sem_Res; use Sem_Res;
|
with Sem_Res; use Sem_Res;
|
||||||
with Sem_Util; use Sem_Util;
|
with Sem_Util; use Sem_Util;
|
||||||
with Sinfo; use Sinfo;
|
with Sinfo; use Sinfo;
|
||||||
with Snames; use Snames;
|
|
||||||
with Stand; use Stand;
|
with Stand; use Stand;
|
||||||
with Tbuild; use Tbuild;
|
|
||||||
|
|
||||||
package body Exp_SPARK is
|
package body Exp_SPARK is
|
||||||
|
|
||||||
|
@ -51,18 +47,9 @@ package body Exp_SPARK is
|
||||||
-- * expansion of actuals to introduce necessary temporaries
|
-- * expansion of actuals to introduce necessary temporaries
|
||||||
-- * replacement of renaming by subprogram renamed
|
-- * replacement of renaming by subprogram renamed
|
||||||
|
|
||||||
procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id);
|
|
||||||
-- Expand attributes 'Old and 'Result only
|
|
||||||
|
|
||||||
procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
|
procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
|
||||||
-- Perform name evaluation for a renamed object
|
-- Perform name evaluation for a renamed object
|
||||||
|
|
||||||
procedure Expand_SPARK_N_Simple_Return_Statement (N : Node_Id);
|
|
||||||
-- Insert conversion on function return if necessary
|
|
||||||
|
|
||||||
procedure Expand_SPARK_Simple_Function_Return (N : Node_Id);
|
|
||||||
-- Expand simple return from function
|
|
||||||
|
|
||||||
procedure Expand_Potential_Renaming (N : Node_Id);
|
procedure Expand_Potential_Renaming (N : Node_Id);
|
||||||
-- N denotes a N_Identifier or N_Expanded_Name. If N references a renaming,
|
-- N denotes a N_Identifier or N_Expanded_Name. If N references a renaming,
|
||||||
-- replace N with the renamed object.
|
-- replace N with the renamed object.
|
||||||
|
@ -74,8 +61,6 @@ package body Exp_SPARK is
|
||||||
procedure Expand_SPARK (N : Node_Id) is
|
procedure Expand_SPARK (N : Node_Id) is
|
||||||
begin
|
begin
|
||||||
case Nkind (N) is
|
case Nkind (N) is
|
||||||
when N_Attribute_Reference =>
|
|
||||||
Expand_SPARK_N_Attribute_Reference (N);
|
|
||||||
|
|
||||||
-- Qualification of entity names in formal verification mode
|
-- Qualification of entity names in formal verification mode
|
||||||
-- is limited to the addition of a suffix for homonyms (see
|
-- is limited to the addition of a suffix for homonyms (see
|
||||||
|
@ -107,9 +92,6 @@ package body Exp_SPARK is
|
||||||
when N_Object_Renaming_Declaration =>
|
when N_Object_Renaming_Declaration =>
|
||||||
Expand_SPARK_N_Object_Renaming_Declaration (N);
|
Expand_SPARK_N_Object_Renaming_Declaration (N);
|
||||||
|
|
||||||
when N_Simple_Return_Statement =>
|
|
||||||
Expand_SPARK_N_Simple_Return_Statement (N);
|
|
||||||
|
|
||||||
-- In SPARK mode, no other constructs require expansion
|
-- In SPARK mode, no other constructs require expansion
|
||||||
|
|
||||||
when others =>
|
when others =>
|
||||||
|
@ -179,24 +161,6 @@ package body Exp_SPARK is
|
||||||
end if;
|
end if;
|
||||||
end Expand_SPARK_Call;
|
end Expand_SPARK_Call;
|
||||||
|
|
||||||
----------------------------------------
|
|
||||||
-- Expand_SPARK_N_Attribute_Reference --
|
|
||||||
----------------------------------------
|
|
||||||
|
|
||||||
procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id) is
|
|
||||||
Id : constant Attribute_Id := Get_Attribute_Id (Attribute_Name (N));
|
|
||||||
|
|
||||||
begin
|
|
||||||
case Id is
|
|
||||||
when Attribute_Old |
|
|
||||||
Attribute_Result =>
|
|
||||||
Expand_N_Attribute_Reference (N);
|
|
||||||
|
|
||||||
when others =>
|
|
||||||
null;
|
|
||||||
end case;
|
|
||||||
end Expand_SPARK_N_Attribute_Reference;
|
|
||||||
|
|
||||||
------------------------------------------------
|
------------------------------------------------
|
||||||
-- Expand_SPARK_N_Object_Renaming_Declaration --
|
-- Expand_SPARK_N_Object_Renaming_Declaration --
|
||||||
------------------------------------------------
|
------------------------------------------------
|
||||||
|
@ -208,80 +172,6 @@ package body Exp_SPARK is
|
||||||
Evaluate_Name (Name (N));
|
Evaluate_Name (Name (N));
|
||||||
end Expand_SPARK_N_Object_Renaming_Declaration;
|
end Expand_SPARK_N_Object_Renaming_Declaration;
|
||||||
|
|
||||||
--------------------------------------------
|
|
||||||
-- Expand_SPARK_N_Simple_Return_Statement --
|
|
||||||
--------------------------------------------
|
|
||||||
|
|
||||||
procedure Expand_SPARK_N_Simple_Return_Statement (N : Node_Id) is
|
|
||||||
begin
|
|
||||||
-- Defend against previous errors (i.e. the return statement calls a
|
|
||||||
-- function that is not available in configurable runtime).
|
|
||||||
|
|
||||||
if Present (Expression (N))
|
|
||||||
and then Nkind (Expression (N)) = N_Empty
|
|
||||||
then
|
|
||||||
return;
|
|
||||||
end if;
|
|
||||||
|
|
||||||
-- Distinguish the function and non-function cases:
|
|
||||||
|
|
||||||
case Ekind (Return_Applies_To (Return_Statement_Entity (N))) is
|
|
||||||
|
|
||||||
when E_Function |
|
|
||||||
E_Generic_Function =>
|
|
||||||
Expand_SPARK_Simple_Function_Return (N);
|
|
||||||
|
|
||||||
when E_Procedure |
|
|
||||||
E_Generic_Procedure |
|
|
||||||
E_Entry |
|
|
||||||
E_Entry_Family |
|
|
||||||
E_Return_Statement =>
|
|
||||||
null;
|
|
||||||
|
|
||||||
when others =>
|
|
||||||
raise Program_Error;
|
|
||||||
end case;
|
|
||||||
|
|
||||||
exception
|
|
||||||
when RE_Not_Available =>
|
|
||||||
return;
|
|
||||||
end Expand_SPARK_N_Simple_Return_Statement;
|
|
||||||
|
|
||||||
-----------------------------------------
|
|
||||||
-- Expand_SPARK_Simple_Function_Return --
|
|
||||||
-----------------------------------------
|
|
||||||
|
|
||||||
procedure Expand_SPARK_Simple_Function_Return (N : Node_Id) is
|
|
||||||
Scope_Id : constant Entity_Id :=
|
|
||||||
Return_Applies_To (Return_Statement_Entity (N));
|
|
||||||
-- The function we are returning from
|
|
||||||
|
|
||||||
R_Type : constant Entity_Id := Etype (Scope_Id);
|
|
||||||
-- The result type of the function
|
|
||||||
|
|
||||||
Exp : constant Node_Id := Expression (N);
|
|
||||||
pragma Assert (Present (Exp));
|
|
||||||
|
|
||||||
Exptyp : constant Entity_Id := Etype (Exp);
|
|
||||||
-- The type of the expression (not necessarily the same as R_Type)
|
|
||||||
|
|
||||||
begin
|
|
||||||
-- Check the result expression of a scalar function against the subtype
|
|
||||||
-- of the function by inserting a conversion. This conversion must
|
|
||||||
-- eventually be performed for other classes of types, but for now it's
|
|
||||||
-- only done for scalars.
|
|
||||||
-- ???
|
|
||||||
|
|
||||||
if Is_Scalar_Type (Exptyp) then
|
|
||||||
Rewrite (Exp, Convert_To (R_Type, Exp));
|
|
||||||
|
|
||||||
-- The expression is resolved to ensure that the conversion gets
|
|
||||||
-- expanded to generate a possible constraint check.
|
|
||||||
|
|
||||||
Analyze_And_Resolve (Exp, R_Type);
|
|
||||||
end if;
|
|
||||||
end Expand_SPARK_Simple_Function_Return;
|
|
||||||
|
|
||||||
-------------------------------
|
-------------------------------
|
||||||
-- Expand_Potential_Renaming --
|
-- Expand_Potential_Renaming --
|
||||||
-------------------------------
|
-------------------------------
|
||||||
|
|
|
@ -1236,12 +1236,14 @@ package body Sem_Ch3 is
|
||||||
-- be updated when the full type declaration is seen. This only applies
|
-- be updated when the full type declaration is seen. This only applies
|
||||||
-- to incomplete types declared in some enclosing scope, not to limited
|
-- to incomplete types declared in some enclosing scope, not to limited
|
||||||
-- views from other packages.
|
-- views from other packages.
|
||||||
|
-- Prior to Ada 2012, access to functions can only have in_parameters.
|
||||||
|
|
||||||
if Present (Formals) then
|
if Present (Formals) then
|
||||||
Formal := First_Formal (Desig_Type);
|
Formal := First_Formal (Desig_Type);
|
||||||
while Present (Formal) loop
|
while Present (Formal) loop
|
||||||
if Ekind (Formal) /= E_In_Parameter
|
if Ekind (Formal) /= E_In_Parameter
|
||||||
and then Nkind (T_Def) = N_Access_Function_Definition
|
and then Nkind (T_Def) = N_Access_Function_Definition
|
||||||
|
and then Ada_Version < Ada_2012
|
||||||
then
|
then
|
||||||
Error_Msg_N ("functions can only have IN parameters", Formal);
|
Error_Msg_N ("functions can only have IN parameters", Formal);
|
||||||
end if;
|
end if;
|
||||||
|
@ -4050,6 +4052,13 @@ package body Sem_Ch3 is
|
||||||
-- type with constraints. In this case the entity has been introduced
|
-- type with constraints. In this case the entity has been introduced
|
||||||
-- in the private declaration.
|
-- in the private declaration.
|
||||||
|
|
||||||
|
-- Finally this happens in some complex cases when validity checks are
|
||||||
|
-- enabled, where the same subtype declaration may be analyzed twice.
|
||||||
|
-- This can happen if the subtype is created by the pre-analysis of
|
||||||
|
-- an attribute tht gives the range of a loop statement, and the loop
|
||||||
|
-- itself appears within an if_statement that will be rewritten during
|
||||||
|
-- expansion.
|
||||||
|
|
||||||
if Skip
|
if Skip
|
||||||
or else (Present (Etype (Id))
|
or else (Present (Etype (Id))
|
||||||
and then (Is_Private_Type (Etype (Id))
|
and then (Is_Private_Type (Etype (Id))
|
||||||
|
@ -4058,6 +4067,9 @@ package body Sem_Ch3 is
|
||||||
then
|
then
|
||||||
null;
|
null;
|
||||||
|
|
||||||
|
elsif Current_Entity (Id) = Id then
|
||||||
|
null;
|
||||||
|
|
||||||
else
|
else
|
||||||
Enter_Name (Id);
|
Enter_Name (Id);
|
||||||
end if;
|
end if;
|
||||||
|
@ -14804,7 +14816,8 @@ package body Sem_Ch3 is
|
||||||
-- extensions of tagged record types.
|
-- extensions of tagged record types.
|
||||||
|
|
||||||
if No (Extension) then
|
if No (Extension) then
|
||||||
Check_SPARK_Restriction ("derived type is not allowed", N);
|
Check_SPARK_Restriction
|
||||||
|
("derived type is not allowed", Original_Node (N));
|
||||||
end if;
|
end if;
|
||||||
end Derived_Type_Declaration;
|
end Derived_Type_Declaration;
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue