[multiple changes]
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. From-SVN: r177179
This commit is contained in:
parent
6ff6152d50
commit
4fbad0ba4c
|
@ -1,3 +1,64 @@
|
|||
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
|
||||
|
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- 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- --
|
||||
|
@ -228,11 +228,11 @@ package Erroutc is
|
|||
--------------------------
|
||||
|
||||
-- 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
|
||||
|
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- 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- --
|
||||
|
@ -8405,12 +8405,10 @@ package body Exp_Ch3 is
|
|||
-- 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)
|
||||
|
@ -8454,12 +8452,22 @@ package body Exp_Ch3 is
|
|||
-- 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,
|
||||
|
@ -8923,18 +8931,26 @@ package body Exp_Ch3 is
|
|||
|
||||
-- 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)
|
||||
|
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- 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- --
|
||||
|
@ -8695,14 +8695,41 @@ package body Exp_Ch9 is
|
|||
-- (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
|
||||
|
||||
|
@ -10878,7 +10905,7 @@ package body Exp_Ch9 is
|
|||
-- 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
|
||||
|
|
|
@ -759,7 +759,11 @@ package body Exp_Disp is
|
|||
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;
|
||||
|
||||
|
@ -2147,7 +2151,11 @@ package body Exp_Disp is
|
|||
|
||||
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
|
||||
|
@ -6307,12 +6315,178 @@ package body Exp_Disp is
|
|||
-----------------
|
||||
|
||||
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;
|
||||
|
@ -6334,12 +6508,13 @@ package body Exp_Disp is
|
|||
|
||||
-- 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
|
||||
-- ...));
|
||||
|
@ -6371,9 +6546,15 @@ package body Exp_Disp is
|
|||
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,
|
||||
|
@ -6431,17 +6612,27 @@ package body Exp_Disp is
|
|||
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;
|
||||
|
@ -6482,28 +6673,6 @@ package body Exp_Disp is
|
|||
-- 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)
|
||||
|
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- 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- --
|
||||
|
@ -26,7 +26,10 @@
|
|||
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;
|
||||
|
||||
|
@ -144,8 +147,19 @@ package body Exp_Sel is
|
|||
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,
|
||||
|
@ -154,8 +168,7 @@ package body Exp_Sel is
|
|||
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;
|
||||
|
||||
|
@ -186,16 +199,47 @@ package body Exp_Sel is
|
|||
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;
|
||||
|
|
|
@ -1770,70 +1770,75 @@ gnat_ugn, @value{EDITION} User's Guide}.
|
|||
Syntax:
|
||||
|
||||
@smallexample @c ada
|
||||
pragma Eliminate (UNIT_NAME, ENTITY, Source_Location => SOURCE_TRACE)
|
||||
|
||||
UNIT_NAME ::= IDENTIFIER |
|
||||
SELECTED_COMPONENT,
|
||||
|
||||
ENTITY ::= IDENTIFIER |
|
||||
SELECTED_COMPONENT,
|
||||
|
||||
SOURCE_TRACE ::= SOURCE_REFERENCE |
|
||||
SOURCE_REFERENCE LBRACKET SOURCE_TRACE RBRACKET
|
||||
|
||||
LBRACKET ::= [
|
||||
RBRACKET ::= ]
|
||||
|
||||
SOURCE_REFERENCE ::= FILE_NAME : LINE_NUMBER
|
||||
|
||||
FILE_NAME ::= STRING_LITERAL
|
||||
LINE_NUMBER ::= INTEGER_LITERAL
|
||||
pragma Eliminate ([Entity =>] DEFINING_DESIGNATOR,
|
||||
[Source_Location =>] STRING_LITERAL);
|
||||
@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.
|
||||
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:
|
||||
|
||||
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.
|
||||
@smallexample @c ada
|
||||
SOURCE_TRACE ::= SOURCE_REFERENCE [LBRACKET SOURCE_TRACE RBRACKET]
|
||||
|
||||
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.
|
||||
LBRACKET ::= [
|
||||
RBRACKET ::= ]
|
||||
|
||||
SOURCE_REFERENCE ::= FILE_NAME : LINE_NUMBER
|
||||
|
||||
LINE_NUMBER ::= DIGIT @{DIGIT@}
|
||||
@end smallexample
|
||||
|
||||
@noindent
|
||||
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.
|
||||
|
||||
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.
|
||||
|
||||
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
|
||||
|
|
|
@ -37,6 +37,7 @@ extern "C" {
|
|||
#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. */
|
||||
|
@ -160,36 +161,6 @@ 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 (__FreeBSD__)
|
||||
const char *__gnat_object_file_option = "";
|
||||
const char *__gnat_run_path_option = "-Wl,-rpath,";
|
||||
|
@ -230,6 +201,51 @@ const char *__gnat_default_libgcc_subdir = "lib64";
|
|||
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 = "";
|
||||
|
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- 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- --
|
||||
|
@ -56,11 +56,28 @@ package body Ch11 is
|
|||
-- 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));
|
||||
|
||||
|
@ -70,6 +87,10 @@ package body Ch11 is
|
|||
(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;
|
||||
|
||||
|
@ -229,10 +250,26 @@ package body Ch11 is
|
|||
-- 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);
|
||||
|
||||
|
@ -253,6 +290,10 @@ package body Ch11 is
|
|||
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;
|
||||
|
||||
|
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- 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- --
|
||||
|
@ -628,6 +628,9 @@ package body Ch6 is
|
|||
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
|
||||
|
@ -770,7 +773,26 @@ package body Ch6 is
|
|||
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;
|
||||
|
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- 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- --
|
||||
|
@ -110,6 +110,10 @@ package body Ch7 is
|
|||
-- 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;
|
||||
|
@ -153,7 +157,26 @@ package body Ch7 is
|
|||
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
|
||||
|
@ -249,9 +272,28 @@ package body Ch7 is
|
|||
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
|
||||
|
|
|
@ -119,6 +119,12 @@ package body Restrict is
|
|||
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.
|
||||
|
@ -141,6 +147,12 @@ package body Restrict is
|
|||
|
||||
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.
|
||||
|
@ -548,6 +560,25 @@ package body Restrict is
|
|||
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 --
|
||||
-------------------------------
|
||||
|
@ -840,6 +871,17 @@ package body Restrict is
|
|||
end if;
|
||||
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 --
|
||||
------------------------------
|
||||
|
|
|
@ -174,6 +174,30 @@ package Restrict is
|
|||
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 --
|
||||
-----------------
|
||||
|
@ -289,6 +313,10 @@ package Restrict is
|
|||
-- 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
|
||||
|
@ -334,6 +362,9 @@ package Restrict is
|
|||
-- 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;
|
||||
|
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- 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- --
|
||||
|
@ -213,6 +213,9 @@ package Scans is
|
|||
-- 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.
|
||||
|
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- 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- --
|
||||
|
@ -184,7 +184,7 @@ package body Scng is
|
|||
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),
|
||||
|
@ -249,7 +249,7 @@ package body Scng is
|
|||
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),
|
||||
|
@ -1761,6 +1761,42 @@ package body Scng is
|
|||
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;
|
||||
|
||||
|
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- 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- --
|
||||
|
@ -188,7 +188,7 @@ package Types is
|
|||
-- 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.
|
||||
|
|
Loading…
Reference in New Issue