[multiple changes]
authorArnaud Charlet <charlet@gcc.gnu.org>
Tue, 2 Aug 2011 15:21:19 +0000 (17:21 +0200)
committerArnaud Charlet <charlet@gcc.gnu.org>
Tue, 2 Aug 2011 15:21:19 +0000 (17:21 +0200)
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

16 files changed:
gcc/ada/ChangeLog
gcc/ada/erroutc.ads
gcc/ada/exp_ch3.adb
gcc/ada/exp_ch9.adb
gcc/ada/exp_disp.adb
gcc/ada/exp_sel.adb
gcc/ada/gnat_rm.texi
gcc/ada/link.c
gcc/ada/par-ch11.adb
gcc/ada/par-ch6.adb
gcc/ada/par-ch7.adb
gcc/ada/restrict.adb
gcc/ada/restrict.ads
gcc/ada/scans.ads
gcc/ada/scng.adb
gcc/ada/types.ads

index 1d855df2a83a056f8409abd055a2da7e033cb379..ff0670569f62efbf6a2f32ef57cdfee5ff0e497b 100644 (file)
@@ -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
index d7628ed01ca9ca31dc535767a7ae87769764a600..df29bad07a3eda61453bdf8f72c5b59a73d64f41 100644 (file)
@@ -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
index 561b138cc711e8f02e1c55343ee600ca64dc3816..c54f3b08ad2d8641bdddfe526063b951afe33e1c 100644 (file)
@@ -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)
index 6a15dd532e56874054e4761ddc5e2e3ba32c7b94..986ed35092b62092a58eaedd447f9a8db3c436fb 100644 (file)
@@ -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
index 553bb4dbdc3f664d626b990426ad51f674f91e0d..9b9946676392f3486ec604112505e8936e782c18 100644 (file)
@@ -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)
index 8250516a04f7629d637d80227b2e9beb6a4cdd76..0c17bd16374f2ae4094b67e94d83e6c2b9c3e77b 100644 (file)
@@ -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- --
 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;
index 94da75d25eeff6b95e3e98b7a2639346c786d28f..cc3435b05815714e46841f8544df4ecbf3347373 100644 (file)
@@ -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,
+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
index a4722d2d3ab57dc027796b0d4a0a8d3675560f76..3c21c975e8e8ec9df22726b39dc7ab4a4f9d12ed 100644 (file)
@@ -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 = "";
index b0b0842b9c1191268e6bbacf366bacd0c435fbe8..a11894cb8f8778dab77fd4febbd6fbea943d1cdc 100644 (file)
@@ -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;
 
index bcb6161fdd44ac46b61f93930587f866597bb771..97dd084302fa16a583d0414b91ec8fdc0c8c1a59 100644 (file)
@@ -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;
index d05aa889801364ed19e2a68410e5575875990df1..15f98bfcfb336f6b793a2d6e9008de5e61b48c17 100644 (file)
@@ -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
index b37a593b8beae6cc3d4dae53c9fb03710f019798..e12dd6396b58b1c6b30fbf5a2990a8519bfbc8df 100644 (file)
@@ -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 --
    ------------------------------
index 46626c96fae406239f9ad2dd0b785c5999230372..001d13166bbd93ed6fa84e51bd3e1e2471d27f6e 100644 (file)
@@ -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;
index fcf474bc8194842f62f241ba359f3b546c1674cb..137f616ccc24d0b5f60e0d91ee9fb42bff71990d 100644 (file)
@@ -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.
index f1386f8fce887457e7cbee38a291af2386677b03..420a4f0f03758e9af04f17e4afcfd626a36194c8 100644 (file)
@@ -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;
 
index ee2966c86a75fe49b6740be44923fb28e2e035a8..0422d82b7e82bab7dd4119dc6c43f9becd8ee534 100644 (file)
@@ -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.