with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
with Ghost; use Ghost;
-with Gnatvsn; use Gnatvsn;
with Lib; use Lib;
with Lib.Writ; use Lib.Writ;
with Lib.Xref; use Lib.Xref;
Table_Increment => 100,
Table_Name => "Name_Externals");
- --------------------------------------------------------
- -- Handling of inherited classwide pre/postconditions --
- --------------------------------------------------------
-
- -- Following AI12-0113, the expression for a classwide condition is
- -- transformed for a subprogram that inherits it, by replacing calls
- -- to primitive operations of the original controlling type into the
- -- corresponding overriding operations of the derived type. The following
- -- hash table manages this mapping, and is expanded on demand whenever
- -- such inherited expression needs to be constructed.
-
- -- The mapping is also used to check whether an inherited operation has
- -- a condition that depends on overridden operations. For such an
- -- operation we must create a wrapper that is then treated as a normal
- -- overriding. In SPARK mode such operations are illegal.
-
- -- For a given root type there may be several type extensions with their
- -- own overriding operations, so at various times a given operation of
- -- the root will be mapped into different overridings. The root type is
- -- also mapped into the current type extension to indicate that its
- -- operations are mapped into the overriding operations of that current
- -- type extension.
-
- subtype Num_Primitives is Integer range 0 .. 510;
- function Entity_Hash (E : Entity_Id) return Num_Primitives;
-
- package Primitives_Mapping is new Gnat.HTable.Simple_Htable
- (Header_Num => Num_Primitives,
- Key => Entity_Id,
- Element => Entity_Id,
- No_element => Empty,
- Hash => Entity_Hash,
- Equal => "=");
+ --------------------------------------------------------
+ -- Handling of inherited classwide pre/postconditions --
+ --------------------------------------------------------
+
+ -- Following AI12-0113, the expression for a classwide condition is
+ -- transformed for a subprogram that inherits it, by replacing calls
+ -- to primitive operations of the original controlling type into the
+ -- corresponding overriding operations of the derived type. The following
+ -- hash table manages this mapping, and is expanded on demand whenever
+ -- such inherited expression needs to be constructed.
+
+ -- The mapping is also used to check whether an inherited operation has
+ -- a condition that depends on overridden operations. For such an
+ -- operation we must create a wrapper that is then treated as a normal
+ -- overriding. In SPARK mode such operations are illegal.
+
+ -- For a given root type there may be several type extensions with their
+ -- own overriding operations, so at various times a given operation of
+ -- the root will be mapped into different overridings. The root type is
+ -- also mapped into the current type extension to indicate that its
+ -- operations are mapped into the overriding operations of that current
+ -- type extension.
+
+ subtype Num_Primitives is Integer range 0 .. 510;
+ function Entity_Hash (E : Entity_Id) return Num_Primitives;
+
+ package Primitives_Mapping is new Gnat.HTable.Simple_Htable
+ (Header_Num => Num_Primitives,
+ Key => Entity_Id,
+ Element => Entity_Id,
+ No_element => Empty,
+ Hash => Entity_Hash,
+ Equal => "=");
-------------------------------------
-- Local Subprograms and Variables --
-- Query whether a particular item appears in a mixed list of nodes and
-- entities. It is assumed that all nodes in the list have entities.
- -- procedure Build_Classwide_Expression (Prag : Node_Id; Subp : Entity_Id);
- -- Build the expression for an inherited classwide condition. Prag is
- -- the pragma constructed from the corresponding aspect of the parent
- -- subprogram, and Subp is the overridding operation.
-
procedure Check_Postcondition_Use_In_Inlined_Subprogram
(Prag : Node_Id;
Spec_Id : Entity_Id);
-- pragma. Entity name for unit and its parents is taken from item in
-- previous with_clause that mentions the unit.
- Dummy : Integer := 0;
- pragma Volatile (Dummy);
- -- Dummy volatile integer used in bodies of ip/rv to prevent optimization
-
procedure Update_Primitives_Mapping
(Inher_Id : Entity_Id;
Subp_Id : Entity_Id);
-
- -- map primitive operations of the parent type to the corresponding
- -- operations of the descendant. note that the descendant type may
+ -- Map primitive operations of the parent type to the corresponding
+ -- operations of the descendant. Note that the descendant type may
-- not be frozen yet, so we cannot use the dispatch table directly.
+ Dummy : Integer := 0;
+ pragma Volatile (Dummy);
+ -- Dummy volatile integer used in bodies of ip/rv to prevent optimization
+
procedure ip;
pragma No_Inline (ip);
-- A dummy procedure called when pragma Inspection_Point is analyzed. This
Check_Valid_Configuration_Pragma;
Check_Arg_Count (0);
- -- Remove backward compatibility if Build_Type is FSF or GPL
- -- and generate a warning.
-
- declare
- Ignore : constant Boolean := Build_Type in FSF .. GPL;
- begin
- if Ignore then
- Error_Pragma ("pragma% is ignored, has no effect??");
- else
- No_Run_Time_Mode := True;
- Configurable_Run_Time_Mode := True;
+ No_Run_Time_Mode := True;
+ Configurable_Run_Time_Mode := True;
- -- Set Duration to 32 bits if word size is 32
+ -- Set Duration to 32 bits if word size is 32
- if Ttypes.System_Word_Size = 32 then
- Duration_32_Bits_On_Target := True;
- end if;
+ if Ttypes.System_Word_Size = 32 then
+ Duration_32_Bits_On_Target := True;
+ end if;
- -- Set appropriate restrictions
+ -- Set appropriate restrictions
- Set_Restriction (No_Finalization, N);
- Set_Restriction (No_Exception_Handlers, N);
- Set_Restriction (Max_Tasks, N, 0);
- Set_Restriction (No_Tasking, N);
- end if;
- end;
+ Set_Restriction (No_Finalization, N);
+ Set_Restriction (No_Exception_Handlers, N);
+ Set_Restriction (Max_Tasks, N, 0);
+ Set_Restriction (No_Tasking, N);
- -----------------------
- -- No_Tagged_Streams --
- -----------------------
+ -----------------------
+ -- No_Tagged_Streams --
+ -----------------------
- -- pragma No_Tagged_Streams;
- -- pragma No_Tagged_Streams ([Entity => ]tagged_type_local_NAME);
+ -- pragma No_Tagged_Streams;
+ -- pragma No_Tagged_Streams ([Entity => ]tagged_type_local_NAME);
when Pragma_No_Tagged_Streams => No_Tagged_Strms : declare
E : Entity_Id;
when Pragma_Universal_Data =>
GNAT_Pragma;
- Error_Pragma ("??pragma% ignored (applies only to AAMP)");
+
+ -- If this is a configuration pragma, then set the universal
+ -- addressing option, otherwise confirm that the pragma satisfies
+ -- the requirements of library unit pragma placement and leave it
+ -- to the GNAAMP back end to detect the pragma (avoids transitive
+ -- setting of the option due to withed units).
+
+ if Is_Configuration_Pragma then
+ Universal_Addressing_On_AAMP := True;
+ else
+ Check_Valid_Library_Unit_Pragma;
+ end if;
+
+ if not AAMP_On_Target then
+ Error_Pragma ("??pragma% ignored (applies only to AAMP)");
+ end if;
----------------
-- Unmodified --
return False;
end Appears_In;
+ --------------------------------
+ -- Build_Classwide_Expression --
+ --------------------------------
+
+ procedure Build_Classwide_Expression (Prag : Node_Id; Subp : Entity_Id) is
+ function Replace_Entity (N : Node_Id) return Traverse_Result;
+ -- Replace reference to formal of inherited operation or to primitive
+ -- operation of root type, with corresponding entity for derived type,
+ -- when constructing the classwide condition of an overridding
+ -- subprogram.
+
+ --------------------
+ -- Replace_Entity --
+ --------------------
+
+ function Replace_Entity (N : Node_Id) return Traverse_Result is
+ New_E : Entity_Id;
+
+ begin
+ if Nkind (N) = N_Identifier
+ and then Present (Entity (N))
+ and then
+ (Is_Formal (Entity (N)) or else Is_Subprogram (Entity (N)))
+ and then
+ (Nkind (Parent (N)) /= N_Attribute_Reference
+ or else Attribute_Name (Parent (N)) /= Name_Class)
+ then
+ -- The replacement does not apply to dispatching calls within the
+ -- condition, but only to calls whose static tag is that of the
+ -- parent type.
+
+ if Is_Subprogram (Entity (N))
+ and then Nkind (Parent (N)) = N_Function_Call
+ and then Present (Controlling_Argument (Parent (N)))
+ then
+ return OK;
+ end if;
+
+ -- Determine whether entity has a renaming
+
+ New_E := Primitives_Mapping.Get (Entity (N));
+
+ if Present (New_E) then
+ Rewrite (N, New_Occurrence_Of (New_E, Sloc (N)));
+ end if;
+
+ -- Check that there are no calls left to abstract operations if
+ -- the current subprogram is not abstract.
+
+ if Nkind (Parent (N)) = N_Function_Call
+ and then N = Name (Parent (N))
+ then
+ if not Is_Abstract_Subprogram (Subp)
+ and then Is_Abstract_Subprogram (Entity (N))
+ then
+ Error_Msg_Sloc := Sloc (Current_Scope);
+ Error_Msg_NE
+ ("cannot call abstract subprogram in inherited condition "
+ & "for&#", N, Current_Scope);
+
+ elsif SPARK_Mode = On
+ and then Warn_On_Suspicious_Contract
+ and then Present (Alias (Subp))
+ then
+ Error_Msg_NE
+ ("?inherited condition is modified, build a wrapper "
+ & "for&", Parent (Subp), Subp);
+ end if;
+ end if;
+
+ -- Update type of function call node, which should be the same as
+ -- the function's return type.
+
+ if Is_Subprogram (Entity (N))
+ and then Nkind (Parent (N)) = N_Function_Call
+ then
+ Set_Etype (Parent (N), Etype (Entity (N)));
+ end if;
+
+ -- The whole expression will be reanalyzed
+
+ elsif Nkind (N) in N_Has_Etype then
+ Set_Analyzed (N, False);
+ end if;
+
+ return OK;
+ end Replace_Entity;
+
+ procedure Replace_Condition_Entities is
+ new Traverse_Proc (Replace_Entity);
+
+ -- Start of processing for Build_Classwide_Expression
+
+ begin
+ Replace_Condition_Entities (Prag);
+ end Build_Classwide_Expression;
+
-----------------------------------
-- Build_Pragma_Check_Equivalent --
-----------------------------------
Inher_Id : Entity_Id := Empty;
Keep_Pragma_Id : Boolean := False) return Node_Id
is
-
function Suppress_Reference (N : Node_Id) return Traverse_Result;
-- Detect whether node N references a formal parameter subject to
-- pragma Unreferenced. If this is the case, set Comes_From_Source
if Is_Entity_Name (N) and then Present (Entity (N)) then
Formal := Entity (N);
- -- The formal parameter is subject to pragma Unreferenced.
- -- Prevent the generation of a reference by resetting the
- -- Comes_From_Source flag.
+ -- The formal parameter is subject to pragma Unreferenced. Prevent
+ -- the generation of references by resetting the Comes_From_Source
+ -- flag.
if Is_Formal (Formal)
and then Has_Pragma_Unreferenced (Formal)
end if;
end Check_Missing_Part_Of;
- --------------------------------
- -- Build_Classwide_Expression --
- --------------------------------
-
- procedure Build_Classwide_Expression (Prag : Node_Id; Subp : Entity_Id) is
- function Replace_Entity (N : Node_Id) return Traverse_Result;
- -- Replace reference to formal of inherited operation or to primitive
- -- operation of root type, with corresponding entity for derived type,
- -- when constructing the classwide condition of an overridding
- -- subprogram.
-
- --------------------
- -- Replace_Entity --
- --------------------
-
- function Replace_Entity (N : Node_Id) return Traverse_Result is
- New_E : Entity_Id;
-
- begin
- if Nkind (N) = N_Identifier
- and then Present (Entity (N))
- and then
- (Is_Formal (Entity (N)) or else Is_Subprogram (Entity (N)))
- and then
- (Nkind (Parent (N)) /= N_Attribute_Reference
- or else Attribute_Name (Parent (N)) /= Name_Class)
- then
- -- The replacement does not apply to dispatching calls within the
- -- condition, but only to calls whose static tag is that of the
- -- parent type.
-
- if Is_Subprogram (Entity (N))
- and then Nkind (Parent (N)) = N_Function_Call
- and then Present (Controlling_Argument (Parent (N)))
- then
- return OK;
- end if;
-
- -- Determine whether entity has a renaming
-
- New_E := Primitives_Mapping.Get (Entity (N));
-
- if Present (New_E) then
- Rewrite (N, New_Occurrence_Of (New_E, Sloc (N)));
- end if;
-
- -- Check that there are no calls left to abstract operations if
- -- the current subprogram is not abstract.
-
- if Nkind (Parent (N)) = N_Function_Call
- and then N = Name (Parent (N))
- then
- if not Is_Abstract_Subprogram (Subp)
- and then Is_Abstract_Subprogram (Entity (N))
- then
- Error_Msg_Sloc := Sloc (Current_Scope);
- Error_Msg_NE
- ("cannot call abstract subprogram in inherited condition "
- & "for&#", N, Current_Scope);
-
- elsif Present (Alias (Subp))
- and then Warn_On_Suspicious_Contract
- and then SPARK_Mode = On
- then
- Error_Msg_NE ("?inherited condition is modified, "
- & "build a wrapper for&", Parent (Subp), Subp);
- end if;
- end if;
-
- -- Update type of function call node, which should be the same as
- -- the function's return type.
-
- if Is_Subprogram (Entity (N))
- and then Nkind (Parent (N)) = N_Function_Call
- then
- Set_Etype (Parent (N), Etype (Entity (N)));
- end if;
-
- -- The whole expression will be reanalyzed
-
- elsif Nkind (N) in N_Has_Etype then
- Set_Analyzed (N, False);
- end if;
-
- return OK;
- end Replace_Entity;
-
- procedure Replace_Condition_Entities is
- new Traverse_Proc (Replace_Entity);
-
- begin
- Replace_Condition_Entities (Prag);
- end Build_Classwide_Expression;
-
---------------------------------------------------
-- Check_Postcondition_Use_In_Inlined_Subprogram --
---------------------------------------------------
end if;
end Duplication_Error;
+ -----------------
+ -- Entity_Hash --
+ -----------------
+
+ function Entity_Hash (E : Entity_Id) return Num_Primitives is
+ begin
+ return Num_Primitives (E mod 511);
+ end Entity_Hash;
+
--------------------------
-- Find_Related_Context --
--------------------------
return Result;
end Get_Base_Subprogram;
- -----------------
- -- Entity_Hash --
- -----------------
-
- function Entity_Hash (E : Entity_Id) return Num_Primitives is
- begin
- return Num_Primitives (E mod 511);
- end Entity_Hash;
-
-----------------------
-- Get_SPARK_Mode_Type --
-----------------------
Generate_Reference (Entity (With_Item), N, Set_Ref => False);
end Set_Elab_Unit_Name;
+ -------------------
+ -- Test_Case_Arg --
+ -------------------
+
+ function Test_Case_Arg
+ (Prag : Node_Id;
+ Arg_Nam : Name_Id;
+ From_Aspect : Boolean := False) return Node_Id
+ is
+ Aspect : constant Node_Id := Corresponding_Aspect (Prag);
+ Arg : Node_Id;
+ Args : Node_Id;
+
+ begin
+ pragma Assert (Nam_In (Arg_Nam, Name_Ensures,
+ Name_Mode,
+ Name_Name,
+ Name_Requires));
+
+ -- The caller requests the aspect argument
+
+ if From_Aspect then
+ if Present (Aspect)
+ and then Nkind (Expression (Aspect)) = N_Aggregate
+ then
+ Args := Expression (Aspect);
+
+ -- "Name" and "Mode" may appear without an identifier as a
+ -- positional association.
+
+ if Present (Expressions (Args)) then
+ Arg := First (Expressions (Args));
+
+ if Present (Arg) and then Arg_Nam = Name_Name then
+ return Arg;
+ end if;
+
+ -- Skip "Name"
+
+ Arg := Next (Arg);
+
+ if Present (Arg) and then Arg_Nam = Name_Mode then
+ return Arg;
+ end if;
+ end if;
+
+ -- Some or all arguments may appear as component associatons
+
+ if Present (Component_Associations (Args)) then
+ Arg := First (Component_Associations (Args));
+ while Present (Arg) loop
+ if Chars (First (Choices (Arg))) = Arg_Nam then
+ return Arg;
+ end if;
+
+ Next (Arg);
+ end loop;
+ end if;
+ end if;
+
+ -- Otherwise retrieve the argument directly from the pragma
+
+ else
+ Arg := First (Pragma_Argument_Associations (Prag));
+
+ if Present (Arg) and then Arg_Nam = Name_Name then
+ return Arg;
+ end if;
+
+ -- Skip argument "Name"
+
+ Arg := Next (Arg);
+
+ if Present (Arg) and then Arg_Nam = Name_Mode then
+ return Arg;
+ end if;
+
+ -- Skip argument "Mode"
+
+ Arg := Next (Arg);
+
+ -- Arguments "Requires" and "Ensures" are optional and may not be
+ -- present at all.
+
+ while Present (Arg) loop
+ if Chars (Arg) = Arg_Nam then
+ return Arg;
+ end if;
+
+ Next (Arg);
+ end loop;
+ end if;
+
+ return Empty;
+ end Test_Case_Arg;
+
-------------------------------
-- Update_Primitives_Mapping --
-------------------------------
Subp_Id : Entity_Id)
is
function Overridden_Ancestor (S : Entity_Id) return Entity_Id;
+ -- ??? what does this routine do?
-------------------------
-- Overridden_Ancestor --
begin
Anc := S;
- -- Locate the ancestor subprogram with the proper controlling
- -- type.
+ -- Locate the ancestor subprogram with the proper controlling type
while Present (Overridden_Operation (Anc)) loop
Anc := Overridden_Operation (Anc);
-- Start of processing for Primitive_Mapping
begin
- -- if the types are already in the map, it has been previously built
- -- for some other overriding primitive.
+ -- If the types are already in the map, it has been previously built for
+ -- some other overriding primitive.
- if Primitives_Mapping.Get (Old_Typ) = Typ then
+ if Primitives_Mapping.Get (Old_Typ) = Typ then
return;
else
-
- -- initialize new mapping with the primitive operations.
+ -- Initialize new mapping with the primitive operations
Decl := First (List_Containing (Unit_Declaration_Node (Subp_Id)));
- -- look for primitive operations of the current type that have
+ -- Look for primitive operations of the current type that have
-- overridden an operation of the type related to the original
- -- class-wide precondition. there may be several intermediate
+ -- class-wide precondition. There may be several intermediate
-- overridings between them.
while Present (Decl) loop
Next (Decl);
end loop;
- -- now examine inherited operations. these do not override, but have
- -- an alias, which is the entity used in a call. that alias may be
+ -- Now examine inherited operations. these do not override, but have
+ -- an alias, which is the entity used in a call. That alias may be
-- inherited or come from source, in which case it may override an
- -- earlier operation. we only need to examine inherited functions,
+ -- earlier operation. We only need to examine inherited functions,
-- that can appear within the inherited expression.
Prim := First_Entity (Scope (Subp_Id));
Next_Entity (Prim);
end loop;
- -- if the parent operation is an interface operation, the
- -- overriding indicator is not present. instead, we get from
- -- the interface operation the primitive of the current type
- -- that implements it.
+ -- If the parent operation is an interface operation, the overriding
+ -- indicator is not present. Instead, we get from the interface
+ -- operation the primitive of the current type that implements it.
if Is_Interface (Old_Typ) then
Old_Elmt := First_Elmt (Collect_Primitive_Operations (Old_Typ));
end if;
end if;
- -- map the types themselves, so that the process is not repeated for
+ -- Map the types themselves, so that the process is not repeated for
-- other overriding primitives.
Primitives_Mapping.Set (Old_Typ, Typ);
end Update_Primitives_Mapping;
- -------------------
- -- Test_Case_Arg --
- -------------------
-
- function Test_Case_Arg
- (Prag : Node_Id;
- Arg_Nam : Name_Id;
- From_Aspect : Boolean := False) return Node_Id
- is
- Aspect : constant Node_Id := Corresponding_Aspect (Prag);
- Arg : Node_Id;
- Args : Node_Id;
-
- begin
- pragma Assert (Nam_In (Arg_Nam, Name_Ensures,
- Name_Mode,
- Name_Name,
- Name_Requires));
-
- -- The caller requests the aspect argument
-
- if From_Aspect then
- if Present (Aspect)
- and then Nkind (Expression (Aspect)) = N_Aggregate
- then
- Args := Expression (Aspect);
-
- -- "Name" and "Mode" may appear without an identifier as a
- -- positional association.
-
- if Present (Expressions (Args)) then
- Arg := First (Expressions (Args));
-
- if Present (Arg) and then Arg_Nam = Name_Name then
- return Arg;
- end if;
-
- -- Skip "Name"
-
- Arg := Next (Arg);
-
- if Present (Arg) and then Arg_Nam = Name_Mode then
- return Arg;
- end if;
- end if;
-
- -- Some or all arguments may appear as component associatons
-
- if Present (Component_Associations (Args)) then
- Arg := First (Component_Associations (Args));
- while Present (Arg) loop
- if Chars (First (Choices (Arg))) = Arg_Nam then
- return Arg;
- end if;
-
- Next (Arg);
- end loop;
- end if;
- end if;
-
- -- Otherwise retrieve the argument directly from the pragma
-
- else
- Arg := First (Pragma_Argument_Associations (Prag));
-
- if Present (Arg) and then Arg_Nam = Name_Name then
- return Arg;
- end if;
-
- -- Skip argument "Name"
-
- Arg := Next (Arg);
-
- if Present (Arg) and then Arg_Nam = Name_Mode then
- return Arg;
- end if;
-
- -- Skip argument "Mode"
-
- Arg := Next (Arg);
-
- -- Arguments "Requires" and "Ensures" are optional and may not be
- -- present at all.
-
- while Present (Arg) loop
- if Chars (Arg) = Arg_Nam then
- return Arg;
- end if;
-
- Next (Arg);
- end loop;
- end if;
-
- return Empty;
- end Test_Case_Arg;
-
end Sem_Prag;
projects / gcc.git / commitdiff