+2011-08-02 Sergey Rybin <rybin@adacore.com>
+
+ * gnat_rm.texi: Ramification of pragma Eliminate documentation
+ - fix bugs in the description of Source_Trace;
+ - get rid of UNIT_NAME;
+
+2011-08-02 Javier Miranda <miranda@adacore.com>
+
+ * exp_ch9.adb
+ (Build_Dispatching_Requeue): Adding support for VM targets
+ since we cannot directly reference the Tag entity.
+ * exp_sel.adb (Build_K): Adding support for VM targets.
+ (Build_S_Assignment): Adding support for VM targets.
+ * exp_disp.adb
+ (Default_Prim_Op_Position): In VM targets do not restrict availability
+ of predefined interface primitives to compiling in Ada 2005 mode.
+ (Is_Predefined_Interface_Primitive): In VM targets this service is not
+ restricted to compiling in Ada 2005 mode.
+ (Make_VM_TSD): Generate code that declares and initializes the OSD
+ record. Needed to support dispatching calls through synchronized
+ interfaces.
+ * exp_ch3.adb
+ (Make_Predefined_Primitive_Specs): Enable generation of predefined
+ primitives associated with synchronized interfaces.
+ (Make_Predefined_Primitive_Bodies): Enable generation of predefined
+ primitives associated with synchronized interfaces.
+
+2011-08-02 Yannick Moy <moy@adacore.com>
+
+ * par-ch11.adb (P_Handled_Sequence_Of_Statements): mark a sequence of
+ statements hidden in SPARK if preceded by the HIDE directive
+ (Parse_Exception_Handlers): mark each exception handler in a sequence of
+ exception handlers as hidden in SPARK if preceded by the HIDE directive
+ * par-ch6.adb (P_Subprogram): mark a subprogram body hidden in SPARK
+ if starting with the HIDE directive
+ * par-ch7.adb (P_Package): mark a package body hidden in SPARK if
+ starting with the HIDE directive; mark the declarations in a private
+ part as hidden in SPARK if the private part starts with the HIDE
+ directive
+ * restrict.adb, restrict.ads
+ (Set_Hidden_Part_In_SPARK): record a range of slocs as hidden in SPARK
+ (Is_In_Hidden_Part_In_SPARK): new function which returns whether its
+ argument node belongs to a part which is hidden in SPARK
+ (Check_SPARK_Restriction): do not issue violations on nodes in hidden
+ parts in SPARK; protect the possibly costly call to
+ Is_In_Hidden_Part_In_SPARK by a check that the SPARK restriction is on
+ * scans.ads (Token_Type): new value Tok_SPARK_Hide in enumeration
+ * scng.adb (Accumulate_Token_Checksum_GNAT_6_3,
+ Accumulate_Token_Checksum_GNAT_5_03): add case for new token
+ Tok_SPARK_Hide.
+ (Scan): recognize special comment starting with '#' and followed by
+ SPARK keyword "hide" as a HIDE directive.
+
+2011-08-02 Yannick Moy <moy@adacore.com>
+
+ * types.ads, erroutc.ads: Minor reformatting.
+
+2011-08-02 Vincent Celier <celier@adacore.com>
+
+ * link.c: Add response file support for cross platforms.
+
2011-08-02 Ed Schonberg <schonberg@adacore.com>
* sem_aggr.adb (Resolve_Array_Aggregate): when copying the expression
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, 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- --
--------------------------
-- Pragma Warnings allows warnings to be turned off for a specified
- -- region of code, and the following tables are the data structure used
+ -- region of code, and the following tables are the data structures used
-- to keep track of these regions.
-- The first table is used for the basic command line control, and for
- -- the forms of Warning with a single ON or OFF parameter
+ -- the forms of Warning with a single ON or OFF parameter.
-- It contains pairs of source locations, the first being the start
-- location for a warnings off region, and the second being the end
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, 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- --
-- Disp_Requeue
-- Disp_Timed_Select
- -- These operations cannot be implemented on VM targets, so we simply
- -- disable their generation in this case. Disable the generation of
- -- these bodies if No_Dispatching_Calls, Ravenscar or ZFP is active.
+ -- Disable the generation of these bodies if No_Dispatching_Calls,
+ -- Ravenscar or ZFP is active.
if Ada_Version >= Ada_2005
- and then Tagged_Type_Expansion
and then not Restriction_Active (No_Dispatching_Calls)
and then not Restriction_Active (No_Select_Statements)
and then RTE_Available (RE_Select_Specific_Data)
-- primitives to override the abstract primitives of the interface
-- type.
+ -- In VM targets we define these primitives in all root tagged types
+ -- that are not interface types. Done because in VM targets we don't
+ -- have secondary dispatch tables and any derivation of Tag_Typ may
+ -- cover limited interfaces (which always have these primitives since
+ -- they may be ancestors of synchronized interface types).
+
elsif (not Is_Interface (Tag_Typ)
and then Is_Interface (Etype (Tag_Typ))
and then Is_Limited_Record (Etype (Tag_Typ)))
or else
(Is_Concurrent_Record_Type (Tag_Typ)
and then Has_Interfaces (Tag_Typ))
+ or else
+ (not Tagged_Type_Expansion
+ and then not Is_Interface (Tag_Typ)
+ and then Tag_Typ = Root_Type (Tag_Typ))
then
Append_To (Res,
Make_Subprogram_Declaration (Loc,
-- The interface versions will have null bodies
- -- These operations cannot be implemented on VM targets, so we simply
- -- disable their generation in this case. Disable the generation of
- -- these bodies if No_Dispatching_Calls, Ravenscar or ZFP is active.
+ -- Disable the generation of these bodies if No_Dispatching_Calls,
+ -- Ravenscar or ZFP is active.
+
+ -- In VM targets we define these primitives in all root tagged types
+ -- that are not interface types. Done because in VM targets we don't
+ -- have secondary dispatch tables and any derivation of Tag_Typ may
+ -- cover limited interfaces (which always have these primitives since
+ -- they may be ancestors of synchronized interface types).
if Ada_Version >= Ada_2005
- and then Tagged_Type_Expansion
and then not Is_Interface (Tag_Typ)
and then
((Is_Interface (Etype (Tag_Typ))
and then Is_Limited_Record (Etype (Tag_Typ)))
- or else (Is_Concurrent_Record_Type (Tag_Typ)
- and then Has_Interfaces (Tag_Typ)))
+ or else
+ (Is_Concurrent_Record_Type (Tag_Typ)
+ and then Has_Interfaces (Tag_Typ))
+ or else
+ (not Tagged_Type_Expansion
+ and then Tag_Typ = Root_Type (Tag_Typ)))
and then not Restriction_Active (No_Dispatching_Calls)
and then not Restriction_Active (No_Select_Statements)
and then RTE_Available (RE_Select_Specific_Data)
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, 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- --
-- (Ada.Tags.Tag (Concval),
-- <interface dispatch table position of Ename>)
- Prepend_To (Params,
- Make_Function_Call (Loc,
- Name =>
- New_Reference_To (RTE (RE_Get_Offset_Index), Loc),
+ if Tagged_Type_Expansion then
+ Prepend_To (Params,
+ Make_Function_Call (Loc,
+ Name =>
+ New_Reference_To (RTE (RE_Get_Offset_Index), Loc),
- Parameter_Associations => New_List (
- Unchecked_Convert_To (RTE (RE_Tag), Concval),
- Make_Integer_Literal (Loc, DT_Position (Entity (Ename))))));
+ Parameter_Associations => New_List (
+ Unchecked_Convert_To (RTE (RE_Tag), Concval),
+ Make_Integer_Literal (Loc, DT_Position (Entity (Ename))))));
+
+ -- VM targets
+
+ else
+ Prepend_To (Params,
+ Make_Function_Call (Loc,
+ Name =>
+ New_Reference_To (RTE (RE_Get_Offset_Index), Loc),
+
+ Parameter_Associations => New_List (
+ -- Obj_Typ
+
+ Make_Attribute_Reference (Loc,
+ Prefix => Concval,
+ Attribute_Name => Name_Tag),
+
+ -- Tag_Typ
+
+ Make_Attribute_Reference (Loc,
+ Prefix => New_Reference_To (Etype (Concval), Loc),
+ Attribute_Name => Name_Tag),
+
+ -- Position
+
+ Make_Integer_Literal (Loc, DT_Position (Entity (Ename))))));
+ end if;
-- Specific actuals for protected to XXX requeue
-- Ada.Tags.Get_Tagged_Kind (Ada.Tags.Tag (<object>));
-- M : Integer :=...;
-- P : Parameters := (Param1 .. ParamN);
- -- S : Iteger;
+ -- S : Integer;
-- begin
-- if K = Ada.Tags.TK_Limited_Tagged then
elsif TSS_Name = TSS_Deep_Finalize then
return Uint_10;
- elsif Ada_Version >= Ada_2005 then
+ -- In VM targets unconditionally allow obtaining the position associated
+ -- with predefined interface primitives since in these platforms any
+ -- tagged type has these primitives.
+
+ elsif Ada_Version >= Ada_2005 or else not Tagged_Type_Expansion then
if Chars (E) = Name_uDisp_Asynchronous_Select then
return Uint_11;
function Is_Predefined_Interface_Primitive (E : Entity_Id) return Boolean is
begin
- return Ada_Version >= Ada_2005
+ -- In VM targets we don't restrict the functionality of this test to
+ -- compiling in Ada 2005 mode since in VM targets any tagged type has
+ -- these primitives
+
+ return (Ada_Version >= Ada_2005 or else not Tagged_Type_Expansion)
and then (Chars (E) = Name_uDisp_Asynchronous_Select or else
Chars (E) = Name_uDisp_Conditional_Select or else
Chars (E) = Name_uDisp_Get_Prim_Op_Kind or else
-----------------
function Make_VM_TSD (Typ : Entity_Id) return List_Id is
- Loc : constant Source_Ptr := Sloc (Typ);
- Result : constant List_Id := New_List;
+ Loc : constant Source_Ptr := Sloc (Typ);
+ Result : constant List_Id := New_List;
+
+ function Count_Primitives (Typ : Entity_Id) return Nat;
+ -- Count the non-predefined primitive operations of Typ
+
+ ----------------------
+ -- Count_Primitives --
+ ----------------------
+
+ function Count_Primitives (Typ : Entity_Id) return Nat is
+ Nb_Prim : Nat;
+ Prim_Elmt : Elmt_Id;
+ Prim : Entity_Id;
+
+ begin
+ Nb_Prim := 0;
+
+ Prim_Elmt := First_Elmt (Primitive_Operations (Typ));
+ while Present (Prim_Elmt) loop
+ Prim := Node (Prim_Elmt);
+
+ if Is_Predefined_Dispatching_Operation (Prim)
+ or else Is_Predefined_Dispatching_Alias (Prim)
+ then
+ null;
+
+ elsif Present (Interface_Alias (Prim)) then
+ null;
+
+ else
+ Nb_Prim := Nb_Prim + 1;
+ end if;
+
+ Next_Elmt (Prim_Elmt);
+ end loop;
+
+ return Nb_Prim;
+ end Count_Primitives;
+
+ --------------
+ -- Make_OSD --
+ --------------
+
+ function Make_OSD (Iface : Entity_Id) return Node_Id;
+ -- Generate the Object Specific Data table required to dispatch calls
+ -- through synchronized interfaces. Returns a node that references the
+ -- generated OSD object.
+
+ function Make_OSD (Iface : Entity_Id) return Node_Id is
+ Nb_Prim : constant Nat := Count_Primitives (Iface);
+ OSD : Entity_Id;
+ OSD_Aggr_List : List_Id;
+
+ begin
+ -- Generate
+ -- OSD : Ada.Tags.Object_Specific_Data (Nb_Prims) :=
+ -- (OSD_Table => (1 => <value>,
+ -- ...
+ -- N => <value>));
+
+ if Nb_Prim = 0
+ or else Is_Abstract_Type (Typ)
+ or else Is_Controlled (Typ)
+ or else Restriction_Active (No_Dispatching_Calls)
+ or else not Is_Limited_Type (Typ)
+ or else not Has_Interfaces (Typ)
+ or else not RTE_Record_Component_Available (RE_OSD_Table)
+ then
+ -- No OSD table required
+
+ return Make_Null (Loc);
+
+ else
+ OSD_Aggr_List := New_List;
+
+ declare
+ Prim_Table : array (Nat range 1 .. Nb_Prim) of Entity_Id;
+ Prim : Entity_Id;
+ Prim_Alias : Entity_Id;
+ Prim_Elmt : Elmt_Id;
+ E : Entity_Id;
+ Count : Nat := 0;
+ Pos : Nat;
+
+ begin
+ Prim_Table := (others => Empty);
+ Prim_Alias := Empty;
+
+ Prim_Elmt := First_Elmt (Primitive_Operations (Typ));
+ while Present (Prim_Elmt) loop
+ Prim := Node (Prim_Elmt);
+
+ if Present (Interface_Alias (Prim))
+ and then Find_Dispatching_Type
+ (Interface_Alias (Prim)) = Iface
+ then
+ Prim_Alias := Interface_Alias (Prim);
+ E := Ultimate_Alias (Prim);
+ Pos := UI_To_Int (DT_Position (Prim_Alias));
+
+ if Present (Prim_Table (Pos)) then
+ pragma Assert (Prim_Table (Pos) = E);
+ null;
+
+ else
+ Prim_Table (Pos) := E;
+
+ Append_To (OSD_Aggr_List,
+ Make_Component_Association (Loc,
+ Choices => New_List (
+ Make_Integer_Literal (Loc,
+ DT_Position (Prim_Alias))),
+ Expression =>
+ Make_Integer_Literal (Loc,
+ DT_Position (Alias (Prim)))));
+
+ Count := Count + 1;
+ end if;
+ end if;
+
+ Next_Elmt (Prim_Elmt);
+ end loop;
+ pragma Assert (Count = Nb_Prim);
+ end;
+
+ OSD := Make_Temporary (Loc, 'I');
+
+ Append_To (Result,
+ Make_Object_Declaration (Loc,
+ Defining_Identifier => OSD,
+ Aliased_Present => True,
+ Constant_Present => True,
+ Object_Definition =>
+ Make_Subtype_Indication (Loc,
+ Subtype_Mark =>
+ New_Reference_To (RTE (RE_Object_Specific_Data), Loc),
+ Constraint =>
+ Make_Index_Or_Discriminant_Constraint (Loc,
+ Constraints => New_List (
+ Make_Integer_Literal (Loc, Nb_Prim)))),
+
+ Expression =>
+ Make_Aggregate (Loc,
+ Component_Associations => New_List (
+ Make_Component_Association (Loc,
+ Choices => New_List (
+ New_Occurrence_Of
+ (RTE_Record_Component (RE_OSD_Num_Prims), Loc)),
+ Expression =>
+ Make_Integer_Literal (Loc, Nb_Prim)),
+
+ Make_Component_Association (Loc,
+ Choices => New_List (
+ New_Occurrence_Of
+ (RTE_Record_Component (RE_OSD_Table), Loc)),
+ Expression => Make_Aggregate (Loc,
+ Component_Associations => OSD_Aggr_List))))));
+
+ return
+ Make_Attribute_Reference (Loc,
+ Prefix => New_Reference_To (OSD, Loc),
+ Attribute_Name => Name_Unchecked_Access);
+ end if;
+ end Make_OSD;
+
+ -- Local variables
+
+ Nb_Prim : constant Nat := Count_Primitives (Typ);
AI : Elmt_Id;
I_Depth : Nat;
Iface_Table_Node : Node_Id;
- Nb_Prim : Nat;
Num_Ifaces : Nat;
TSD_Aggr_List : List_Id;
Typ_Ifaces : Elist_Id;
-- TSD : Type_Specific_Data (I_Depth) :=
-- (Idepth => I_Depth,
- -- T => T'Tag,
+ -- Tag_Kind => <tag_kind-value>,
-- Access_Level => Type_Access_Level (Typ),
-- HT_Link => null,
-- Type_Is_Abstract => <<boolean-value>>,
-- Type_Is_Library_Level => <<boolean-value>>,
-- Interfaces_Table => <<access-value>>
+ -- SSD => SSD_Table'Address
-- Tags_Table => (0 => Typ'Tag,
-- 1 => Parent'Tag
-- ...));
end loop;
end;
+ -- I_Depth
+
Append_To (TSD_Aggr_List,
Make_Integer_Literal (Loc, I_Depth));
+ -- Tag_Kind
+
+ Append_To (TSD_Aggr_List, Tagged_Kind (Typ));
+
-- Access_Level
Append_To (TSD_Aggr_List,
else
declare
TSD_Ifaces_List : constant List_Id := New_List;
+ Iface : Entity_Id;
ITable : Node_Id;
begin
AI := First_Elmt (Typ_Ifaces);
while Present (AI) loop
+ Iface := Node (AI);
+
Append_To (TSD_Ifaces_List,
Make_Aggregate (Loc,
Expressions => New_List (
+
+ -- Iface_Tag
+
Make_Attribute_Reference (Loc,
- Prefix => New_Reference_To (Node (AI), Loc),
- Attribute_Name => Name_Tag))));
+ Prefix => New_Reference_To (Iface, Loc),
+ Attribute_Name => Name_Tag),
+
+ -- OSD
+
+ Make_OSD (Iface))));
Next_Elmt (AI);
end loop;
-- implement synchronized interfaces. The size of the table is
-- constrained by the number of non-predefined primitive operations.
- -- Count the non-predefined primitive operations
-
- Nb_Prim := 0;
-
- declare
- Prim_Elmt : Elmt_Id;
- Prim : Entity_Id;
- begin
- Prim_Elmt := First_Elmt (Primitive_Operations (Typ));
- while Present (Prim_Elmt) loop
- Prim := Node (Prim_Elmt);
-
- if not (Is_Predefined_Dispatching_Operation (Prim)
- or else Is_Predefined_Dispatching_Alias (Prim))
- then
- Nb_Prim := Nb_Prim + 1;
- end if;
-
- Next_Elmt (Prim_Elmt);
- end loop;
- end;
-
if RTE_Record_Component_Available (RE_SSD) then
if Ada_Version >= Ada_2005
and then Has_DT (Typ)
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, 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- --
with Einfo; use Einfo;
with Nlists; use Nlists;
with Nmake; use Nmake;
+with Opt; use Opt;
with Rtsfind; use Rtsfind;
+with Sinfo; use Sinfo;
+with Snames; use Snames;
with Stand; use Stand;
with Tbuild; use Tbuild;
Decls : List_Id;
Obj : Entity_Id) return Entity_Id
is
- K : constant Entity_Id := Make_Temporary (Loc, 'K');
+ K : constant Entity_Id := Make_Temporary (Loc, 'K');
+ Tag_Node : Node_Id;
+
begin
+ if Tagged_Type_Expansion then
+ Tag_Node := Unchecked_Convert_To (RTE (RE_Tag), Obj);
+ else
+ Tag_Node :=
+ Make_Attribute_Reference (Loc,
+ Prefix => Obj,
+ Attribute_Name => Name_Tag);
+ end if;
+
Append_To (Decls,
Make_Object_Declaration (Loc,
Defining_Identifier => K,
Expression =>
Make_Function_Call (Loc,
Name => New_Reference_To (RTE (RE_Get_Tagged_Kind), Loc),
- Parameter_Associations => New_List (
- Unchecked_Convert_To (RTE (RE_Tag), Obj)))));
+ Parameter_Associations => New_List (Tag_Node))));
return K;
end Build_K;
Obj : Entity_Id;
Call_Ent : Entity_Id) return Node_Id
is
+ Typ : constant Entity_Id := Etype (Obj);
+
begin
- return
- Make_Assignment_Statement (Loc,
- Name => New_Reference_To (S, Loc),
- Expression =>
- Make_Function_Call (Loc,
- Name => New_Reference_To (RTE (RE_Get_Offset_Index), Loc),
- Parameter_Associations => New_List (
- Unchecked_Convert_To (RTE (RE_Tag), Obj),
- Make_Integer_Literal (Loc, DT_Position (Call_Ent)))));
+ if Tagged_Type_Expansion then
+ return
+ Make_Assignment_Statement (Loc,
+ Name => New_Reference_To (S, Loc),
+ Expression =>
+ Make_Function_Call (Loc,
+ Name => New_Reference_To (RTE (RE_Get_Offset_Index), Loc),
+ Parameter_Associations => New_List (
+ Unchecked_Convert_To (RTE (RE_Tag), Obj),
+ Make_Integer_Literal (Loc, DT_Position (Call_Ent)))));
+
+ -- VM targets
+
+ else
+ return
+ Make_Assignment_Statement (Loc,
+ Name => New_Reference_To (S, Loc),
+ Expression =>
+ Make_Function_Call (Loc,
+ Name => New_Reference_To (RTE (RE_Get_Offset_Index), Loc),
+ Parameter_Associations => New_List (
+
+ -- Obj_Typ
+
+ Make_Attribute_Reference (Loc,
+ Prefix => Obj,
+ Attribute_Name => Name_Tag),
+
+ -- Iface_Typ
+
+ Make_Attribute_Reference (Loc,
+ Prefix => New_Reference_To (Typ, Loc),
+ Attribute_Name => Name_Tag),
+
+ -- Position
+
+ Make_Integer_Literal (Loc, DT_Position (Call_Ent)))));
+ end if;
end Build_S_Assignment;
end Exp_Sel;
Syntax:
@smallexample @c ada
-pragma Eliminate (UNIT_NAME, ENTITY, Source_Location => SOURCE_TRACE)
-
-UNIT_NAME ::= IDENTIFIER |
- SELECTED_COMPONENT,
+pragma Eliminate ([Entity =>] DEFINING_DESIGNATOR,
+ [Source_Location =>] STRING_LITERAL);
+@end smallexample
-ENTITY ::= IDENTIFIER |
- SELECTED_COMPONENT,
+@noindent
+The string literal given for the source location is a string which
+specifies the line number of the occurrence of the entity, using
+the syntax for SOURCE_TRACE given below:
-SOURCE_TRACE ::= SOURCE_REFERENCE |
- SOURCE_REFERENCE LBRACKET SOURCE_TRACE RBRACKET
+@smallexample @c ada
+ SOURCE_TRACE ::= SOURCE_REFERENCE [LBRACKET SOURCE_TRACE RBRACKET]
-LBRACKET ::= [
-RBRACKET ::= ]
+ LBRACKET ::= [
+ RBRACKET ::= ]
-SOURCE_REFERENCE ::= FILE_NAME : LINE_NUMBER
+ SOURCE_REFERENCE ::= FILE_NAME : LINE_NUMBER
-FILE_NAME ::= STRING_LITERAL
-LINE_NUMBER ::= INTEGER_LITERAL
+ LINE_NUMBER ::= DIGIT @{DIGIT@}
@end smallexample
@noindent
-This pragma indicates that the given entity is not used in the program
-to be compiled and built. The entity must be an explicitly declared
-subprogram; this includes generic subprogram instances and
-subprograms declared in generic package instances. @code{Unit_Name}
-must be the name of the compilation unit in which the entity is declared.
+Spaces around the colon in a @code{Source_Reference} are optional.
+
+The @code{DEFINING_DESIGNATOR} matches the defining designator used in an
+explicit subprogram declaration, where the @code{entity} name in this
+designator appears on the source line specified by the source location.
+
+The source trace that is given as the @code{Source_Location} shall obey the
+following rules. The @code{FILE_NAME} is the short name (with no directory
+information) of an Ada source file, given using exactly the required syntax
+for the underlying file system (e.g. case is important if the underlying
+operating system is case sensitive). @code{LINE_NUMBER} gives the line
+number of the occurrence of the @code{entity}
+as a decimal literal without an exponent or point. If an @code{entity} is not
+declared in a generic instantiation (this includes generic subprogram
+instances), the source trace includes only one source reference. If an entity
+is declared inside a generic instantiation, its source trace (when parsing
+from left to right) starts with the source location of the declaration of the
+entity in the generic unit and ends with the source location of the
+instantiation (it is given in square brackets). This approach is recursively
+used in case of nested instantiations: the rightmost (nested most deeply in
+square brackets) element of the source trace is the location of the outermost
+instantiation, the next to left element is the location of the next (first
+nested) instantiation in the code of the corresponding generic unit, and so
+on, and the leftmost element (that is out of any square brackets) is the
+location of the declaration of the entity to eliminate in a generic unit.
-The @code{Source_Location} argument is used to resolve overloading
-in case more then one callable entity with the same name is declared
-in the given compilation unit. Each file name must be the short name of the
-source file (with no directory information).
-If an entity is not declared in
-a generic instantiation (this includes generic subprogram instances),
-the source trace includes only one source
-reference. If an entity is declared inside a generic instantiation,
-its source trace starts from the source location in the instantiation and
-ends with the source location of the declaration of the corresponding
-entity in the generic
-unit. This approach is recursively used in case of nested instantiations:
-the leftmost element of the
-source trace is the location of the outermost instantiation, the next
-element is the location of the next (first nested) instantiation in the
-code of the corresponding generic unit, and so on.
+Note that the @code{Source_Location} argument specifies which of a set of
+similarly named entities is being eliminated, dealing both with overloading,
+and also appearence of the same entity name in different scopes.
-The effect of the pragma is to allow the compiler to eliminate
-the code or data associated with the named entity. Any reference to
-an eliminated entity outside the compilation unit where it is defined
-causes a compile-time or link-time error.
+This pragma indicates that the given entity is not used in the program to be
+compiled and built. The effect of the pragma is to allow the compiler to
+eliminate the code or data associated with the named entity. Any reference to
+an eliminated entity causes a compile-time or link-time error.
The intention of pragma @code{Eliminate} is to allow a program to be compiled
in a system-independent manner, with unused entities eliminated, without
-needing to modify the source text. Normally the required set
-of @code{Eliminate} pragmas is constructed automatically using the gnatelim
-tool. Elimination of unused entities local to a compilation unit is
-automatic, without requiring the use of pragma @code{Eliminate}.
+needing to modify the source text. Normally the required set of
+@code{Eliminate} pragmas is constructed automatically using the gnatelim tool.
Any source file change that removes, splits, or
adds lines may make the set of Eliminate pragmas invalid because their
@code{Source_Location} argument values may get out of date.
-Pragma Eliminate may be used where the referenced entity is a
-dispatching operation. In this case all the subprograms to which the
-given operation can dispatch are considered to be unused (are never called
-as a result of a direct or a dispatching call).
+Pragma @code{Eliminate} may be used where the referenced entity is a dispatching
+operation. In this case all the subprograms to which the given operation can
+dispatch are considered to be unused (are never called as a result of a direct
+or a dispatching call).
@node Pragma Export_Exception
@unnumberedsec Pragma Export_Exception
#endif
#include <string.h>
+#include "auto-host.h"
/* objlist_file_supported is set to 1 when the system linker allows */
/* response file, that is a file that contains the list of object files. */
unsigned char __gnat_separate_run_path_options = 0;
const char *__gnat_default_libgcc_subdir = "lib";
-#elif defined (VMS)
-const char *__gnat_object_file_option = "";
-const char *__gnat_run_path_option = "";
-char __gnat_shared_libgnat_default = STATIC;
-char __gnat_shared_libgcc_default = STATIC;
-int __gnat_link_max = 2147483647;
-unsigned char __gnat_objlist_file_supported = 0;
-unsigned char __gnat_using_gnu_linker = 0;
-const char *__gnat_object_library_extension = ".olb";
-unsigned char __gnat_separate_run_path_options = 0;
-const char *__gnat_default_libgcc_subdir = "lib";
-
-#elif defined (sun)
-const char *__gnat_object_file_option = "";
-const char *__gnat_run_path_option = "-Wl,-R";
-char __gnat_shared_libgnat_default = STATIC;
-char __gnat_shared_libgcc_default = STATIC;
-int __gnat_link_max = 2147483647;
-unsigned char __gnat_objlist_file_supported = 0;
-unsigned char __gnat_using_gnu_linker = 0;
-const char *__gnat_object_library_extension = ".a";
-unsigned char __gnat_separate_run_path_options = 0;
-#if defined (__sparc_v9__) || defined (__sparcv9)
-const char *__gnat_default_libgcc_subdir = "lib/sparcv9";
-#elif defined (__x86_64)
-const char *__gnat_default_libgcc_subdir = "lib/amd64";
-#else
-const char *__gnat_default_libgcc_subdir = "lib";
-#endif
-
#elif defined (__FreeBSD__)
const char *__gnat_object_file_option = "";
const char *__gnat_run_path_option = "-Wl,-rpath,";
const char *__gnat_default_libgcc_subdir = "lib";
#endif
+#elif (HAVE_GNU_LD)
+/* These are the settings for all systems that use gnu ld. GNU style response
+ file is supported, the shared library default is STATIC. */
+
+const char *__gnat_run_path_option = "";
+const char *__gnat_object_file_option = "";
+char __gnat_shared_libgnat_default = STATIC;
+char __gnat_shared_libgcc_default = STATIC;
+int __gnat_link_max = 8192;
+unsigned char __gnat_objlist_file_supported = 1;
+unsigned char __gnat_using_gnu_linker = 1;
+const char *__gnat_object_library_extension = ".a";
+unsigned char __gnat_separate_run_path_options = 0;
+const char *__gnat_default_libgcc_subdir = "lib";
+
+#elif defined (VMS)
+const char *__gnat_object_file_option = "";
+const char *__gnat_run_path_option = "";
+char __gnat_shared_libgnat_default = STATIC;
+char __gnat_shared_libgcc_default = STATIC;
+int __gnat_link_max = 2147483647;
+unsigned char __gnat_objlist_file_supported = 0;
+unsigned char __gnat_using_gnu_linker = 0;
+const char *__gnat_object_library_extension = ".olb";
+unsigned char __gnat_separate_run_path_options = 0;
+const char *__gnat_default_libgcc_subdir = "lib";
+
+#elif defined (sun)
+const char *__gnat_object_file_option = "";
+const char *__gnat_run_path_option = "-Wl,-R";
+char __gnat_shared_libgnat_default = STATIC;
+char __gnat_shared_libgcc_default = STATIC;
+int __gnat_link_max = 2147483647;
+unsigned char __gnat_objlist_file_supported = 0;
+unsigned char __gnat_using_gnu_linker = 0;
+const char *__gnat_object_library_extension = ".a";
+unsigned char __gnat_separate_run_path_options = 0;
+#if defined (__sparc_v9__) || defined (__sparcv9)
+const char *__gnat_default_libgcc_subdir = "lib/sparcv9";
+#elif defined (__x86_64)
+const char *__gnat_default_libgcc_subdir = "lib/amd64";
+#else
+const char *__gnat_default_libgcc_subdir = "lib";
+#endif
+
#elif defined (__svr4__) && defined (i386)
const char *__gnat_object_file_option = "";
const char *__gnat_run_path_option = "";
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, 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- --
-- Error_Recovery : Cannot raise Error_Resync
function P_Handled_Sequence_Of_Statements return Node_Id is
- Handled_Stmt_Seq_Node : Node_Id;
+ Handled_Stmt_Seq_Node : Node_Id;
+ Seq_Is_Hidden_In_SPARK : Boolean;
+ Hidden_Region_Start : Source_Ptr;
begin
Handled_Stmt_Seq_Node :=
New_Node (N_Handled_Sequence_Of_Statements, Token_Ptr);
+
+ -- In SPARK, a HIDE directive can be placed at the beginning of a
+ -- package initialization, thus hiding the sequence of statements (and
+ -- possible exception handlers) from SPARK tool-set. No violation of the
+ -- SPARK restriction should be issued on nodes in a hidden part, which
+ -- is obtained by marking such hidden parts.
+
+ if Token = Tok_SPARK_Hide then
+ Seq_Is_Hidden_In_SPARK := True;
+ Hidden_Region_Start := Token_Ptr;
+ Scan; -- past HIDE directive
+ else
+ Seq_Is_Hidden_In_SPARK := False;
+ end if;
+
Set_Statements
(Handled_Stmt_Seq_Node, P_Sequence_Of_Statements (SS_Extm_Sreq));
(Handled_Stmt_Seq_Node, Parse_Exception_Handlers);
end if;
+ if Seq_Is_Hidden_In_SPARK then
+ Set_Hidden_Part_In_SPARK (Hidden_Region_Start, Token_Ptr);
+ end if;
+
return Handled_Stmt_Seq_Node;
end P_Handled_Sequence_Of_Statements;
-- Error recovery: cannot raise Error_Resync
function Parse_Exception_Handlers return List_Id is
- Handler : Node_Id;
- Handlers_List : List_Id;
+ Handler : Node_Id;
+ Handlers_List : List_Id;
+ Handler_Is_Hidden_In_SPARK : Boolean;
+ Hidden_Region_Start : Source_Ptr;
begin
+ -- In SPARK, a HIDE directive can be placed at the beginning of a
+ -- sequence of exception handlers for a subprogram implementation, thus
+ -- hiding the exception handlers from SPARK tool-set. No violation of
+ -- the SPARK restriction should be issued on nodes in a hidden part,
+ -- which is obtained by marking such hidden parts.
+
+ if Token = Tok_SPARK_Hide then
+ Handler_Is_Hidden_In_SPARK := True;
+ Hidden_Region_Start := Token_Ptr;
+ Scan; -- past HIDE directive
+ else
+ Handler_Is_Hidden_In_SPARK := False;
+ end if;
+
Handlers_List := New_List;
P_Pragmas_Opt (Handlers_List);
end loop;
end if;
+ if Handler_Is_Hidden_In_SPARK then
+ Set_Hidden_Part_In_SPARK (Hidden_Region_Start, Token_Ptr);
+ end if;
+
return Handlers_List;
end Parse_Exception_Handlers;
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, 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- --
else
Scan_Body_Or_Expression_Function : declare
+ Body_Is_Hidden_In_SPARK : Boolean;
+ Hidden_Region_Start : Source_Ptr;
+
function Likely_Expression_Function return Boolean;
-- Returns True if we have a probable case of an expression
-- function omitting the parentheses, if so, returns True
Body_Node :=
New_Node (N_Subprogram_Body, Sloc (Specification_Node));
Set_Specification (Body_Node, Specification_Node);
+
+ -- In SPARK, a HIDE directive can be placed at the beginning
+ -- of a subprogram implementation, thus hiding the
+ -- subprogram body from SPARK tool-set. No violation of the
+ -- SPARK restriction should be issued on nodes in a hidden
+ -- part, which is obtained by marking such hidden parts.
+
+ if Token = Tok_SPARK_Hide then
+ Body_Is_Hidden_In_SPARK := True;
+ Hidden_Region_Start := Token_Ptr;
+ Scan; -- past HIDE directive
+ else
+ Body_Is_Hidden_In_SPARK := False;
+ end if;
+
Parse_Decls_Begin_End (Body_Node);
+
+ if Body_Is_Hidden_In_SPARK then
+ Set_Hidden_Part_In_SPARK (Hidden_Region_Start, Token_Ptr);
+ end if;
end if;
return Body_Node;
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, 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- --
-- Dummy node to attach aspect specifications to until we properly
-- figure out where they eventually belong.
+ Body_Is_Hidden_In_SPARK : Boolean;
+ Private_Part_Is_Hidden_In_SPARK : Boolean;
+ Hidden_Region_Start : Source_Ptr;
+
begin
Push_Scope_Stack;
Scope.Table (Scope.Last).Etyp := E_Name;
else
Package_Node := New_Node (N_Package_Body, Package_Sloc);
Set_Defining_Unit_Name (Package_Node, Name_Node);
+
+ -- In SPARK, a HIDE directive can be placed at the beginning of a
+ -- package implementation, thus hiding the package body from SPARK
+ -- tool-set. No violation of the SPARK restriction should be
+ -- issued on nodes in a hidden part, which is obtained by marking
+ -- such hidden parts.
+
+ if Token = Tok_SPARK_Hide then
+ Body_Is_Hidden_In_SPARK := True;
+ Hidden_Region_Start := Token_Ptr;
+ Scan; -- past HIDE directive
+ else
+ Body_Is_Hidden_In_SPARK := False;
+ end if;
+
Parse_Decls_Begin_End (Package_Node);
+
+ if Body_Is_Hidden_In_SPARK then
+ Set_Hidden_Part_In_SPARK (Hidden_Region_Start, Token_Ptr);
+ end if;
end if;
-- Cases other than Package_Body
end if;
Scan; -- past PRIVATE
+
+ if Token = Tok_SPARK_Hide then
+ Private_Part_Is_Hidden_In_SPARK := True;
+ Hidden_Region_Start := Token_Ptr;
+ Scan; -- past HIDE directive
+ else
+ Private_Part_Is_Hidden_In_SPARK := False;
+ end if;
+
Set_Private_Declarations
(Specification_Node, P_Basic_Declarative_Items);
+ -- In SPARK, a HIDE directive can be placed at the beginning
+ -- of a private part, thus hiding all declarations in the
+ -- private part from SPARK tool-set. No violation of the
+ -- SPARK restriction should be issued on nodes in a hidden
+ -- part, which is obtained by marking such hidden parts.
+
+ if Private_Part_Is_Hidden_In_SPARK then
+ Set_Hidden_Part_In_SPARK (Hidden_Region_Start, Token_Ptr);
+ end if;
+
-- Deal gracefully with multiple PRIVATE parts
while Token = Tok_Private loop
begin
if Force or else Comes_From_Source (N) then
+ if Restriction_Check_Required (SPARK)
+ and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
+ then
+ return;
+ end if;
+
-- Since the call to Restriction_Msg from Check_Restriction may set
-- Error_Msg_Sloc to the location of the pragma restriction, save and
-- restore the previous value of the global variable around the call.
if Comes_From_Source (N) then
+ if Restriction_Check_Required (SPARK)
+ and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
+ then
+ return;
+ end if;
+
-- Since the call to Restriction_Msg from Check_Restriction may set
-- Error_Msg_Sloc to the location of the pragma restriction, save and
-- restore the previous value of the global variable around the call.
return Not_A_Restriction_Id;
end Get_Restriction_Id;
+ --------------------------------
+ -- Is_In_Hidden_Part_In_SPARK --
+ --------------------------------
+
+ function Is_In_Hidden_Part_In_SPARK (Loc : Source_Ptr) return Boolean is
+ begin
+ -- Loop through table of hidden ranges
+
+ for J in SPARK_Hides.First .. SPARK_Hides.Last loop
+ if SPARK_Hides.Table (J).Start <= Loc
+ and then Loc <= SPARK_Hides.Table (J).Stop
+ then
+ return True;
+ end if;
+ end loop;
+
+ return False;
+ end Is_In_Hidden_Part_In_SPARK;
+
-------------------------------
-- No_Exception_Handlers_Set --
-------------------------------
end Same_Unit;
------------------------------
+ -- Set_Hidden_Part_In_SPARK --
+ ------------------------------
+
+ procedure Set_Hidden_Part_In_SPARK (Loc1, Loc2 : Source_Ptr) is
+ begin
+ SPARK_Hides.Increment_Last;
+ SPARK_Hides.Table (SPARK_Hides.Last).Start := Loc1;
+ SPARK_Hides.Table (SPARK_Hides.Last).Stop := Loc2;
+ end Set_Hidden_Part_In_SPARK;
+
+ ------------------------------
-- Set_Profile_Restrictions --
------------------------------
Table_Increment => 200,
Table_Name => "Name_No_Dependence");
+ -------------------------------
+ -- SPARK Restriction Control --
+ -------------------------------
+
+ -- SPARK HIDE directives allow turning off SPARK restriction for a
+ -- specified region of code, and the following tables are the data
+ -- structures used to keep track of these regions.
+
+ -- The table contains pairs of source locations, the first being the start
+ -- location for hidden region, and the second being the end location.
+
+ type SPARK_Hide_Entry is record
+ Start : Source_Ptr;
+ Stop : Source_Ptr;
+ end record;
+
+ package SPARK_Hides is new Table.Table (
+ Table_Component_Type => SPARK_Hide_Entry,
+ Table_Index_Type => Natural,
+ Table_Low_Bound => 1,
+ Table_Initial => 100,
+ Table_Increment => 200,
+ Table_Name => "SPARK Hides");
+
-----------------
-- Subprograms --
-----------------
-- identifier, and if so returns the corresponding Restriction_Id
-- value, otherwise returns Not_A_Restriction_Id.
+ function Is_In_Hidden_Part_In_SPARK (Loc : Source_Ptr) return Boolean;
+ -- Determine if given location is covered by a hidden region range in the
+ -- SPARK hides table.
+
function No_Exception_Handlers_Set return Boolean;
-- Test to see if current restrictions settings specify that no exception
-- handlers are present. This function is called by Gigi when it needs to
-- of individual Restrictions pragmas). Returns True only if all the
-- required restrictions are set.
+ procedure Set_Hidden_Part_In_SPARK (Loc1, Loc2 : Source_Ptr);
+ -- Insert a new hidden region range in the SPARK hides table
+
procedure Set_Profile_Restrictions
(P : Profile_Name;
N : Node_Id;
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, 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- --
-- characters '#', '$', '?', '@', '`', '\', '^', '~', or '_'. The
-- character value itself is stored in Scans.Special_Character.
+ Tok_SPARK_Hide,
+ -- HIDE directive in SPARK
+
No_Token);
-- No_Token is used for initializing Token values to indicate that
-- no value has been set yet.
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, 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- --
Tok_Separate | Tok_EOF | Tok_Semicolon | Tok_Arrow |
Tok_Vertical_Bar | Tok_Dot_Dot | Tok_Project | Tok_Extends |
Tok_External | Tok_External_As_List | Tok_Comment |
- Tok_End_Of_Line | Tok_Special | No_Token =>
+ Tok_End_Of_Line | Tok_Special | Tok_SPARK_Hide | No_Token =>
System.CRC32.Update
(System.CRC32.CRC32 (Checksum),
Tok_Separate | Tok_EOF | Tok_Semicolon | Tok_Arrow |
Tok_Vertical_Bar | Tok_Dot_Dot | Tok_Project | Tok_Extends |
Tok_External | Tok_External_As_List | Tok_Comment |
- Tok_End_Of_Line | Tok_Special | No_Token =>
+ Tok_End_Of_Line | Tok_Special | Tok_SPARK_Hide | No_Token =>
System.CRC32.Update
(System.CRC32.CRC32 (Checksum),
Token := Tok_Comment;
return;
end if;
+
+ if Source (Start_Of_Comment) = '#' then
+ declare
+ Scan_SPARK_Ptr : Source_Ptr;
+
+ begin
+ Scan_SPARK_Ptr := Start_Of_Comment + 1;
+
+ -- Scan out blanks
+
+ while Source (Scan_SPARK_Ptr) = ' '
+ or else Source (Scan_SPARK_Ptr) = HT
+ loop
+ Scan_SPARK_Ptr := Scan_SPARK_Ptr + 1;
+ end loop;
+
+ -- Recognize HIDE directive. SPARK input cannot be
+ -- encoded as wide characters, so only deal with
+ -- lower/upper case.
+
+ if (Source (Scan_SPARK_Ptr) = 'h'
+ or else Source (Scan_SPARK_Ptr) = 'H')
+ and then (Source (Scan_SPARK_Ptr + 1) = 'i'
+ or else Source (Scan_SPARK_Ptr + 1) = 'I')
+ and then (Source (Scan_SPARK_Ptr + 2) = 'd'
+ or else Source (Scan_SPARK_Ptr + 2) = 'D')
+ and then (Source (Scan_SPARK_Ptr + 3) = 'e'
+ or else Source (Scan_SPARK_Ptr + 3) = 'E')
+ and then (Source (Scan_SPARK_Ptr + 4) = ' '
+ or else Source (Scan_SPARK_Ptr + 4) = HT)
+ then
+ Token := Tok_SPARK_Hide;
+ return;
+ end if;
+ end;
+ end if;
end if;
end Minus_Case;
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, 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- --
-- Special value used to indicate no column number
subtype Source_Buffer is Text_Buffer;
- -- Type used to store text of a source file . The buffer for the main
+ -- Type used to store text of a source file. The buffer for the main
-- source (the source specified on the command line) has a lower bound
-- starting at zero. Subsequent subsidiary sources have lower bounds
-- which are one greater than the previous upper bound.