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_Ch4;  use Exp_Ch4;
  29 with Exp_Ch6;  use Exp_Ch6;
  30 with Exp_Dbug; use Exp_Dbug;
  31 with Exp_Util; use Exp_Util;
  32 with Sem_Aux;  use Sem_Aux;
  33 with Sem_Res;  use Sem_Res;
  34 with Sem_Util; use Sem_Util;
  35 with Sinfo;    use Sinfo;
  36 with Stand;    use Stand;
  37
  38 package body Exp_SPARK is
  39
  40    -----------------------
  41    -- Local Subprograms --
  42    -----------------------
  43
  44    procedure Expand_SPARK_Call (N : Node_Id);
  45    --  This procedure contains common processing for function and procedure
  46    --  calls:
  47    --    * expansion of actuals to introduce necessary temporaries
  48    --    * replacement of renaming by subprogram renamed
  49
  50    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
  51    --  Perform name evaluation for a renamed object
  52
  53    procedure Expand_Potential_Renaming (N : Node_Id);
  54    --  N denotes a N_Identifier or N_Expanded_Name. If N references a renaming,
  55    --  replace N with the renamed object.
  56
  57    ------------------
  58    -- Expand_SPARK --
  59    ------------------
  60
  61    procedure Expand_SPARK (N : Node_Id) is
  62    begin
  63       case Nkind (N) is
  64
  65          --  Qualification of entity names in formal verification mode
  66          --  is limited to the addition of a suffix for homonyms (see
  67          --  Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names
  68          --  as full expansion does, but this was removed as this prevents the
  69          --  verification back-end from using a short name for debugging and
  70          --  user interaction. The verification back-end already takes care
  71          --  of qualifying names when needed.
  72
  73          when N_Block_Statement     |
  74               N_Package_Body        |
  75               N_Package_Declaration |
  76               N_Subprogram_Body     =>
  77             Qualify_Entity_Names (N);
  78
  79          when N_Subprogram_Call     =>
  80             Expand_SPARK_Call (N);
  81
  82          when N_Expanded_Name |
  83               N_Identifier    =>
  84             Expand_Potential_Renaming (N);
  85
  86          --  A NOT IN B gets transformed to NOT (A IN B). This is the same
  87          --  expansion used in the normal case, so shared the code.
  88
  89          when N_Not_In =>
  90             Expand_N_Not_In (N);
  91
  92          when N_Object_Renaming_Declaration =>
  93             Expand_SPARK_N_Object_Renaming_Declaration (N);
  94
  95          --  In SPARK mode, no other constructs require expansion
  96
  97          when others =>
  98             null;
  99       end case;
 100    end Expand_SPARK;
 101
 102    -----------------------
 103    -- Expand_SPARK_Call --
 104    -----------------------
 105
 106    procedure Expand_SPARK_Call (N : Node_Id) is
 107       Call_Node   : constant Node_Id := N;
 108       Parent_Subp : Entity_Id;
 109       Subp        : Entity_Id;
 110
 111    begin
 112       --  Ignore if previous error
 113
 114       if Nkind (Call_Node) in N_Has_Etype
 115         and then Etype (Call_Node) = Any_Type
 116       then
 117          return;
 118       end if;
 119
 120       --  Call using access to subprogram with explicit dereference
 121
 122       if Nkind (Name (Call_Node)) = N_Explicit_Dereference then
 123          Subp        := Etype (Name (Call_Node));
 124          Parent_Subp := Empty;
 125
 126       --  Case of call to simple entry, where the Name is a selected component
 127       --  whose prefix is the task, and whose selector name is the entry name
 128
 129       elsif Nkind (Name (Call_Node)) = N_Selected_Component then
 130          Subp        := Entity (Selector_Name (Name (Call_Node)));
 131          Parent_Subp := Empty;
 132
 133       --  Case of call to member of entry family, where Name is an indexed
 134       --  component, with the prefix being a selected component giving the
 135       --  task and entry family name, and the index being the entry index.
 136
 137       elsif Nkind (Name (Call_Node)) = N_Indexed_Component then
 138          Subp        := Entity (Selector_Name (Prefix (Name (Call_Node))));
 139          Parent_Subp := Empty;
 140
 141       --  Normal case
 142
 143       else
 144          Subp        := Entity (Name (Call_Node));
 145          Parent_Subp := Alias (Subp);
 146       end if;
 147
 148       --  Various expansion activities for actuals are carried out
 149
 150       Expand_Actuals (N, Subp);
 151
 152       --  If the subprogram is a renaming, replace it in the call with the name
 153       --  of the actual subprogram being called.
 154
 155       if Present (Parent_Subp) then
 156          Parent_Subp := Ultimate_Alias (Parent_Subp);
 157
 158          --  The below setting of Entity is suspect, see F109-018 discussion???
 159
 160          Set_Entity (Name (Call_Node), Parent_Subp);
 161       end if;
 162    end Expand_SPARK_Call;
 163
 164    ------------------------------------------------
 165    -- Expand_SPARK_N_Object_Renaming_Declaration --
 166    ------------------------------------------------
 167
 168    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id) is
 169    begin
 170       --  Unconditionally remove all side effects from the name
 171
 172       Evaluate_Name (Name (N));
 173    end Expand_SPARK_N_Object_Renaming_Declaration;
 174
 175    -------------------------------
 176    -- Expand_Potential_Renaming --
 177    -------------------------------
 178
 179    procedure Expand_Potential_Renaming (N : Node_Id) is
 180       E : constant Entity_Id := Entity (N);
 181       T : constant Entity_Id := Etype (N);
 182
 183    begin
 184       --  Replace a reference to a renaming with the actual renamed object
 185
 186       if Ekind (E) in Object_Kind and then Present (Renamed_Object (E)) then
 187          Rewrite (N, New_Copy_Tree (Renamed_Object (E)));
 188          Reset_Analyzed_Flags (N);
 189          Analyze_And_Resolve (N, T);
 190       end if;
 191    end Expand_Potential_Renaming;
 192
 193 end Exp_SPARK;