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-2015, 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_Ch5;  use Exp_Ch5;
  29 with Exp_Dbug; use Exp_Dbug;
  30 with Exp_Util; use Exp_Util;
  31 with Sem_Res;  use Sem_Res;
  32 with Sem_Util; use Sem_Util;
  33 with Sinfo;    use Sinfo;
  34 with Tbuild;   use Tbuild;
  35
  36 package body Exp_SPARK is
  37
  38    -----------------------
  39    -- Local Subprograms --
  40    -----------------------
  41
  42    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
  43    --  Perform name evaluation for a renamed object
  44
  45    procedure Expand_Potential_Renaming (N : Node_Id);
  46    --  N denotes a N_Identifier or N_Expanded_Name. If N references a renaming,
  47    --  replace N with the renamed object.
  48
  49    ------------------
  50    -- Expand_SPARK --
  51    ------------------
  52
  53    procedure Expand_SPARK (N : Node_Id) is
  54    begin
  55       case Nkind (N) is
  56
  57          --  Qualification of entity names in formal verification mode
  58          --  is limited to the addition of a suffix for homonyms (see
  59          --  Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names
  60          --  as full expansion does, but this was removed as this prevents the
  61          --  verification back-end from using a short name for debugging and
  62          --  user interaction. The verification back-end already takes care
  63          --  of qualifying names when needed.
  64
  65          when N_Block_Statement     |
  66               N_Package_Body        |
  67               N_Package_Declaration |
  68               N_Subprogram_Body     =>
  69             Qualify_Entity_Names (N);
  70
  71          when N_Expanded_Name |
  72               N_Identifier    =>
  73             Expand_Potential_Renaming (N);
  74
  75          when N_Object_Renaming_Declaration =>
  76             Expand_SPARK_N_Object_Renaming_Declaration (N);
  77
  78          --  Loop iterations over arrays need to be expanded, to avoid getting
  79          --  two names referring to the same object in memory (the array and
  80          --  the iterator) in GNATprove, especially since both can be written
  81          --  (thus possibly leading to interferences due to aliasing). No such
  82          --  problem arises with quantified expressions over arrays, which are
  83          --  dealt with specially in GNATprove.
  84
  85          when N_Loop_Statement =>
  86             declare
  87                Scheme : constant Node_Id := Iteration_Scheme (N);
  88             begin
  89                if Present (Scheme)
  90                  and then Present (Iterator_Specification (Scheme))
  91                  and then
  92                    Is_Iterator_Over_Array (Iterator_Specification (Scheme))
  93                then
  94                   Expand_Iterator_Loop_Over_Array (N);
  95                end if;
  96             end;
  97
  98          --  In SPARK mode, no other constructs require expansion
  99
 100          when others =>
 101             null;
 102       end case;
 103    end Expand_SPARK;
 104
 105    ------------------------------------------------
 106    -- Expand_SPARK_N_Object_Renaming_Declaration --
 107    ------------------------------------------------
 108
 109    procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id) is
 110    begin
 111       --  Unconditionally remove all side effects from the name
 112
 113       Evaluate_Name (Name (N));
 114    end Expand_SPARK_N_Object_Renaming_Declaration;
 115
 116    -------------------------------
 117    -- Expand_Potential_Renaming --
 118    -------------------------------
 119
 120    procedure Expand_Potential_Renaming (N : Node_Id) is
 121       Id     : constant Entity_Id  := Entity (N);
 122       Loc    : constant Source_Ptr := Sloc (N);
 123       Typ    : constant Entity_Id  := Etype (N);
 124       Ren_Id : Node_Id;
 125
 126    begin
 127       --  Replace a reference to a renaming with the actual renamed object
 128
 129       if Ekind (Id) in Object_Kind then
 130          Ren_Id := Renamed_Object (Id);
 131
 132          if Present (Ren_Id) then
 133
 134             --  The renamed object is an entity when instantiating generics
 135             --  or inlining bodies. In this case the renaming is part of the
 136             --  mapping "prologue" which links actuals to formals.
 137
 138             if Nkind (Ren_Id) in N_Entity then
 139                Rewrite (N, New_Occurrence_Of (Ren_Id, Loc));
 140
 141             --  Otherwise the renamed object denotes a name
 142
 143             else
 144                Rewrite (N, New_Copy_Tree (Ren_Id));
 145                Reset_Analyzed_Flags (N);
 146             end if;
 147
 148             Analyze_And_Resolve (N, Typ);
 149          end if;
 150       end if;
 151    end Expand_Potential_Renaming;
 152
 153 end Exp_SPARK;