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 <kirtc...@adacore.com>
* sem_ch7.adb (Analyze_Package_Body_Helper): The body of an
instantiated package should not cause freezing of previous contracts.
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb (revision 235481)
+++ sem_ch7.adb (working copy)
@@ -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.
