[Ada] Crash on access-to-object in SPARK

[Pierre-Marie de Rodat <derodat at adacore dot com>]

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.

Attachment: difs
Description: Text document