gcc/ada/exp_spark.adb

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT COMPILER COMPONENTS                         --
   4 --                                                                          --
   5 --                            E X P _ S P A R K                             --
   6 --                                                                          --
   7 --                                 B o d y                                  --
   8 --                                                                          --
   9 --          Copyright (C) 1992-2013, Free Software Foundation, Inc.         --
  10 --                                                                          --
  11 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
  12 -- terms of the  GNU General Public License as published  by the Free Soft- --
  13 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
  14 -- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
  15 -- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
  16 -- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
  17 -- for  more details.  You should have  received  a copy of the GNU General --
  18 -- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
  19 -- http://www.gnu.org/licenses for a complete copy of the license.          --
  20 --                                                                          --
  21 -- GNAT was originally developed  by the GNAT team at  New York University. --
  22 -- Extensive contributions were provided by Ada Core Technologies Inc.      --
  23 --                                                                          --
  24 ------------------------------------------------------------------------------
  25
  26 with Atree;    use Atree;
  27 with Einfo;    use Einfo;
  28 with Exp_Dbug; use Exp_Dbug;
  29 with Exp_Util; use Exp_Util;
  30 with Sem_Aux;  use Sem_Aux;
  31 with Sem_Res;  use Sem_Res;
  32 with Sem_Util; use Sem_Util;
  33 with Sinfo;    use Sinfo;
  34
  35 package body Exp_SPARK is
  36
  37    -----------------------
  38    -- Local Subprograms --
  39    -----------------------
  40
  41    procedure Expand_SPARK_Call (N : Node_Id);
  42    --  This procedure contains common processing for function and procedure
  43    --  calls: replacement of renaming by subprogram renamed
  44
  45    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
  46    --  Perform name evaluation for a renamed object
  47
  48    procedure Expand_Potential_Renaming (N : Node_Id);
  49    --  N denotes a N_Identifier or N_Expanded_Name. If N references a renaming,
  50    --  replace N with the renamed object.
  51
  52    ------------------
  53    -- Expand_SPARK --
  54    ------------------
  55
  56    procedure Expand_SPARK (N : Node_Id) is
  57    begin
  58       case Nkind (N) is
  59
  60          --  Qualification of entity names in formal verification mode
  61          --  is limited to the addition of a suffix for homonyms (see
  62          --  Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names
  63          --  as full expansion does, but this was removed as this prevents the
  64          --  verification back-end from using a short name for debugging and
  65          --  user interaction. The verification back-end already takes care
  66          --  of qualifying names when needed.
  67
  68          when N_Block_Statement     |
  69               N_Package_Body        |
  70               N_Package_Declaration |
  71               N_Subprogram_Body     =>
  72             Qualify_Entity_Names (N);
  73
  74          when N_Subprogram_Call     =>
  75             Expand_SPARK_Call (N);
  76
  77          when N_Expanded_Name |
  78               N_Identifier    =>
  79             Expand_Potential_Renaming (N);
  80
  81          when N_Object_Renaming_Declaration =>
  82             Expand_SPARK_N_Object_Renaming_Declaration (N);
  83
  84          --  In SPARK mode, no other constructs require expansion
  85
  86          when others =>
  87             null;
  88       end case;
  89    end Expand_SPARK;
  90
  91    -----------------------
  92    -- Expand_SPARK_Call --
  93    -----------------------
  94
  95    procedure Expand_SPARK_Call (N : Node_Id) is
  96    begin
  97       --  If the subprogram is a renaming, replace it in the call with the name
  98       --  of the actual subprogram being called. We distinguish renamings from
  99       --  inherited primitive operations, which both have an Alias component,
 100       --  by looking at the parent node of the entity. The entity for a
 101       --  renaming has the function or procedure specification node as
 102       --  parent, while an inherited primitive operation has the derived
 103       --  type declaration as parent.
 104
 105       if Nkind (Name (N)) in N_Has_Entity
 106         and then Present (Entity (Name (N)))
 107       then
 108          declare
 109             E : constant Entity_Id := Entity (Name (N));
 110          begin
 111             if Nkind_In (Parent (E), N_Function_Specification,
 112                                      N_Procedure_Specification)
 113               and then Present (Alias (E))
 114             then
 115                Set_Entity (Name (N), Ultimate_Alias (E));
 116             end if;
 117          end;
 118       end if;
 119    end Expand_SPARK_Call;
 120
 121    ------------------------------------------------
 122    -- Expand_SPARK_N_Object_Renaming_Declaration --
 123    ------------------------------------------------
 124
 125    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id) is
 126    begin
 127       --  Unconditionally remove all side effects from the name
 128
 129       Evaluate_Name (Name (N));
 130    end Expand_SPARK_N_Object_Renaming_Declaration;
 131
 132    -------------------------------
 133    -- Expand_Potential_Renaming --
 134    -------------------------------
 135
 136    procedure Expand_Potential_Renaming (N : Node_Id) is
 137       E : constant Entity_Id := Entity (N);
 138       T : constant Entity_Id := Etype (N);
 139
 140    begin
 141       --  Replace a reference to a renaming with the actual renamed object
 142
 143       if Ekind (E) in Object_Kind and then Present (Renamed_Object (E)) then
 144          Rewrite (N, New_Copy_Tree (Renamed_Object (E)));
 145          Reset_Analyzed_Flags (N);
 146          Analyze_And_Resolve (N, T);
 147       end if;
 148    end Expand_Potential_Renaming;
 149
 150 end Exp_SPARK;