| Message ID | 20171108173239.GA27934@adacore.com |
|---|---|
| State | New |
| Headers | show |
| Series | [Ada] Crash on access-to-object in SPARK | expand |
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
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 <kirtchev@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.