This patch corrects the light expansion of object renamings for SPARK to
prevent a crash by querying the subtype mark when the renaming carries an
access definition.
-------------
-- Sources --
-------------
-- p.ads
package P with SPARK_Mode is
type T is record
Ptr : access constant Integer;
end record;
function Get (X : T) return Integer;
end P;
-- p.adb
package body P with SPARK_Mode is
function Get (X : T) return Integer is
Proxy : access constant Integer renames X.Ptr;
begin
return Proxy.all;
end;
end P;
-----------------
-- Compilation --
-----------------
$ gcc -c p.adb
$ gcc -c p.adb -gnatd.F
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-11-08 Hristian Kirtchev <kirtc...@adacore.com>
* exp_spark.adb (Expand_SPARK_N_Object_Renaming_Declaration): Obtain
the type of the renaming from its defining entity, rather then the
subtype mark as there may not be a subtype mark.
Index: exp_spark.adb
===================================================================
--- exp_spark.adb (revision 254542)
+++ exp_spark.adb (working copy)
@@ -349,7 +349,7 @@
Loc : constant Source_Ptr := Sloc (N);
Obj_Id : constant Entity_Id := Defining_Entity (N);
Nam : constant Node_Id := Name (N);
- Typ : constant Entity_Id := Etype (Subtype_Mark (N));
+ Typ : constant Entity_Id := Etype (Obj_Id);
begin
-- Transform a renaming of the form
