This patch ensures that only source package and subprogram bodies "freeze" the
contract of the nearest enclosing package body.
------------
-- Source --
------------
-- expr_funcs.ads
package Expr_Funcs
with SPARK_Mode,
Abstract_State => State
is
Var_1 : Integer := 1;
function In_Spec return Boolean is (Var_1 = 1)
with Global => (Input => (State, Var_1));
-- Does not freeze
function Spec_And_Body return Boolean
with Global => (Input => (State, Var_2));
-- See body
Var_2 : Integer := 2;
end Expr_Funcs;
-- expr_funcs.adb
package body Expr_Funcs
with SPARK_Mode,
Refined_State => (State => (Constit_1, Constit_2)) -- Error
is
Constit_1 : Integer := 1;
function In_Body return Boolean is (Constit_1 = 1)
with Global => (Input => Constit_1);
-- Does not freeze
package Nested_Expr_Funcs is
function Nested_In_Spec return Boolean is (Constit_1 = 1)
with Global => (Input => Constit_1);
-- Does not freeze
end Nested_Expr_Funcs;
function Spec_And_Body return Boolean is (Constit_1 = 1)
with Refined_Global => (Input => Constit_1);
-- Freezes because it acts as a completion. As a result Constit_2 in
-- Refined_State appears as undefined.
Constit_2 : Integer := 2;
end Expr_Funcs;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c expr_funcs.adb
expr_funcs.adb:1:14: body of package "Expr_Funcs" has unused hidden states
expr_funcs.adb:1:14: variable "Constit_2" defined at line 22
expr_funcs.adb:3:08: body "Spec_And_Body" declared at line 17 freezes the
contract of "Expr_Funcs"
expr_funcs.adb:3:08: all constituents must be declared before body at line 17
expr_funcs.adb:3:47: "Constit_2" is undefined
Tested on x86_64-pc-linux-gnu, committed on trunk
2015-10-26 Hristian Kirtchev <[email protected]>
* sem_ch7.adb, sem_ch6.adb (Analyze_Subprogram_Body_Helper): Only source
bodies should "freeze" the contract of the nearest enclosing
package body.
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb (revision 229313)
+++ sem_ch7.adb (working copy)
@@ -564,8 +564,12 @@
-- Freeze_xxx mechanism because it must also work in the context of
-- generics where normal freezing is disabled.
- Analyze_Enclosing_Package_Body_Contract (N);
+ -- Only bodies coming from source should cause this type of "freezing"
+ if Comes_From_Source (N) then
+ Analyze_Enclosing_Package_Body_Contract (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
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 229313)
+++ sem_ch6.adb (working copy)
@@ -3011,8 +3011,15 @@
-- decoupled from the usual Freeze_xxx mechanism because it must also
-- work in the context of generics where normal freezing is disabled.
- Analyze_Enclosing_Package_Body_Contract (N);
+ -- Only bodies coming from source should cause this type of "freezing".
+ -- Expression functions that act as bodies and complete an initial
+ -- declaration must be included in this category, hence the use of
+ -- Original_Node.
+ if Comes_From_Source (Original_Node (N)) then
+ Analyze_Enclosing_Package_Body_Contract (N);
+ end if;
+
-- Generic subprograms are handled separately. They always have a
-- generic specification. Determine whether current scope has a
-- previous declaration.
