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