[Ada] Freezing of contracts, Part_Of and current instance of a concurrent type

[Arnaud Charlet <charlet at adacore dot com>]

This patch addresses several areas:

The freezing of contracts has been enhanced. A body continues to freeze the
contract of the nearest enclosing package and now freezes the contracts of
all eligible constructs in the same declarative list that precede the body.

A concurrent constituent is no longer considered a visible state of a package
body because it is already part of a single protected/task type.

The current instance of a concurrent type now correctly includes single
protected/task types. As a result, the current instance of such a type will
appear as an implicit formal parameter of a protected subprogram or a single
task type as per SPARK RM 6.1.4.

------------
-- Source --
------------

--  subprogram_freezing.ads

package Subprogram_Freezing with SPARK_Mode is
   procedure Force_Freeze;
end Subprogram_Freezing;

--  subprogram_freezing.adb

package body Subprogram_Freezing with SPARK_Mode is
   function Func (Formal : Integer) return Integer
     with Contract_Cases =>
            (Var + Formal = 1 => Var + Func'Result = 0,              --  Error
             others           => Var - Func'Result = 1),             --  Error
          Pre            => (Var > 2),                               --  Error
          Post           => (Var + Func'Result = 100);               --  Error

   procedure Force_Freeze is begin null; end Force_Freeze;

   Var : Integer := 1;

   function Func (Formal : Integer) return Integer is
   begin return Formal; end Func;
end Subprogram_Freezing;

--  variable_freezing.ads

package Variable_Freezing with SPARK_Mode is
   procedure Force_Freeze;
end Variable_Freezing;

--  variable_freezing.adb

package body Variable_Freezing with SPARK_Mode is
   Error_1 : Integer := 1 with Part_Of => Prot;                      --  Error

   procedure Force_Freeze is begin null; end Force_Freeze;

   protected Prot is
   end Prot;

   protected body Prot is
   end Prot;
end Variable_Freezing;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c subprogram_freezing.adb
$ gcc -c variable_freezing.adb
subprogram_freezing.adb:2:13: body "Force_Freeze" declared at line 9 freezes
  the contract of "Func"
subprogram_freezing.adb:2:13: all contractual items must be declared before
  body at line 9
subprogram_freezing.adb:6:30: "Var" is undefined (more references follow)
variable_freezing.adb:2:04: body "Force_Freeze" declared at line 4 freezes the
  contract of "Error_1"
variable_freezing.adb:2:04: all contractual items must be declared before body
  at line 4
variable_freezing.adb:2:43: "Prot" is undefined

Tested on x86_64-pc-linux-gnu, committed on trunk

2015-11-18  Hristian Kirtchev  <kirtchev@adacore.com>

	* contracts.adb (Analyze_Contracts): New routine.
	(Analyze_Enclosing_Package_Body_Contract): Removed.
	(Analyze_Entry_Or_Subprogram_Contract): Add formal parameter
	Freeze_Id.  Propagate the entity of the freezing body to vaious
	analysis routines.
	(Analyze_Initial_Declaration_Contract): Removed.
	(Analyze_Object_Contract): Add formal parameter
	Freeze_Id. Propagate the entity of the freezing body to vaious
	analysis routines.
	(Analyze_Previous_Contracts): New routine.
	* contracts.ads (Analyze_Enclosing_Package_Body_Contract): Removed.
	(Analyze_Contracts): New routine.
	(Analyze_Entry_Or_Subprogram_Contract): Add formal
	parameter Freeze_Id and update the comment on usage.
	(Analyze_Initial_Declaration_Contract): Removed.
	(Analyze_Object_Contract): Add formal parameter Freeze_Id and
	update the comment on usage.
	(Analyze_Previous_Contracts): New routine.
	* sem_ch3.adb (Analyze_Declarations): Use Analyze_Contracts to
	analyze all contracts of eligible constructs.
	* sem_ch6.adb (Analyze_Generic_Subprogram_Body):
	A body no longer freezes the contract of its initial
	declaration. This effect is achieved through different means.
	(Analyze_Subprogram_Body_Helper): A body now freezes the contracts
	of all eligible constructs that precede it. A body no longer
	freezes the contract of its initial declaration. This effect is
	achieved through different means.
	* sem_ch7.adb (Analyze_Package_Body_Helper): A body now freezes
	the contracts of all eligible constructs that precede it. A body
	no longer freezes the contract of its initial declaration. This
	effect is achieved through different means.
	* sem_ch9.adb (Analyze_Entry_Body): A body now freezes
	the contracts of all eligible constructs that precede
	it. A body no longer freezes the contract of its initial
	declaration. This effect is achieved through different means.
	(Analyze_Protected_Body): A body now freezes the contracts
	of all eligible constructs that precede it. A body no longer
	freezes the contract of its initial declaration. This effect
	is achieved through different means.
	(Analyze_Task_Body): A
	body now freezes the contracts of all eligible constructs that
	precede it. A body no longer freezes the contract of its initial
	declaration. This effect is achieved through different means.
	* sem_prag.adb (Add_Item_To_Name_Buffer): Single protected/task
	objects now output their respective current instance of xxx
	type messages.	(Analyze_Contract_Cases_In_Decl_Part): Add
	formal parameter Freeze_Id. Emit a clarification message
	when an undefined entity may the byproduct of contract
	freezing.
	(Analyze_Part_Of_In_Decl_Part): Add formal
	parameter Freeze_Id. Emit a clarification message when an
	undefined entity may the byproduct of contract freezing.
	(Analyze_Pre_Post_Condition_In_Decl_Part): Add formal
	parameter Freeze_Id. Emit a clarification message when an
	undefined entity may the byproduct of contract freezing.
	(Analyze_Refined_State_In_Decl_Part): Do not report unused body
	states as constituents of single protected/task types may not
	bave been identified yet.
	(Collect_Subprogram_Inputs_Outputs):
	Reimplemented.	(Contract_Freeze_Error): New routine.
	(Process_Overloadable): Use predicate Is_Single_Task_Object.
	* sem_prag.ads (Analyze_Contract_Cases_In_Decl_Part):
	Add formal parameter Freeze_Id and update the comment
	on usage.
	(Analyze_Part_Of_In_Decl_Part): Add formal
	parameter Freeze_Id and update the comment on usage.
	(Analyze_Pre_Post_Condition_In_Decl_Part): Add formal parameter
	Freeze_Id and update the comment on usage.
	* sem_util.adb (Check_Unused_Body_States): Remove global
	variable Legal_Constits. The routine now reports unused
	body states regardless of whether constituents are
	legal or not.
	(Collect_Body_States): A constituent of a
	single protected/task type is not a visible state of a
	package body.
	(Collect_Visible_States): A constituent
	of a single protected/task type is not a visible
	state of a package body.
	(Has_Undefined_Reference): New routine.
	(Is_Single_Concurrent_Object): Reimplemented.
	(Is_Single_Protected_Object): New routine.
	(Is_Single_Task_Object): New routine.
	(Is_Visible_Object): New routine.
	(Report_Unused_Body_States): Moved to Check_Unused_Body_States.
	* sem_util.ads (Check_Unused_Body_States): Update the comment on usage.
	(Has_Undefined_Reference): New routine.
	(Is_Single_Protected_Object): New routine.
	(Is_Single_Task_Object): New routine.
	(Report_Unused_Body_States): Moved to Check_Unused_Body_States.

Attachment: difs
Description: Text document