[Ada] Spurious error on variable in private child package body

[Arnaud Charlet <charlet at adacore dot com>]

This patch modifies the contract freezing mechanism to suppress freezing when
the trigger is the body of an instantiated package. This effectively prevents
a spurious attempt to freeze because a) the body instantiation pass does not
have all semantic information and b) freezing has already taken place.

------------
-- Source --
------------

--  gp.ads

generic
   type T is private;

package GP with
   SPARK_Mode => On,
   Elaborate_Body,
   Abstract_State => (State,
                      (Atomic_State with External))
is
end GP;

--  gp.adb

package body GP with
   SPARK_Mode => On,
   Refined_State => (State        => GG1,
                     Atomic_State => GG2)
is
   GG1 : T;
   GG2 : T with Volatile;
end GP;

--  base.ads

package Base with
   SPARK_Mode => On
is
end Base;

--  base-a.ads

package Base.A with
   SPARK_Mode => On,
   Elaborate_Body,
   Abstract_State => (State,
                      (Atomic_State with External))
is
end Base.A;

--  base-a.adb

with Base.A.B;

package body Base.A with
   SPARK_Mode => On,
   Refined_State => (State        => Base.A.B.State,
                     Atomic_State => Base.A.B.Atomic_State)
is
end Base.A;

--  base-a-b.ads

private package Base.A.B with
   SPARK_Mode => On,
   Elaborate_Body,
   Abstract_State =>
     ((State        with           Part_Of => Base.A.State),
      (Atomic_State with External, Part_Of => Base.A.Atomic_State))
is
end Base.A.B;

--  base-a-b.adb

with GP; pragma Elaborate_All (GP);

package body Base.A.B with
   SPARK_Mode => On,
   Refined_State =>
     (State        => (G1, P.State),
      Atomic_State => P.Atomic_State)
is
   G1 : Boolean := False;

   package P is new GP (T => Boolean);
end Base.A.B;

-----------------
-- Compilation --
-----------------

$ gcc -c base-a-b.adb

Tested on x86_64-pc-linux-gnu, committed on trunk

2016-04-27  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch7.adb (Analyze_Package_Body_Helper): The body of an
	instantiated package should not cause freezing of previous contracts.

Attachment: difs
Description: Text document