[Ada] Detection of missing abstract state refinement

[Arnaud Charlet <charlet at adacore dot com>]

This patch implements a mechanism which detects missing refinement of abstract
states depending on whether a package requires a completing body or not. The
patch also cleans up the two entity lists used to store refinement and Part_Of
constituents of abstract states.

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

--  lib_pack_1.ads

package Lib_Pack_1
  with SPARK_Mode,
       Abstract_State => Error_State_1                               --  Error
is
   package Nested_1
     with Abstract_State => Error_State_2                            --  Error
   is
   end Nested_1;
end Lib_Pack_1;

--  lib_pack_2.ads

package Lib_Pack_2
  with SPARK_Mode,
       Abstract_State => OK_1
is
   package Nested_1
     with Abstract_State => Error_1                                  --  Error
   is
   end Nested_1;

   package Nested_2
     with Abstract_State => OK_2
   is
   end Nested_2;

   package Nested_3
     with Abstract_State => Error_2                                  --  Error
   is
   end Nested_3;

   procedure Force_Body;
end Lib_Pack_2;

--  lib_pack_2.adb

package body Lib_Pack_2
   with SPARK_Mode,
        Refined_State => (OK_1 => null)
is
   package body Nested_1 is
   end Nested_1;

   package body Nested_2
     with Refined_State => (OK_2 => null)
   is
   end Nested_2;

   --  package body Nested_3 is missing

   procedure Force_Body is begin null; end Force_Body;
end Lib_Pack_2;

--  non_lib_pack.ads

package Non_Lib_Pack with SPARK_Mode is
   procedure Force_Body;
end Non_Lib_Pack;

--  non_lib_pack.adb

package body Non_Lib_Pack with SPARK_Mode is
   procedure Force_Body is
      package Nested_1
        with Abstract_State => Error_1                               --  Error
      is
      end Nested_1;

      package body Nested_1 is
      end Nested_1;

      package Nested_2
        with Abstract_State => OK_1
      is
      end Nested_2;

      package body Nested_2
        with Refined_State => (OK_1 => null)                         --  OK
      is
      end Nested_2;

      package Nested_3
        with Abstract_State => Error_2                               --  Error
      is
      end Nested_3;

      --  package body Nested_3 is missing
   begin
      null;
   end Force_Body;
end Non_Lib_Pack;

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

$ gcc -c lib_pack_1.ads
$ gcc -c lib_pack_2.adb
$ gcc -c non_lib_pack.adb
lib_pack_1.ads:3:26: state "Error_State_1" requires refinement
lib_pack_1.ads:6:29: state "Error_State_2" requires refinement
lib_pack_2.ads:6:29: state "Error_1" requires refinement
lib_pack_2.ads:16:29: state "Error_2" requires refinement
non_lib_pack.adb:4:32: state "Error_1" requires refinement
non_lib_pack.adb:22:32: state "Error_2" requires refinement

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

2016-04-21  Hristian Kirtchev  <kirtchev@adacore.com>

	* contracts.adb (Analyze_Package_Body_Contract): Do not check
	for a missing package refinement because 1) packages do not have
	"refinement" and 2) the check for proper state refinement is
	performed in a different place.
	* einfo.adb (Has_Non_Null_Visible_Refinement): Reimplemented.
	(Has_Null_Visible_Refinement): Reimplemented.
	* sem_ch3.adb (Analyze_Declarations): Determine whether all
	abstract states have received a refinement and if not, emit
	errors.
	* sem_ch7.adb (Analyze_Package_Declaration): Code
	cleanup. Determine whether all abstract states of the
	package and any nested packages have received a refinement
	and if not, emit errors.
	(Requires_Completion_In_Body): Add new formal parameter
	Do_Abstract_States. Update the comment on usage. Propagate the
	Do_Abstract_States flag to all Unit_Requires_Body calls.
	(Unit_Requires_Body): Remove formal
	parameter Ignore_Abstract_States. Add new formal paramter
	Do_Abstract_States. Propagate the Do_Abstract_States flag to
	all Requires_Completion_In calls.
	* sem_ch7.ads (Unit_Requires_Body): Remove formal
	parameter Ignore_Abstract_States. Add new formal paramter
	Do_Abstract_States. Update the comment on usage.
	* sem_ch9.adb (Analyze_Single_Protected_Declaration): Do
	not initialize the constituent list as this is now done on a
	need-to-add-element basis.
	(Analyze_Single_Task_Declaration):
	Do not initialize the constituent list as this is now done on
	a need-to-add-element basis.
	* sem_ch10.adb (Decorate_State): Do not initialize the constituent
	lists as this is now done on a need-to-add-element basis.
	* sem_prag.adb (Analyze_Constituent): Set the
	refinement constituents when adding a new element.
	(Analyze_Part_Of_In_Decl_Part): Set the Part_Of constituents when
	adding a new element.
	(Analyze_Part_Of_Option): Set the Part_Of
	constituents when adding a new element.
	(Analyze_Pragma): Set the Part_Of constituents when adding a new
	element.
	(Check_Constituent_Usage (all versions)): Reimplemented.
	(Collect_Constituent): Set the refinement constituents when adding
	a new element.
	(Create_Abstract_State): Do not initialize the
	constituent lists as this is now done on a need-to-add-element basis.
	(Propagate_Part_Of): Set the Part_Of constituents when
	adding a new element.
	* sem_util.adb (Check_State_Refinements): New routine.
	(Has_Non_Null_Refinement): Reimplemented.
	(Has_Null_Refinement): Reimplemented.
	(Requires_State_Refinement): Removed.
	* sem_util.ads (Check_State_Refinements): New routine.
	(Requires_State_Refinement): Removed.

Attachment: difs
Description: Text document