+2015-10-26 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_prag.adb (Add_Item_To_Name_Buffer): Update the comment on usage.
+ Add an output string for loop parameters.
+ (Analyze_Global_Items): Loop parameters are now a
+ valid global item. The share the legality checks of constants.
+ (Analyze_Input_Output): Loop parameters are now a valid dependency item.
+ (Find_Role): Loop parameters share the role of constants.
+
+2015-10-26 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_res.adb (Resolve_Generalized_Indexing): In ASIS mode,
+ preserve the Generalized_ indexing link if the context is not
+ a spec expression that will be analyzed anew.
+
+2015-10-26 Javier Miranda <miranda@adacore.com>
+
+ * exp_ch6.ads, exp_ch6.adb (Build_Procedure_Body_Form): Promote it to
+ library level (to invoke this routine from the semantic analyzer).
+ * sem_ch6.adb (Analyze_Subprogram_Body_Helper): When generating
+ C code, invoke Build_Procedure_Body_Form to transform a function
+ that returns a constrained array type into a procedure with an
+ out parameter that carries the return value.
+
+2015-10-26 Arnaud Charlet <charlet@adacore.com>
+
+ * a-reatim.ads: Add "Clock_Time with Synchronous" contract in package
+ Ada.Real_Time.
+ * a-taside.ads: Add "Tasking_State with Synchronous" contract in
+ package Ada.Task_Identification.
+ * sem_ch12.adb: minor typo in comment
+
2015-10-26 Hristian Kirtchev <kirtchev@adacore.com>
* contracts.adb (Analyze_Object_Contract): Set and restore
package Ada.Real_Time with
SPARK_Mode,
- Abstract_State => (Clock_Time with External => (Async_Readers,
+ Abstract_State => (Clock_Time with Synchronous,
+ External => (Async_Readers,
Async_Writers))
is
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
-- --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow --
package Ada.Task_Identification with
SPARK_Mode,
- Abstract_State => (Tasking_State with External => (Async_Readers,
+ Abstract_State => (Tasking_State with Synchronous,
+ External => (Async_Readers,
Async_Writers))
is
pragma Preelaborate;
return Extra_Formal;
end Build_In_Place_Formal;
+ -------------------------------
+ -- Build_Procedure_Body_Form --
+ -------------------------------
+
+ function Build_Procedure_Body_Form
+ (Func_Id : Entity_Id;
+ Func_Body : Node_Id) return Node_Id
+ is
+ Loc : constant Source_Ptr := Sloc (Func_Body);
+
+ Proc_Decl : constant Node_Id :=
+ Next (Unit_Declaration_Node (Func_Id));
+ -- It is assumed that the next node following the declaration of the
+ -- corresponding subprogram spec is the declaration of the procedure
+ -- form.
+
+ Proc_Id : constant Entity_Id := Defining_Entity (Proc_Decl);
+
+ procedure Replace_Returns (Param_Id : Entity_Id; Stmts : List_Id);
+ -- Replace each return statement found in the list Stmts with an
+ -- assignment of the return expression to parameter Param_Id.
+
+ ---------------------
+ -- Replace_Returns --
+ ---------------------
+
+ procedure Replace_Returns (Param_Id : Entity_Id; Stmts : List_Id) is
+ Stmt : Node_Id;
+
+ begin
+ Stmt := First (Stmts);
+ while Present (Stmt) loop
+ if Nkind (Stmt) = N_Block_Statement then
+ Replace_Returns (Param_Id, Statements (Stmt));
+
+ elsif Nkind (Stmt) = N_Case_Statement then
+ declare
+ Alt : Node_Id;
+ begin
+ Alt := First (Alternatives (Stmt));
+ while Present (Alt) loop
+ Replace_Returns (Param_Id, Statements (Alt));
+ Next (Alt);
+ end loop;
+ end;
+
+ elsif Nkind (Stmt) = N_If_Statement then
+ Replace_Returns (Param_Id, Then_Statements (Stmt));
+ Replace_Returns (Param_Id, Else_Statements (Stmt));
+
+ declare
+ Part : Node_Id;
+ begin
+ Part := First (Elsif_Parts (Stmt));
+ while Present (Part) loop
+ Replace_Returns (Part, Then_Statements (Part));
+ Next (Part);
+ end loop;
+ end;
+
+ elsif Nkind (Stmt) = N_Loop_Statement then
+ Replace_Returns (Param_Id, Statements (Stmt));
+
+ elsif Nkind (Stmt) = N_Simple_Return_Statement then
+
+ -- Generate:
+ -- Param := Expr;
+ -- return;
+
+ Rewrite (Stmt,
+ Make_Assignment_Statement (Sloc (Stmt),
+ Name => New_Occurrence_Of (Param_Id, Loc),
+ Expression => Relocate_Node (Expression (Stmt))));
+
+ Insert_After (Stmt, Make_Simple_Return_Statement (Loc));
+
+ -- Skip the added return
+
+ Next (Stmt);
+ end if;
+
+ Next (Stmt);
+ end loop;
+ end Replace_Returns;
+
+ -- Local variables
+
+ Stmts : List_Id;
+ New_Body : Node_Id;
+
+ -- Start of processing for Build_Procedure_Body_Form
+
+ begin
+ -- This routine replaces the original function body:
+
+ -- function F (...) return Array_Typ is
+ -- begin
+ -- ...
+ -- return Something;
+ -- end F;
+
+ -- with the following:
+
+ -- procedure P (..., Result : out Array_Typ) is
+ -- begin
+ -- ...
+ -- Result := Something;
+ -- end P;
+
+ Stmts :=
+ Statements (Handled_Statement_Sequence (Func_Body));
+ Replace_Returns (Last_Entity (Proc_Id), Stmts);
+
+ New_Body :=
+ Make_Subprogram_Body (Loc,
+ Specification =>
+ Copy_Subprogram_Spec (Specification (Proc_Decl)),
+ Declarations => Declarations (Func_Body),
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => Stmts));
+
+ return New_Body;
+ end Build_Procedure_Body_Form;
+
--------------------------------
-- Check_Overriding_Operation --
--------------------------------
-- returns, since they get eliminated anyway later on. Spec_Id denotes
-- the corresponding spec of the subprogram body.
- procedure Build_Procedure_Body_Form (Func_Id : Entity_Id);
- -- Create a procedure body which emulates the behavior of function
- -- Func_Id. This body replaces the original function body, which is
- -- not needed for the C program.
-
----------------
-- Add_Return --
----------------
end if;
end Add_Return;
- -------------------------------
- -- Build_Procedure_Body_Form --
- -------------------------------
-
- procedure Build_Procedure_Body_Form (Func_Id : Entity_Id) is
- Proc_Decl : constant Node_Id :=
- Next (Unit_Declaration_Node (Func_Id));
- -- It is assumed that the next node following the declaration of the
- -- corresponding subprogram spec is the declaration of the procedure
- -- form.
-
- Proc_Id : constant Entity_Id := Defining_Entity (Proc_Decl);
-
- procedure Replace_Returns (Param_Id : Entity_Id; Stmts : List_Id);
- -- Replace each return statement found in the list Stmts with an
- -- assignment of the return expression to parameter Param_Id.
-
- ---------------------
- -- Replace_Returns --
- ---------------------
-
- procedure Replace_Returns (Param_Id : Entity_Id; Stmts : List_Id) is
- Stmt : Node_Id;
-
- begin
- Stmt := First (Stmts);
- while Present (Stmt) loop
- if Nkind (Stmt) = N_Block_Statement then
- Replace_Returns (Param_Id, Statements (Stmt));
-
- elsif Nkind (Stmt) = N_Case_Statement then
- declare
- Alt : Node_Id;
- begin
- Alt := First (Alternatives (Stmt));
- while Present (Alt) loop
- Replace_Returns (Param_Id, Statements (Alt));
- Next (Alt);
- end loop;
- end;
-
- elsif Nkind (Stmt) = N_If_Statement then
- Replace_Returns (Param_Id, Then_Statements (Stmt));
- Replace_Returns (Param_Id, Else_Statements (Stmt));
-
- declare
- Part : Node_Id;
- begin
- Part := First (Elsif_Parts (Stmt));
- while Present (Part) loop
- Replace_Returns (Part, Then_Statements (Part));
- Next (Part);
- end loop;
- end;
-
- elsif Nkind (Stmt) = N_Loop_Statement then
- Replace_Returns (Param_Id, Statements (Stmt));
-
- elsif Nkind (Stmt) = N_Simple_Return_Statement then
-
- -- Generate:
- -- Param := Expr;
- -- return;
-
- Rewrite (Stmt,
- Make_Assignment_Statement (Sloc (Stmt),
- Name => New_Occurrence_Of (Param_Id, Loc),
- Expression => Relocate_Node (Expression (Stmt))));
-
- Insert_After (Stmt, Make_Simple_Return_Statement (Loc));
-
- -- Skip the added return
-
- Next (Stmt);
- end if;
-
- Next (Stmt);
- end loop;
- end Replace_Returns;
-
- -- Local variables
-
- Stmts : List_Id;
-
- -- Start of processing for Build_Procedure_Body_Form
-
- begin
- -- This routine replaces the original function body:
-
- -- function F (...) return Array_Typ is
- -- begin
- -- ...
- -- return Something;
- -- end F;
-
- -- with the following:
-
- -- procedure P (..., Result : out Array_Typ) is
- -- begin
- -- ...
- -- Result := Something;
- -- end P;
-
- Stmts := Statements (HSS);
- Replace_Returns (Last_Entity (Proc_Id), Stmts);
-
- Replace (N,
- Make_Subprogram_Body (Loc,
- Specification =>
- Copy_Subprogram_Spec (Specification (Proc_Decl)),
- Declarations => Declarations (N),
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => Stmts)));
-
- Analyze (N);
- end Build_Procedure_Body_Form;
-
- -- Local varaibles
+ -- Local variables
Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
Unest_Bodies.Append ((Spec_Id, N));
end if;
- -- When generating C code, transform a function that returns a
- -- constrained array type into a procedure with an out parameter
- -- that carries the return value.
-
- if Modify_Tree_For_C
- and then Ekind (Spec_Id) = E_Function
- and then Rewritten_For_C (Spec_Id)
- then
- Build_Procedure_Body_Form (Spec_Id);
- end if;
-
Ghost_Mode := Save_Ghost_Mode;
end Expand_N_Subprogram_Body;
-- function Func, and returns its Entity_Id. It is a bug if not found; the
-- caller should ensure this is called only when the extra formal exists.
+ function Build_Procedure_Body_Form
+ (Func_Id : Entity_Id; Func_Body : Node_Id) return Node_Id;
+ -- Create a procedure body which emulates the behavior of function Func_Id.
+ -- Func_Body is the root of the body of the function before its analysis.
+ -- The returned node is the root of the procedure body which will replace
+ -- the original function body, which is not needed for the C program.
+
procedure Initialize;
-- Initialize internal tables
begin
Check_SPARK_05_Restriction ("generic is not allowed", N);
- -- Very first thing: check for Text_IO sp[ecial unit in case we are
+ -- Very first thing: check for Text_IO special unit in case we are
-- instantiating one of the children of [[Wide_]Wide_]Text_IO.
Check_Text_IO_Special_Unit (Name (N));
-- Local variables
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Cloned_Body_For_C : Node_Id := Empty;
-- Start of processing for Analyze_Subprogram_Body_Helper
return;
end if;
+ -- If we are generating C and this is a function returning a constrained
+ -- array type for which we must create a procedure with an extra out
+ -- parameter then clone the body before it is analyzed. Needed to ensure
+ -- that the body of the built procedure does not have any reference to
+ -- the body of the function.
+
+ if Expander_Active
+ and then Modify_Tree_For_C
+ and then Present (Spec_Id)
+ and then Ekind (Spec_Id) = E_Function
+ and then Rewritten_For_C (Spec_Id)
+ then
+ Cloned_Body_For_C := Copy_Separate_Tree (N);
+ end if;
+
-- Handle frontend inlining
-- Note: Normally we don't do any inlining if expansion is off, since
end if;
end;
+ -- When generating C code, transform a function that returns a
+ -- constrained array type into a procedure with an out parameter
+ -- that carries the return value.
+
+ if Present (Cloned_Body_For_C) then
+ Replace (N,
+ Build_Procedure_Body_Form (Spec_Id, Cloned_Body_For_C));
+ Analyze (N);
+ end if;
+
Ghost_Mode := Save_Ghost_Mode;
end Analyze_Subprogram_Body_Helper;
-- E_Generic_Out_Parameter - "generic parameter"
-- E_In_Parameter - "parameter"
-- E_In_Out_Parameter - "parameter"
+ -- E_Loop_Parameter - "loop parameter"
-- E_Out_Parameter - "parameter"
-- E_Protected_Type - "current instance of protected type"
-- E_Task_Type - "current instance of task type"
elsif Is_Formal (Item_Id) then
Add_Str_To_Name_Buffer ("parameter");
+ elsif Ekind (Item_Id) = E_Loop_Parameter then
+ Add_Str_To_Name_Buffer ("loop parameter");
+
elsif Ekind (Item_Id) = E_Protected_Type then
Add_Str_To_Name_Buffer ("current instance of protected type");
Item_Id := Entity_Of (Item);
if Present (Item_Id) then
- if Ekind_In (Item_Id, E_Abstract_State,
- E_Constant,
+
+ -- Constants
+
+ if Ekind_In (Item_Id, E_Constant,
E_Discriminant,
- E_Generic_In_Out_Parameter,
- E_Generic_In_Parameter,
- E_In_Parameter,
- E_In_Out_Parameter,
- E_Out_Parameter,
- E_Protected_Type,
- E_Task_Type,
- E_Variable)
+ E_Loop_Parameter)
+ or else
+
+ -- Current instances of concurrent types
+
+ Ekind_In (Item_Id, E_Protected_Type, E_Task_Type)
+ or else
+
+ -- Formal parameters
+
+ Ekind_In (Item_Id, E_Generic_In_Out_Parameter,
+ E_Generic_In_Parameter,
+ E_In_Parameter,
+ E_In_Out_Parameter,
+ E_Out_Parameter)
+ or else
+
+ -- States, variables
+
+ Ekind_In (Item_Id, E_Abstract_State, E_Variable)
then
-- The item denotes a concurrent type, but it is not the
-- current instance of an enclosing concurrent type.
Item_Is_Input := False;
Item_Is_Output := False;
- -- Abstract state cases
+ -- Abstract states
if Ekind (Item_Id) = E_Abstract_State then
Item_Is_Output := True;
end if;
- -- Constant case
-
- elsif Ekind (Item_Id) = E_Constant then
- Item_Is_Input := True;
-
- elsif Ekind (Item_Id) = E_Discriminant then
- Item_Is_Input := True;
-
- -- Generic parameter cases
+ -- Constants
- elsif Ekind (Item_Id) = E_Generic_In_Parameter then
+ elsif Ekind_In (Item_Id, E_Constant,
+ E_Discriminant,
+ E_Loop_Parameter)
+ then
Item_Is_Input := True;
- elsif Ekind (Item_Id) = E_Generic_In_Out_Parameter then
- Item_Is_Input := True;
- Item_Is_Output := True;
-
- -- Parameter cases
+ -- Parameters
- elsif Ekind (Item_Id) = E_In_Parameter then
+ elsif Ekind_In (Item_Id, E_Generic_In_Parameter,
+ E_In_Parameter)
+ then
Item_Is_Input := True;
- elsif Ekind (Item_Id) = E_In_Out_Parameter then
+ elsif Ekind_In (Item_Id, E_Generic_In_Out_Parameter,
+ E_In_Out_Parameter)
+ then
Item_Is_Input := True;
Item_Is_Output := True;
null;
-- The only legal references are those to abstract states,
- -- discriminants and objects (SPARK RM 6.1.4(4)).
+ -- objects and various kinds of constants (SPARK RM 6.1.4(4)).
elsif not Ekind_In (Item_Id, E_Abstract_State,
E_Constant,
E_Discriminant,
+ E_Loop_Parameter,
E_Variable)
then
SPARK_Msg_N
return;
end if;
+ -- Loop parameter related checks
+
+ elsif Ekind (Item_Id) = E_Loop_Parameter then
+
+ -- A loop parameter is a read-only item, therefore it cannot
+ -- act as an output.
+
+ if Nam_In (Global_Mode, Name_In_Out, Name_Output) then
+ SPARK_Msg_NE
+ ("loop parameter & cannot act as output",
+ Item, Item_Id);
+ return;
+ end if;
+
-- Variable related checks. These are only relevant when
-- SPARK_Mode is on as they are not standard Ada legality
-- rules.
Indexes := Parameter_Associations (Call);
Pref := Remove_Head (Indexes);
Set_Expressions (N, Indexes);
- Set_Generalized_Indexing (N, Empty);
+
+ -- If expression is to be reanalyzed, reset Generalized_Indexing
+ -- to recreate call node, as is the case when the expression is
+ -- part of an expression function.
+
+ if In_Spec_Expression then
+ Set_Generalized_Indexing (N, Empty);
+ end if;
+
Set_Prefix (N, Pref);
end if;