===================================================================
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
+-- Copyright (C) 1992-2016, 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- --
@@ -42,10 +42,6 @@
procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
-- Perform name evaluation for a renamed object
- procedure Expand_Potential_Renaming (N : Node_Id);
- -- N denotes a N_Identifier or N_Expanded_Name. If N references a renaming,
- -- replace N with the renamed object.
-
------------------
-- Expand_SPARK --
------------------
@@ -73,7 +69,7 @@
when N_Expanded_Name |
N_Identifier =>
- Expand_Potential_Renaming (N);
+ Expand_SPARK_Potential_Renaming (N);
when N_Object_Renaming_Declaration =>
Expand_SPARK_N_Object_Renaming_Declaration (N);
@@ -116,41 +112,41 @@
Evaluate_Name (Name (N));
end Expand_SPARK_N_Object_Renaming_Declaration;
- -------------------------------
- -- Expand_Potential_Renaming --
- -------------------------------
+ -------------------------------------
+ -- Expand_SPARK_Potential_Renaming --
+ -------------------------------------
- procedure Expand_Potential_Renaming (N : Node_Id) is
- Id : constant Entity_Id := Entity (N);
+ procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is
Loc : constant Source_Ptr := Sloc (N);
+ Ren_Id : constant Entity_Id := Entity (N);
Typ : constant Entity_Id := Etype (N);
- Ren_Id : Node_Id;
+ Obj_Id : Node_Id;
begin
-- Replace a reference to a renaming with the actual renamed object
- if Ekind (Id) in Object_Kind then
- Ren_Id := Renamed_Object (Id);
+ if Ekind (Ren_Id) in Object_Kind then
+ Obj_Id := Renamed_Object (Ren_Id);
- if Present (Ren_Id) then
+ if Present (Obj_Id) then
-- The renamed object is an entity when instantiating generics
-- or inlining bodies. In this case the renaming is part of the
-- mapping "prologue" which links actuals to formals.
- if Nkind (Ren_Id) in N_Entity then
- Rewrite (N, New_Occurrence_Of (Ren_Id, Loc));
+ if Nkind (Obj_Id) in N_Entity then
+ Rewrite (N, New_Occurrence_Of (Obj_Id, Loc));
-- Otherwise the renamed object denotes a name
else
- Rewrite (N, New_Copy_Tree (Ren_Id));
+ Rewrite (N, New_Copy_Tree (Obj_Id));
Reset_Analyzed_Flags (N);
end if;
Analyze_And_Resolve (N, Typ);
end if;
end if;
- end Expand_Potential_Renaming;
+ end Expand_SPARK_Potential_Renaming;
end Exp_SPARK;
===================================================================
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
+-- Copyright (C) 2011-2016, 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- --
@@ -35,4 +35,8 @@
procedure Expand_SPARK (N : Node_Id);
+ procedure Expand_SPARK_Potential_Renaming (N : Node_Id);
+ -- N must denote an N_Expanded_Name or N_Identifier. If N is a reference to
+ -- a renaming, replace N with the renamed object.
+
end Exp_SPARK;
===================================================================
@@ -23,39 +23,40 @@
-- --
------------------------------------------------------------------------------
-with Atree; use Atree;
-with Debug; use Debug;
-with Debug_A; use Debug_A;
-with Elists; use Elists;
-with Expander; use Expander;
-with Fname; use Fname;
-with Ghost; use Ghost;
-with Lib; use Lib;
-with Lib.Load; use Lib.Load;
-with Nlists; use Nlists;
-with Output; use Output;
-with Restrict; use Restrict;
-with Sem_Attr; use Sem_Attr;
-with Sem_Aux; use Sem_Aux;
-with Sem_Ch2; use Sem_Ch2;
-with Sem_Ch3; use Sem_Ch3;
-with Sem_Ch4; use Sem_Ch4;
-with Sem_Ch5; use Sem_Ch5;
-with Sem_Ch6; use Sem_Ch6;
-with Sem_Ch7; use Sem_Ch7;
-with Sem_Ch8; use Sem_Ch8;
-with Sem_Ch9; use Sem_Ch9;
-with Sem_Ch10; use Sem_Ch10;
-with Sem_Ch11; use Sem_Ch11;
-with Sem_Ch12; use Sem_Ch12;
-with Sem_Ch13; use Sem_Ch13;
-with Sem_Prag; use Sem_Prag;
-with Sem_Util; use Sem_Util;
-with Sinfo; use Sinfo;
-with Stand; use Stand;
-with Stylesw; use Stylesw;
-with Uintp; use Uintp;
-with Uname; use Uname;
+with Atree; use Atree;
+with Debug; use Debug;
+with Debug_A; use Debug_A;
+with Elists; use Elists;
+with Exp_SPARK; use Exp_SPARK;
+with Expander; use Expander;
+with Fname; use Fname;
+with Ghost; use Ghost;
+with Lib; use Lib;
+with Lib.Load; use Lib.Load;
+with Nlists; use Nlists;
+with Output; use Output;
+with Restrict; use Restrict;
+with Sem_Attr; use Sem_Attr;
+with Sem_Aux; use Sem_Aux;
+with Sem_Ch2; use Sem_Ch2;
+with Sem_Ch3; use Sem_Ch3;
+with Sem_Ch4; use Sem_Ch4;
+with Sem_Ch5; use Sem_Ch5;
+with Sem_Ch6; use Sem_Ch6;
+with Sem_Ch7; use Sem_Ch7;
+with Sem_Ch8; use Sem_Ch8;
+with Sem_Ch9; use Sem_Ch9;
+with Sem_Ch10; use Sem_Ch10;
+with Sem_Ch11; use Sem_Ch11;
+with Sem_Ch12; use Sem_Ch12;
+with Sem_Ch13; use Sem_Ch13;
+with Sem_Prag; use Sem_Prag;
+with Sem_Util; use Sem_Util;
+with Sinfo; use Sinfo;
+with Stand; use Stand;
+with Stylesw; use Stylesw;
+with Uintp; use Uintp;
+with Uname; use Uname;
with Unchecked_Deallocation;
@@ -726,6 +727,21 @@
and then Etype (N) = Standard_Void_Type)
then
Expand (N);
+
+ -- Replace a reference to a renaming with the renamed object for SPARK.
+ -- In general this modification is performed by Expand_SPARK, however
+ -- certain constructs may not reach the resolution or expansion phase
+ -- and thus remain unchanged. The replacement is not performed when the
+ -- construct is overloaded as resolution must first take place. This is
+ -- also not done when analyzing a generic to preserve the original tree
+ -- and because the reference may become overloaded in the instance.
+
+ elsif GNATprove_Mode
+ and then Nkind_In (N, N_Expanded_Name, N_Identifier)
+ and then not Is_Overloaded (N)
+ and then not Inside_A_Generic
+ then
+ Expand_SPARK_Potential_Renaming (N);
end if;
Ghost_Mode := Save_Ghost_Mode;
This patch implements a mechanism for handling of renamings in SPARK. Since SPARK cannot handle this form of aliasing, a reference to a renamed object is replaced by a reference to the object itself. ------------ -- Source -- ------------ -- regpat.ads package Regpat is type Program_Data is array (Integer range <>) of Character; type Pattern_Matcher is record Program : Program_Data (1 .. 16) := (others => ASCII.NUL); end record; procedure Match (Self : in out Pattern_Matcher); end Regpat; -- regpat.adb package body Regpat is type Opcode is (BRANCH); function "=" (Left : Character; Right : Opcode) return Boolean is begin return Character'Pos (Left) = Opcode'Pos (Right); end "="; procedure Match (Self : in out Pattern_Matcher) is Short_Program : Program_Data renames Self.Program; begin Short_Program (1) := ASCII.NUL; pragma Assert (Short_Program (1) /= BRANCH); end Match; end Regpat; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c -gnatD -gnatd.F regpat.adb > regpat.dg $ grep "self.program" regpat.dg | wc -l 3 Tested on x86_64-pc-linux-gnu, committed on trunk 2016-04-27 Hristian Kirtchev <kirtchev@adacore.com> * exp_spark.adb (Expand_Potential_Renaming): Removed. (Expand_SPARK): Update the call to expand a potential renaming. (Expand_SPARK_Potential_Renaming): New routine. * exp_spark.ads (Expand_SPARK_Potential_Renaming): New routine. * sem.adb Add with and use clauses for Exp_SPARK. (Analyze): Expand a non-overloaded potential renaming for SPARK.