===================================================================
@@ -544,35 +544,6 @@
-- Start of processing for Analyze_Package_Body_Helper
begin
- -- A [generic] package body "freezes" the contract of the nearest
- -- enclosing package body and all other contracts encountered in the
- -- same declarative part up to and excluding the package body:
-
- -- package body Nearest_Enclosing_Package
- -- with Refined_State => (State => Constit)
- -- is
- -- Constit : ...;
-
- -- package body Freezes_Enclosing_Package_Body
- -- with Refined_State => (State_2 => Constit_2)
- -- is
- -- Constit_2 : ...;
-
- -- procedure Proc
- -- with Refined_Depends => (Input => (Constit, Constit_2)) ...
-
- -- This ensures that any annotations referenced by the contract of a
- -- [generic] subprogram body declared within the current package body
- -- are available. This form of "freezing" is decoupled from the usual
- -- Freeze_xxx mechanism because it must also work in the context of
- -- generics where normal freezing is disabled.
-
- -- Only bodies coming from source should cause this type of "freezing"
-
- if Comes_From_Source (N) then
- Analyze_Previous_Contracts (N);
- end if;
-
-- Find corresponding package specification, and establish the current
-- scope. The visible defining entity for the package is the defining
-- occurrence in the spec. On exit from the package body, all body
@@ -628,6 +599,42 @@
end if;
end if;
+ -- A [generic] package body "freezes" the contract of the nearest
+ -- enclosing package body and all other contracts encountered in the
+ -- same declarative part up to and excluding the package body:
+
+ -- package body Nearest_Enclosing_Package
+ -- with Refined_State => (State => Constit)
+ -- is
+ -- Constit : ...;
+
+ -- package body Freezes_Enclosing_Package_Body
+ -- with Refined_State => (State_2 => Constit_2)
+ -- is
+ -- Constit_2 : ...;
+
+ -- procedure Proc
+ -- with Refined_Depends => (Input => (Constit, Constit_2)) ...
+
+ -- This ensures that any annotations referenced by the contract of a
+ -- [generic] subprogram body declared within the current package body
+ -- are available. This form of "freezing" is decoupled from the usual
+ -- Freeze_xxx mechanism because it must also work in the context of
+ -- generics where normal freezing is disabled.
+
+ -- Only bodies coming from source should cause this type of "freezing".
+ -- Instantiated generic bodies are excluded because their processing is
+ -- performed in a separate compilation pass which lacks enough semantic
+ -- information with respect to contract analysis. It is safe to suppress
+ -- the "freezing" of contracts in this case because this action already
+ -- took place at the end of the enclosing declarative part.
+
+ if Comes_From_Source (N)
+ and then not Is_Generic_Instance (Spec_Id)
+ then
+ Analyze_Previous_Contracts (N);
+ end if;
+
-- A package body is Ghost when the corresponding spec is Ghost. Set
-- the mode now to ensure that any nodes generated during analysis and
-- expansion are properly flagged as ignored Ghost.
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.