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 <[email protected]>
* 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.
Index: exp_spark.adb
===================================================================
--- exp_spark.adb (revision 235481)
+++ exp_spark.adb (working copy)
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
+-- 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;
Index: exp_spark.ads
===================================================================
--- exp_spark.ads (revision 235481)
+++ exp_spark.ads (working copy)
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
--- Copyright (C) 2011-2013, Free Software Foundation, Inc. --
+-- 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;
Index: sem.adb
===================================================================
--- sem.adb (revision 235481)
+++ sem.adb (working copy)
@@ -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;
