This patch suppresses the transformation of references to renamings into
references to renamed names when the reference appears within a pragma of
no significance to SPARK.
------------
-- Source --
------------
-- uname.adb
procedure Uname is
type Bounded_String is record
Length : Natural;
end record;
Global_Name_Buffer : Bounded_String := (Length => 0);
Right_Length : Natural renames Global_Name_Buffer.Length;
begin
pragma Warnings (Off, Right_Length);
pragma Assert (Right_Length = 0);
end Uname;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c -gnatdg -gnatd.F uname.adb
with system;
procedure uname is
type bounded_string is record
length : natural;
end record;
freeze bounded_string []
global_name_buffer : bounded_string := (
length => 0);
right_length : natural renames global_name_buffer.length;
begin
pragma warnings (off, right_length);
pragma check (assert, global_name_buffer.length = 0);
null;
end uname;
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-09-25 Hristian Kirtchev <kirtc...@adacore.com>
* exp_spark.adb (Expand_SPARK_Potential_Renaming): Do not process a
reference when it appears within a pragma of no significance to SPARK.
(In_Insignificant_Pragma): New routine.
* sem_prag.ads: Add new table Pragma_Significant_In_SPARK.
Index: sem_prag.ads
===================================================================
--- sem_prag.ads (revision 253134)
+++ sem_prag.ads (working copy)
@@ -175,6 +175,25 @@
Pragma_Warnings => True,
others => False);
+ -- The following table lists all pragmas which are significant in SPARK and
+ -- as a result get translated into verification conditions. The table is an
+ -- amalgamation of the pragmas listed in SPARK RM 16.1 and internally added
+ -- entries.
+
+ Pragma_Significant_In_SPARK : constant array (Pragma_Id) of Boolean :=
+ (Pragma_All_Calls_Remote => False,
+ Pragma_Asynchronous => False,
+ Pragma_Default_Storage_Pool => False,
+ Pragma_Discard_Names => False,
+ Pragma_Dispatching_Domain => False,
+ Pragma_Priority_Specific_Dispatching => False,
+ Pragma_Remote_Call_Interface => False,
+ Pragma_Remote_Types => False,
+ Pragma_Shared_Passive => False,
+ Pragma_Task_Dispatching_Policy => False,
+ Pragma_Warnings => False,
+ others => True);
+
-----------------
-- Subprograms --
-----------------
Index: exp_spark.adb
===================================================================
--- exp_spark.adb (revision 253134)
+++ exp_spark.adb (working copy)
@@ -36,6 +36,7 @@
with Rtsfind; use Rtsfind;
with Sem; use Sem;
with Sem_Eval; use Sem_Eval;
+with Sem_Prag; use Sem_Prag;
with Sem_Res; use Sem_Res;
with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo;
@@ -368,11 +369,46 @@
-------------------------------------
procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is
+ function In_Insignificant_Pragma (Nod : Node_Id) return Boolean;
+ -- Determine whether arbitrary node Nod appears within a significant
+ -- pragma for SPARK.
+
+ -----------------------------
+ -- In_Insignificant_Pragma --
+ -----------------------------
+
+ function In_Insignificant_Pragma (Nod : Node_Id) return Boolean is
+ Par : Node_Id;
+
+ begin
+ -- Climb the parent chain looking for an enclosing pragma
+
+ Par := Nod;
+ while Present (Par) loop
+ if Nkind (Par) = N_Pragma then
+ return not Pragma_Significant_In_SPARK (Get_Pragma_Id (Par));
+
+ -- Prevent the search from going too far
+
+ elsif Is_Body_Or_Package_Declaration (Par) then
+ exit;
+ end if;
+
+ Par := Parent (Par);
+ end loop;
+
+ return False;
+ end In_Insignificant_Pragma;
+
+ -- Local variables
+
Loc : constant Source_Ptr := Sloc (N);
Obj_Id : constant Entity_Id := Entity (N);
Typ : constant Entity_Id := Etype (N);
Ren : Node_Id;
+ -- Start of processing for Expand_SPARK_Potential_Renaming
+
begin
-- Replace a reference to a renaming with the actual renamed object
@@ -381,12 +417,20 @@
if Present (Ren) then
+ -- Do not process a reference when it appears within a pragma of
+ -- no significance to SPARK. It is assumed that the replacement
+ -- will violate the semantics of the pragma and cause a spurious
+ -- error.
+
+ if In_Insignificant_Pragma (N) then
+ return;
+
-- Instantiations and inlining of subprograms employ "prologues"
-- which map actual to formal parameters by means of renamings.
-- Replace a reference to a formal by the corresponding actual
-- parameter.
- if Nkind (Ren) in N_Entity then
+ elsif Nkind (Ren) in N_Entity then
Rewrite (N, New_Occurrence_Of (Ren, Loc));
-- Otherwise the renamed object denotes a name
