===================================================================
@@ -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
===================================================================
@@ -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.
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 <kirtchev@adacore.com> * sem_ch7.adb, sem_ch6.adb (Analyze_Subprogram_Body_Helper): Only source bodies should "freeze" the contract of the nearest enclosing package body.