===================================================================
@@ -6732,7 +6732,7 @@
-- PROPERTY_LIST ::= PROPERTY {, PROPERTY}
-- PROPERTY ::= SIMPLE_PROPERTY
- -- | NAME_VALUE_PROPERTY
+ -- | NAME_VALUE_PROPERTY
-- SIMPLE_PROPERTY ::= IDENTIFIER
-- NAME_VALUE_PROPERTY ::= IDENTIFIER => EXPRESSION
-- STATE_NAME ::= DEFINING_IDENTIFIER
@@ -8872,6 +8872,706 @@
Debug_Pragmas_Disabled :=
Chars (Get_Pragma_Arg (Arg1)) = Name_Disable;
+ -------------
+ -- Depends --
+ -------------
+
+ -- pragma Depends (DEPENDENCY_RELATION);
+
+ -- DEPENDENCY_RELATION ::= null
+ -- | DEPENDENCY_CLAUSE {, DEPENDENCY_CLAUSE}
+ -- DEPENDENCY_CLAUSE ::= OUTPUT_LIST =>[+] INPUT_LIST
+ -- OUTPUT_LIST ::= null
+ -- | OUTPUT
+ -- | (OUTPUT {, OUTPUT})
+ -- INPUT_LIST ::= null
+ -- | INPUT
+ -- | (INPUT {, INPUT})
+ -- OUTPUT ::= NAME | FUNCTION_RESULT
+ -- INPUT ::= NAME
+
+ -- where FUNCTION_RESULT is a function Result attribute_reference
+
+ when Pragma_Depends => Depends : declare
+ Subp_Decl : Node_Id;
+ Subp_Id : Entity_Id;
+
+ All_Inputs_Seen : Elist_Id := No_Elist;
+ -- A list containing the entities of all the inputs processed so
+ -- far. This Elist is populated with unique entities because the
+ -- same input may appear in multiple input lists.
+
+ Outputs_Seen : Elist_Id := No_Elist;
+ -- A list containing the entities of all the outputs processed so
+ -- far. The elements of this list may come from different output
+ -- lists.
+
+ Null_Output_Seen : Boolean := False;
+ -- A flag used to track the legality of a null output
+
+ procedure Analyze_Dependency_Clause
+ (Clause : Node_Id;
+ Is_Last : Boolean);
+ -- Verify the legality of a single dependency clause. Flag Is_Last
+ -- denotes whether Clause is the last clause in the relation.
+
+ function Entity_Of (N : Node_Id) return Entity_Id;
+ -- Return the entity of N or Empty. If N is a renaming, find the
+ -- entity of the root renamed object.
+
+ procedure Normalize_Clause (Clause : Node_Id);
+ -- Remove a self-dependency "+" from the input list of a clause.
+ -- Depending on the contents of the relation, either split the
+ -- the clause into multiple smaller clauses or perform the
+ -- normalization in place.
+
+ -------------------------------
+ -- Analyze_Dependency_Clause --
+ -------------------------------
+
+ procedure Analyze_Dependency_Clause
+ (Clause : Node_Id;
+ Is_Last : Boolean)
+ is
+ procedure Analyze_Input_List (Inputs : Node_Id);
+ -- Verify the legality of a single input list
+
+ procedure Analyze_Input_Output
+ (Item : Node_Id;
+ Is_Input : Boolean;
+ Top_Level : Boolean;
+ Seen : in out Elist_Id;
+ Null_Seen : in out Boolean);
+ -- Verify the legality of a single input or output item. Flag
+ -- Is_Input should be set whenever Item is an input, False when
+ -- it denotes an output. Flag Top_Level should be set whenever
+ -- Item appears immediately within an input or output list.
+ -- Seen is a collection of all abstract states, variables and
+ -- formals processed so far. Flag Null_Seen denotes whether a
+ -- null input or output has been encountered.
+
+ ------------------------
+ -- Analyze_Input_List --
+ ------------------------
+
+ procedure Analyze_Input_List (Inputs : Node_Id) is
+ Inputs_Seen : Elist_Id := No_Elist;
+ -- A list containing the entities of all inputs that appear
+ -- in the current input list.
+
+ Null_Input_Seen : Boolean := False;
+ -- A flag used to track the legality of a null input
+
+ Input : Node_Id;
+
+ begin
+ -- Multiple inputs appear as an aggregate
+
+ if Nkind (Inputs) = N_Aggregate then
+ if Present (Component_Associations (Inputs)) then
+ Error_Msg_N
+ ("nested dependency relations not allowed", Inputs);
+
+ elsif Present (Expressions (Inputs)) then
+ Input := First (Expressions (Inputs));
+ while Present (Input) loop
+ Analyze_Input_Output
+ (Item => Input,
+ Is_Input => True,
+ Top_Level => False,
+ Seen => Inputs_Seen,
+ Null_Seen => Null_Input_Seen);
+
+ Next (Input);
+ end loop;
+
+ else
+ Error_Msg_N
+ ("malformed input dependency list", Inputs);
+ end if;
+
+ -- Process a solitary input
+
+ else
+ Analyze_Input_Output
+ (Item => Inputs,
+ Is_Input => True,
+ Top_Level => False,
+ Seen => Inputs_Seen,
+ Null_Seen => Null_Input_Seen);
+ end if;
+ end Analyze_Input_List;
+
+ --------------------------
+ -- Analyze_Input_Output --
+ --------------------------
+
+ procedure Analyze_Input_Output
+ (Item : Node_Id;
+ Is_Input : Boolean;
+ Top_Level : Boolean;
+ Seen : in out Elist_Id;
+ Null_Seen : in out Boolean)
+ is
+ Is_Output : constant Boolean := not Is_Input;
+ Item_Id : Entity_Id;
+ Grouped : Node_Id;
+
+ begin
+ -- Multiple input or output items appear as an aggregate
+
+ if Nkind (Item) = N_Aggregate then
+ if not Top_Level then
+ Error_Msg_N
+ ("nested grouping of items not allowed", Item);
+
+ elsif Present (Component_Associations (Item)) then
+ Error_Msg_N
+ ("nested dependency relations not allowed", Item);
+
+ -- Recursively analyze the grouped items
+
+ elsif Present (Expressions (Item)) then
+ Grouped := First (Expressions (Item));
+ while Present (Grouped) loop
+ Analyze_Input_Output
+ (Item => Grouped,
+ Is_Input => Is_Input,
+ Top_Level => False,
+ Seen => Seen,
+ Null_Seen => Null_Seen);
+
+ Next (Grouped);
+ end loop;
+
+ else
+ Error_Msg_N ("malformed dependency list", Item);
+ end if;
+
+ -- Process Function'Result in the context of a dependency
+ -- clause.
+
+ elsif Nkind (Item) = N_Attribute_Reference
+ and then Attribute_Name (Item) = Name_Result
+ then
+ -- It is sufficent to analyze the prefix of 'Result in
+ -- order to establish legality of the attribute.
+
+ Analyze (Prefix (Item));
+
+ -- The prefix of 'Result must denote the function for
+ -- which aspect/pragma Depends applies.
+
+ if not Is_Entity_Name (Prefix (Item))
+ or else Ekind (Subp_Id) /= E_Function
+ or else Entity (Prefix (Item)) /= Subp_Id
+ then
+ Error_Msg_Name_1 := Name_Result;
+ Error_Msg_N
+ ("prefix of attribute % must denote the enclosing " &
+ "function", Item);
+
+ -- Function'Result is allowed to appear on the output
+ -- side of a dependency clause.
+
+ elsif Is_Input then
+ Error_Msg_N
+ ("function result cannot act as input", Item);
+ end if;
+
+ -- Detect multiple uses of null in a single dependency list
+ -- or throughout the whole relation. Verify the placement of
+ -- a null output list relative to the other clauses.
+
+ elsif Nkind (Item) = N_Null then
+ if Null_Seen then
+ Error_Msg_N
+ ("multiple null dependency relations not allowed",
+ Item);
+ else
+ Null_Seen := True;
+
+ if Is_Output and then not Is_Last then
+ Error_Msg_N
+ ("null output list must be the last clause in " &
+ "a dependency relation", Item);
+ end if;
+ end if;
+
+ -- Default case
+
+ else
+ Analyze (Item);
+
+ if Is_Entity_Name (Item) then
+ Item_Id := Entity_Of (Item);
+
+ if Present (Item_Id)
+ and then Ekind_In (Item_Id, E_Abstract_State,
+ E_In_Parameter,
+ E_In_Out_Parameter,
+ E_Out_Parameter,
+ E_Variable)
+ then
+ -- Detect multiple uses of the same state, variable
+ -- or formal parameter. If this is not the case,
+ -- add the item to the list of processed relations.
+
+ if Contains (Seen, Item_Id) then
+ Error_Msg_N ("duplicate use of item", Item);
+ else
+ if No (Seen) then
+ Seen := New_Elmt_List;
+ end if;
+
+ Append_Elmt (Item_Id, Seen);
+ end if;
+
+ -- Detect an illegal use of an input related to a
+ -- null output. Such input items cannot appear in
+ -- other input lists.
+
+ if Null_Output_Seen
+ and then Contains (All_Inputs_Seen, Item_Id)
+ then
+ Error_Msg_N
+ ("input of a null output list appears in " &
+ "multiple input lists", Item);
+ else
+ if No (All_Inputs_Seen) then
+ All_Inputs_Seen := New_Elmt_List;
+ end if;
+
+ Append_Unique_Elmt (Item_Id, All_Inputs_Seen);
+ end if;
+
+ -- All other input/output items are illegal
+
+ else
+ Error_Msg_N
+ ("item must denote variable, state or formal " &
+ "parameter", Item);
+ end if;
+
+ -- All other input/output items are illegal
+
+ else
+ Error_Msg_N
+ ("item must denote variable, state or formal " &
+ "parameter", Item);
+ end if;
+ end if;
+ end Analyze_Input_Output;
+
+ -- Local variables
+
+ Inputs : Node_Id;
+ Output : Node_Id;
+
+ -- Start of processing for Analyze_Dependency_Clause
+
+ begin
+ -- Process the output_list of a dependency_clause
+
+ Output := First (Choices (Clause));
+ while Present (Output) loop
+ Analyze_Input_Output
+ (Item => Output,
+ Is_Input => False,
+ Top_Level => True,
+ Seen => Outputs_Seen,
+ Null_Seen => Null_Output_Seen);
+
+ Next (Output);
+ end loop;
+
+ -- Process the input_list of a dependency_clause
+
+ Inputs := Expression (Clause);
+
+ -- An input list with a self-dependency appears as operator "+"
+ -- where the actuals inputs are the right operand.
+
+ if Nkind (Inputs) = N_Op_Plus then
+ Inputs := Right_Opnd (Inputs);
+ end if;
+
+ Analyze_Input_List (Inputs);
+ end Analyze_Dependency_Clause;
+
+ ---------------
+ -- Entity_Of --
+ ---------------
+
+ function Entity_Of (N : Node_Id) return Entity_Id is
+ Id : Entity_Id := Entity (N);
+
+ begin
+ -- Follow a possible chain of renamings to reach the root
+ -- renamed object.
+
+ while Present (Renamed_Object (Id)) loop
+ if Is_Entity_Name (Renamed_Object (Id)) then
+ Id := Entity (Renamed_Object (Id));
+
+ -- The root of the renaming is not an entire object or
+ -- variable, return Empty.
+
+ else
+ Id := Empty;
+ exit;
+ end if;
+ end loop;
+
+ return Id;
+ end Entity_Of;
+
+ ----------------------
+ -- Normalize_Clause --
+ ----------------------
+
+ procedure Normalize_Clause (Clause : Node_Id) is
+ procedure Create_Or_Modify_Clause
+ (Output : Node_Id;
+ Outputs : Node_Id;
+ Inputs : Node_Id;
+ After : Node_Id;
+ In_Place : Boolean;
+ Multiple : Boolean);
+ -- Create a brand new clause to represent the self-reference
+ -- or modify the input and/or output lists of an existing
+ -- clause. Output denotes a self-referencial output. Outputs
+ -- is the output list of a clause. Inputs is the input list
+ -- of a clause. After denotes the clause after which the new
+ -- clause is to be inserted. Flag In_Place should be set when
+ -- normalizing the last output of an output list. Flag Multiple
+ -- should be set when Output comes from a list with multiple
+ -- items.
+
+ -----------------------------
+ -- Create_Or_Modify_Clause --
+ -----------------------------
+
+ procedure Create_Or_Modify_Clause
+ (Output : Node_Id;
+ Outputs : Node_Id;
+ Inputs : Node_Id;
+ After : Node_Id;
+ In_Place : Boolean;
+ Multiple : Boolean)
+ is
+ procedure Propagate_Output
+ (Output : Node_Id;
+ Inputs : Node_Id);
+ -- Handle the various cases of output propagation to the
+ -- input list. Output denotes a self-referencial output
+ -- item. Inputs is the input list of a clause.
+
+ ----------------------
+ -- Propagate_Output --
+ ----------------------
+
+ procedure Propagate_Output
+ (Output : Node_Id;
+ Inputs : Node_Id)
+ is
+ function Contains
+ (List : List_Id;
+ Id : Entity_Id) return Boolean;
+ -- Determine whether List contains element Id
+
+ --------------
+ -- Contains --
+ --------------
+
+ function Contains
+ (List : List_Id;
+ Id : Entity_Id) return Boolean
+ is
+ Elmt : Node_Id;
+
+ begin
+ Elmt := First (List);
+ while Present (Elmt) loop
+ if Entity_Of (Elmt) = Id then
+ return True;
+ end if;
+
+ Next (Elmt);
+ end loop;
+
+ return False;
+ end Contains;
+
+ -- Local variables
+
+ Grouped : List_Id;
+
+ -- Start of processing for Propagate_Output
+
+ begin
+ -- The clause is of the form:
+
+ -- (Output =>+ null)
+
+ -- Remove the null input and replace it with a copy of
+ -- the output:
+
+ -- (Output => Output)
+
+ if Nkind (Inputs) = N_Null then
+ Rewrite (Inputs, New_Copy_Tree (Output));
+
+ -- The clause is of the form:
+
+ -- (Output =>+ (Input1, ..., InputN))
+
+ -- Determine whether the output is not already mentioned
+ -- in the input list and if not, add it to the list of
+ -- inputs:
+
+ -- (Output => (Output, Input1, ..., InputN))
+
+ elsif Nkind (Inputs) = N_Aggregate then
+ Grouped := Expressions (Inputs);
+
+ if not Contains (Grouped, Entity_Of (Output)) then
+ Prepend_To (Grouped, New_Copy_Tree (Output));
+ end if;
+
+ -- The clause is of the form:
+
+ -- (Output =>+ Input)
+
+ -- If the input does not mention the output, group the
+ -- two together:
+
+ -- (Output => (Output, Input))
+
+ elsif Entity_Of (Output) /= Entity_Of (Inputs) then
+ Rewrite (Inputs,
+ Make_Aggregate (Loc,
+ Expressions => New_List (
+ New_Copy_Tree (Output),
+ New_Copy_Tree (Inputs))));
+ end if;
+ end Propagate_Output;
+
+ -- Local variables
+
+ Loc : constant Source_Ptr := Sloc (Output);
+ Clause : Node_Id;
+
+ -- Start of processing for Create_Or_Modify_Clause
+
+ begin
+ -- A function result cannot depend on itself because it
+ -- cannot appear in the input list of a relation.
+
+ if Nkind (Output) = N_Attribute_Reference
+ and then Attribute_Name (Output) = Name_Result
+ then
+ Error_Msg_N
+ ("function result cannot depend on itself", Output);
+ return;
+
+ -- A null output depending on itself does not require any
+ -- normalization.
+
+ elsif Nkind (Output) = N_Null then
+ return;
+ end if;
+
+ -- When performing the transformation in place, simply add
+ -- the output to the list of inputs (if not already there).
+ -- This case arises when dealing with the last output of an
+ -- output list - we perform the normalization in place to
+ -- avoid generating a malformed tree.
+
+ if In_Place then
+ Propagate_Output (Output, Inputs);
+
+ -- A list with multiple outputs is slowly trimmed until
+ -- only one element remains. When this happens, replace
+ -- the aggregate with the element itself.
+
+ if Multiple then
+ Remove (Output);
+ Rewrite (Outputs, Output);
+ end if;
+
+ -- Default case
+
+ else
+ -- Unchain the output from its output list as it will
+ -- appear in a new clause. Note that we cannot simply
+ -- rewrite the output as null because this will violate
+ -- the semantics of aspect/pragma Depends.
+
+ Remove (Output);
+
+ -- Create a new clause of the form:
+
+ -- (Output => Inputs)
+
+ Clause :=
+ Make_Component_Association (Loc,
+ Choices => New_List (Output),
+ Expression => New_Copy_Tree (Inputs));
+
+ -- The new clause contains replicated content that has
+ -- already been analyzed. There is not need to reanalyze
+ -- it or renormalize it again.
+
+ Set_Analyzed (Clause);
+
+ Propagate_Output
+ (Output => First (Choices (Clause)),
+ Inputs => Expression (Clause));
+
+ Insert_After (After, Clause);
+ end if;
+ end Create_Or_Modify_Clause;
+
+ -- Local variables
+
+ Outputs : constant Node_Id := First (Choices (Clause));
+ Inputs : Node_Id;
+ Last_Output : Node_Id;
+ Next_Output : Node_Id;
+ Output : Node_Id;
+
+ -- Start of processing for Normalize_Clause
+
+ begin
+ -- A self-dependency appears as operator "+". Remove the "+"
+ -- from the tree by moving the real inputs to their proper
+ -- place.
+
+ if Nkind (Expression (Clause)) = N_Op_Plus then
+ Rewrite
+ (Expression (Clause), Right_Opnd (Expression (Clause)));
+ Inputs := Expression (Clause);
+
+ -- Multiple outputs appear as an aggregate
+
+ if Nkind (Outputs) = N_Aggregate then
+ Last_Output := Last (Expressions (Outputs));
+
+ Output := First (Expressions (Outputs));
+ while Present (Output) loop
+
+ -- Normalization may remove an output from its list,
+ -- preserve the subsequent output now.
+
+ Next_Output := Next (Output);
+
+ Create_Or_Modify_Clause
+ (Output => Output,
+ Outputs => Outputs,
+ Inputs => Inputs,
+ After => Clause,
+ In_Place => Output = Last_Output,
+ Multiple => True);
+
+ Output := Next_Output;
+ end loop;
+
+ -- Solitary output
+
+ else
+ Create_Or_Modify_Clause
+ (Output => Outputs,
+ Outputs => Empty,
+ Inputs => Inputs,
+ After => Empty,
+ In_Place => True,
+ Multiple => False);
+ end if;
+ end if;
+ end Normalize_Clause;
+
+ -- Local variables
+
+ Clause : Node_Id;
+ Errors : Nat;
+ Last_Clause : Node_Id;
+
+ -- Start of processing for Depends
+
+ begin
+ GNAT_Pragma;
+ S14_Pragma;
+ Check_Arg_Count (1);
+
+ -- Ensure the proper placement of the pragma. Depends must be
+ -- associated with a subprogram declaration.
+
+ Subp_Decl := Parent (Corresponding_Aspect (N));
+
+ if Nkind (Subp_Decl) /= N_Subprogram_Declaration then
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ Subp_Id := Defining_Unit_Name (Specification (Subp_Decl));
+ Clause := Expression (Arg1);
+
+ -- There is nothing to be done for a null dependency relation
+
+ if Nkind (Clause) = N_Null then
+ null;
+
+ -- Dependency clauses appear as component associations of an
+ -- aggregate.
+
+ elsif Nkind (Clause) = N_Aggregate
+ and then Present (Component_Associations (Clause))
+ then
+ Last_Clause := Last (Component_Associations (Clause));
+
+ -- Ensure that the formal parameters are visible when analyzing
+ -- all clauses. This falls out of the general rule of aspects
+ -- pertaining to subprogram declarations.
+
+ Push_Scope (Subp_Id);
+ Install_Formals (Subp_Id);
+
+ Clause := First (Component_Associations (Clause));
+ while Present (Clause) loop
+ Errors := Serious_Errors_Detected;
+
+ -- Normalization may create extra clauses that contain
+ -- replicated input and output names. There is no need
+ -- to reanalyze or renormalize these extra clauses.
+
+ if not Analyzed (Clause) then
+ Set_Analyzed (Clause);
+
+ Analyze_Dependency_Clause
+ (Clause => Clause,
+ Is_Last => Clause = Last_Clause);
+
+ -- Do not normalize an erroneous clause because the
+ -- inputs or outputs may denote illegal items.
+
+ if Errors = Serious_Errors_Detected then
+ Normalize_Clause (Clause);
+ end if;
+ end if;
+
+ Next (Clause);
+ end loop;
+
+ End_Scope;
+
+ -- The top level dependency relation is malformed
+
+ else
+ Error_Msg_N ("malformed dependency relation", Clause);
+ end if;
+ end Depends;
+
---------------------
-- Detect_Blocking --
---------------------
@@ -10064,13 +10764,13 @@
-- pragma Global (GLOBAL_SPECIFICATION)
- -- GLOBAL_SPECIFICATION ::= MODED_GLOBAL_LIST {, MODED_GLOBAL_LIST}
- -- | GLOBAL_LIST
- -- | null
+ -- GLOBAL_SPECIFICATION ::= null
+ -- | GLOBAL_LIST
+ -- | MODED_GLOBAL_LIST {, MODED_GLOBAL_LIST}
-- MODED_GLOBAL_LIST ::= MODE_SELECTOR => GLOBAL_LIST
-- MODE_SELECTOR ::= Input | Output | In_Out | Contract_In
-- GLOBAL_LIST ::= GLOBAL_ITEM
- -- | (GLOBAL_ITEM {, GLOBAL_ITEM})
+ -- | (GLOBAL_ITEM {, GLOBAL_ITEM})
-- GLOBAL_ITEM ::= NAME
when Pragma_Global => Global : declare
@@ -10127,37 +10827,8 @@
(Item : Node_Id;
Global_Mode : Name_Id)
is
- function Is_Duplicate_Item (Id : Entity_Id) return Boolean;
- -- Determine whether Id has already been processed
-
- -----------------------
- -- Is_Duplicate_Item --
- -----------------------
-
- function Is_Duplicate_Item (Id : Entity_Id) return Boolean is
- Item_Elmt : Elmt_Id;
-
- begin
- if Present (Seen) then
- Item_Elmt := First_Elmt (Seen);
- while Present (Item_Elmt) loop
- if Node (Item_Elmt) = Id then
- return True;
- end if;
-
- Next_Elmt (Item_Elmt);
- end loop;
- end if;
-
- return False;
- end Is_Duplicate_Item;
-
- -- Local declarations
-
Id : Entity_Id;
- -- Start of processing for Analyze_Global_Item
-
begin
-- Detect one of the following cases
@@ -10207,7 +10878,7 @@
-- The same entity might be referenced through various way.
-- Check the entity of the item rather than the item itself.
- if Is_Duplicate_Item (Id) then
+ if Contains (Seen, Id) then
Error_Msg_N ("duplicate global item", Item);
-- Add the entity of the current item to the list of
@@ -10421,7 +11092,7 @@
Analyze_Global_List (List);
- Pop_Scope;
+ End_Scope;
end if;
end Global;
@@ -16624,6 +17295,7 @@
Pragma_Debug_Policy => 0,
Pragma_Detect_Blocking => -1,
Pragma_Default_Storage_Pool => -1,
+ Pragma_Depends => -1,
Pragma_Disable_Atomic_Synchronization => -1,
Pragma_Discard_Names => 0,
Pragma_Dispatching_Domain => -1,
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- Copyright (C) 1992-2013, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -158,6 +158,28 @@
end loop;
end Append_Unique_Elmt;
+ --------------
+ -- Contains --
+ --------------
+
+ function Contains (List : Elist_Id; N : Node_Or_Entity_Id) return Boolean is
+ Elmt : Elmt_Id;
+
+ begin
+ if Present (List) then
+ Elmt := First_Elmt (List);
+ while Present (Elmt) loop
+ if Node (Elmt) = N then
+ return True;
+ end if;
+
+ Next_Elmt (Elmt);
+ end loop;
+ end if;
+
+ return False;
+ end Contains;
+
--------------------
-- Elists_Address --
--------------------
===================================================================
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
+-- Copyright (C) 1992-2013, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -153,6 +153,10 @@
-- affected, but the space used by the list element may be (but is not
-- required to be) freed for reuse in a subsequent Append_Elmt call.
+ function Contains (List : Elist_Id; N : Node_Or_Entity_Id) return Boolean;
+ -- Perform a sequential search to determine whether the given list contains
+ -- a node or an entity.
+
function No (List : Elist_Id) return Boolean;
pragma Inline (No);
-- Tests given Id for equality with No_Elist. This allows notations like
===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- Copyright (C) 2010-2013, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -259,6 +259,7 @@
Aspect_Default_Component_Value => Aspect_Default_Component_Value,
Aspect_Default_Iterator => Aspect_Default_Iterator,
Aspect_Default_Value => Aspect_Default_Value,
+ Aspect_Depends => Aspect_Depends,
Aspect_Dimension => Aspect_Dimension,
Aspect_Dimension_System => Aspect_Dimension_System,
Aspect_Discard_Names => Aspect_Discard_Names,
===================================================================
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
+-- Copyright (C) 2010-2013, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -88,6 +88,7 @@
Aspect_Default_Component_Value,
Aspect_Default_Iterator,
Aspect_Default_Value,
+ Aspect_Depends, -- GNAT
Aspect_Dimension, -- GNAT
Aspect_Dimension_System, -- GNAT
Aspect_Dispatching_Domain,
@@ -229,6 +230,7 @@
Aspect_Compiler_Unit => True,
Aspect_Contract_Case => True,
Aspect_Contract_Cases => True,
+ Aspect_Depends => True,
Aspect_Dimension => True,
Aspect_Dimension_System => True,
Aspect_Favor_Top_Level => True,
@@ -325,6 +327,7 @@
Aspect_Default_Component_Value => Expression,
Aspect_Default_Iterator => Name,
Aspect_Default_Value => Expression,
+ Aspect_Depends => Expression,
Aspect_Dimension => Expression,
Aspect_Dimension_System => Expression,
Aspect_Dispatching_Domain => Expression,
@@ -399,6 +402,7 @@
Aspect_Default_Iterator => Name_Default_Iterator,
Aspect_Default_Value => Name_Default_Value,
Aspect_Default_Component_Value => Name_Default_Component_Value,
+ Aspect_Depends => Name_Depends,
Aspect_Dimension => Name_Dimension,
Aspect_Dimension_System => Name_Dimension_System,
Aspect_Discard_Names => Name_Discard_Names,
===================================================================
@@ -1140,6 +1140,7 @@
Pragma_Controlled |
Pragma_Convention |
Pragma_Debug_Policy |
+ Pragma_Depends |
Pragma_Detect_Blocking |
Pragma_Default_Storage_Pool |
Pragma_Disable_Atomic_Synchronization |
===================================================================
@@ -1475,6 +1475,17 @@
Delay_Required := False;
+ when Aspect_Depends =>
+ Aitem :=
+ Make_Pragma (Loc,
+ Pragma_Identifier =>
+ Make_Identifier (Sloc (Id), Name_Depends),
+ Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))));
+
+ Delay_Required := False;
+
-- Aspect Global must be delayed because it can mention names
-- and benefit from the forward visibility rules applicable to
-- aspects of subprograms.
@@ -7265,6 +7276,7 @@
when Aspect_Abstract_State |
Aspect_Contract_Case |
Aspect_Contract_Cases |
+ Aspect_Depends |
Aspect_Dimension |
Aspect_Dimension_System |
Aspect_Implicit_Dereference |
===================================================================
@@ -485,6 +485,7 @@
-- pragma.
Name_Debug : constant Name_Id := N + $; -- GNAT
+ Name_Depends : 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 + $;
@@ -1774,6 +1775,7 @@
Pragma_CPP_Virtual,
Pragma_CPP_Vtable,
Pragma_Debug,
+ Pragma_Depends,
Pragma_Elaborate,
Pragma_Elaborate_All,
Pragma_Elaborate_Body,
This patch provides the initial implementation of aspect Depends. This construct is intended for formal verification proofs. The syntax of the aspect is as follows: DEPENDENCY_RELATION ::= null | DEPENDENCY_CLAUSE {, DEPENDENCY_CLAUSE} DEPENDENCY_CLAUSE ::= OUTPUT_LIST =>[+] INPUT_LIST OUTPUT_LIST ::= null | OUTPUT | (OUTPUT {, OUTPUT}) INPUT_LIST ::= null | INPUT | (INPUT {, INPUT}) OUTPUT ::= NAME | FUNCTION_RESULT INPUT ::= NAME where FUNCTION_RESULT is a function Result attribute_reference The semantics of the aspect are as follows: Every input and output of a dependency_relation of a Depends aspect of a subprogram denotes a state abstraction, an entire variable or a formal parameter of the subprogram. An input must have a mode of in or in out and an output must have an mode of in out or out. [Note: As a consequence an entity which is both an input and an output shall have a mode of in out.] For the purposes of determining the legality of a Result attribute_reference, a dependency_relation is considered to be a postcondition of the function to which the enclosing aspect_specification applies. There can be at most one output_list which is a null symbol and if it exists it must be the output_list of the last dependency_clause in the dependency_relation. An input which is in an input_list of a null output_list may not appear in another input_list of the same dependency_relation. The entity denoted by an output in an output_list shall not be denoted by any other output in that output_list or any other output_list. The entity denoted by an input in an input_list shall not be denoted by any other input in that input_list. Every output of the subprogram shall appear in exactly one output_list. Every input of the subprogram shall appear in at least one input_list. ------------ -- Source -- ------------ -- types.ads package Types is type Rec is record Comp : Natural; end record; type Arr is array (1 .. 5) of Rec; function Get_Comp (Obj : Rec) return Natural; end Types; -- types.adb package body Types is function Get_Comp (Obj : Rec) return Natural is begin return Obj.Comp; end Get_Comp; end Types; -- semantics.ads with Types; use Types; package Semantics with Abstract_State => State is Arr_Obj : Arr; Rec_Obj : Rec; -- Renaming chain of an object Ren_1 : Rec renames Rec_Obj; Ren_2 : Rec renames Ren_1; -- Renaming of a record component Ren_3 : Natural renames Rec_Obj.Comp; -- Renaming of an array element Ren_4 : Rec renames Arr_Obj (3); -- Renaming of a function call result Ren_5 : Natural renames Get_Comp (Rec_Obj); -- Legality rules -- 1. Every input and output of a dependency_relation of a Depends aspect -- of a subprogram denotes a state abstraction, an entire variable or a -- formal parameter of the subprogram. procedure OK_1a (Formal : Natural; Result : out Natural) with Depends => (Result => (State, -- abstract state Arr_Obj, -- object Rec_Obj, -- object Formal)); -- formal procedure OK_1b (Result : out Natural) with Depends => (Result => Ren_1); -- renaming of object procedure OK_1c (Result : out Natural) with Depends => (Result => Ren_2); -- renaming of renaming of object procedure Error_1 (Result : out Natural) with Depends => (Result => (Arr_Obj (3), -- element Rec_Obj.Comp, -- component Get_Comp (Rec_Obj), -- function call Ren_3, -- renaming of component Ren_4, -- renaming of element Ren_5, -- renaming of function call result 1234)); -- junk -- Legality rules -- 3. For the purposes of determining the legality of a Result -- attribute_reference, a dependency_relation is considered to -- be a postcondition of the function to which the enclosing -- aspect_specification applies. function OK_3 return Natural with Depends => (OK_3'Result => Rec_Obj); -- 'Result is an output function Error_3a (Result : out Natural) return Natural with Depends => (Result => Error_3a'Result); -- 'Result is an input function Error_3b (Formal : Natural) return Natural with Depends => (Get_Comp (Rec_Obj)'Result => Formal); -- 'Result must apply to the -- enclosing function -- Legality rules -- 4. There can be at most one output_list which is a null symbol and if it -- exists it must be the output_list of the last dependency_clause in the -- dependency_relation. procedure OK_4a (Formal : Natural; Result : out Natural) with Depends => (Result => Formal, null => Rec_Obj); -- null is last output_list function Error_4a (Formal : Natural) return Natural with Depends => (null => Arr_Obj, -- null is not the last output_list Error_4a'Result => Formal); -- Legality rules -- 4. An input which is in an input_list of a null output_list may not -- appear in another input_list of the same dependency_relation. procedure OK_4b (Formal : Natural; Result : out Natural) with Depends => (Result => Ren_1, null => Formal); procedure Error_4b (Formal : Natural; Result : out Natural) with Depends => (Result => Formal, null => Formal); -- Formal appears in both output_lists -- Legality rules -- 5. The entity denoted by an output in an output_list shall not -- be denoted by any other output in that output_list or any other -- output_list. procedure OK_5a (Result_1 : out Natural; Result_2 : out Natural) with Depends => ((Result_1, Result_2) => Ren_2); procedure OK_5b (Result_1 : out Natural; Result_2 : out Natural) with Depends => (Result_1 => Arr_Obj, Result_2 => Rec_Obj); procedure Error_5 (Result_1 : out Natural; Result_2 : out Natural) with Depends => ((Result_1, Result_2, Result_1) => Arr_Obj, -- Result_1 appears twice Result_2 => Ren_1); -- Result_2 is already in the first input_list -- Legality rules -- 6. The entity denoted by an input in an input_list shall not be denoted -- by any other input in that input_list. function OK_6 (Result : out Natural) return Natural with Depends => (Result => (Rec_Obj, Arr_Obj), OK_6'Result => Rec_Obj); procedure Error_6 (Result : out Natural) with Depends => (Result => (Rec_Obj, Ren_1, Ren_2)); -- All inputs are the same object -- Extra checks procedure Error_E1 (Formal : Natural; Result_1 : out Natural; Result_2 : out Natural; Result_3 : out Natural) with Depends => ((Result_1, (Result_2, Result_3)) => (Formal, (Arr_Obj, Rec_Obj))); -- Cannot have nested groupings such as (Result_2, Result_3) end Semantics; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c -gnat12 -gnatd.V semantics.ads semantics.ads:48:12: item must denote variale, state or formal parameter semantics.ads:49:19: item must denote variale, state or formal parameter semantics.ads:50:12: item must denote variale, state or formal parameter semantics.ads:51:12: item must denote variale, state or formal parameter semantics.ads:52:12: item must denote variale, state or formal parameter semantics.ads:53:12: item must denote variale, state or formal parameter semantics.ads:54:12: item must denote variale, state or formal parameter semantics.ads:68:28: function result cannot act as input semantics.ads:72:28: prefix of attribute "Result" must denote the enclosing function semantics.ads:87:10: null output list must be the last clause in a dependency relation semantics.ads:102:20: input of a null output list appears in multiple input lists semantics.ads:120:31: duplicate use of item semantics.ads:121:11: duplicate use of item semantics.ads:135:21: duplicate use of item semantics.ads:135:28: duplicate use of item semantics.ads:145:19: nested grouping of items not allowed semantics.ads:145:53: nested grouping of items not allowed Tested on x86_64-pc-linux-gnu, committed on trunk 2013-04-11 Hristian Kirtchev <kirtchev@adacore.com> * aspects.ads, aspects.adb: Add Aspect_Depends to all the relevant tables. * elists.ads, elists.adb (Contains): New routine. * par-prag.adb: Pragma Depends does not need any special treatment by the parser. * sem_ch13.adb (Analyze_Aspect_Specifications): Transform aspect Depends into a corresponding pragma. (Check_Aspect_At_Freeze_Point): Aspect Depends does not need inspection at its freeze point. * sem_prag.adb (Analyze_Pragma): Perform analysis and normalization of pragma Depends. Remove the use of function Is_Duplicate_Item. Use End_Scope to uninstalle the formal parameters of a subprogram. Add a value for pragma Depends in table Sig_Flags. (Is_Duplicate_Item): Removed. * snames.ads-tmpl: Add predefined name for Depends as well as a pragma identifier.