[Ada] Reject certain constants as constituents

[Pierre-Marie de Rodat <derodat at adacore dot com>]

This patch updates the analysis of pragma Refined_State to reject constants
which are used as refinement constituents and are either

   * Part of the visible state of a package

   * Part of the hidden state of a package, and lack indicator Part_Of.

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

--  var.ads

package Var
  with SPARK_Mode,
       Initializes => Input
is
   Input : Integer := 0;
end Var;

--  pack.ads

with Var;

package Pack
  with SPARK_Mode,
       Abstract_State => State
is
   procedure Force_Body;

private
   Const_1 : constant Integer := Var.Input;
   Const_2 : constant Integer := 2 with Part_Of => State;

   Var_1 : Integer := 1;
   Var_2 : Integer := 2 with Part_Of => State;

   package Priv_Pack is
      Const_3 : constant Integer := Var.Input;
      Const_4 : constant Integer := 4 with Part_Of => State;

      Var_3 : Integer := 3;
      Var_4 : Integer := 4 with Part_Of => State;
   end Priv_Pack;
end Pack;

--  pack.adb

package body Pack
  with SPARK_Mode,
       Refined_State =>
         (State =>
           (Const_1,                                                 --  Error
            Const_2,                                                 --  OK
            Var_1,                                                   --  Error
            Var_2,                                                   --  OK
            Priv_Pack.Const_3,                                       --  Error
            Priv_Pack.Const_4,                                       --  OK
            Priv_Pack.Var_3,                                         --  Error
            Priv_Pack.Var_4,                                         --  OK
            Const_5,                                                 --  OK
            Const_6,                                                 --  OK
            Body_Pack.Const_7,                                       --  OK
            Body_Pack.Const_8))                                      --  OK
is
   Const_5 : constant Integer := Var.Input;
   Const_6 : constant Integer := 6;

   package Body_Pack is
      Const_7 : constant Integer := Var.Input;
      Const_8 : constant Integer := 8;
   end Body_Pack;

   procedure Force_Body is begin null; end Force_Body;
end Pack;

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

$ gcc -c -gnatf pack.adb
pack.adb:5:13: cannot use "Const_1" in refinement, constituent is not a hidden
  state of package "Pack"
pack.adb:7:13: cannot use "Var_1" in refinement, constituent is not a hidden
  state of package "Pack"
pack.adb:9:22: cannot use "Const_3" in refinement, constituent is not a hidden
  state of package "Pack"
pack.adb:11:22: cannot use "Var_3" in refinement, constituent is not a hidden
  state of package "Pack"
pack.ads:13:04: indicator Part_Of is required in this context (SPARK RM
  7.2.6(2))
pack.ads:13:04: "Var_1" is declared in the private part of package "Pack"
pack.ads:20:07: indicator Part_Of is required in this context (SPARK RM
  7.2.6(2))
pack.ads:20:07: "Var_3" is declared in the private part of package "Pack"

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

2017-12-15  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Match_Constituent): Do not quietly accept constants as
	suitable constituents.
	* exp_util.adb: Minor reformatting.

Attachment: difs
Description: Text document