[Ada] Expression functions, internal bodies and freezing of contracts

[Arnaud Charlet <charlet at adacore dot com>]

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.

Attachment: difs
Description: Text document