This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

[Ada] Constants without variable input are not hidden state


This patch implements the following rule with respect to constants:

   SPARK RM 7.1.1(2) - The hidden state of a package P consists of:
   * any variables, or constants with variable inputs, declared immediately in
   the private part or body of P.

Constants without variable input are not considered part of the hidden state of
a package. These constants do not require indicator Part_Of when declared in
the private part of a package.

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

--  types.ads

ackage Types is
   type CA is array (1 .. 3) of Integer;
   type UA is array (Integer range <>) of Integer;

   type VR (Discr : Boolean) is record
      Comp_1 : Integer;

      case Discr is
         when True =>
            Comp_2 : Integer;
         when others =>
            null;
      end case;
   end record;

   subtype CR is VR (True);

   function Get_CA return CA;
   function Get_CR return CR;
   function Get_In return Integer;
   function Get_UA return UA;
   function Get_VR return VR;
end Types;

--  types.adb

package body Types is
   function Get_CA return CA is
      Result : constant CA := (others => 0);
   begin
      return Result;
   end Get_CA;

   function Get_CR return CR is
      Result : constant CR := (Discr => True, Comp_1 => 0, Comp_2 => 0);
   begin
      return Result;
   end Get_CR;

   function Get_In return Integer is
   begin
      return 0;
   end Get_In;

   function Get_UA return UA is
   begin
      return (0, 0, 0);
   end Get_UA;

   function Get_VR return VR is
   begin
      return (Discr => False, Comp_1 => 0);
   end Get_VR;
end Types;

--  legal_hidden_state.ads

with Types; use Types;
pragma Elaborate_All (Types);

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

private
   --  Constrained array

   C1 : constant CA := Get_CA with Part_Of => State;
   C2 : constant CA := (others => Get_In) with Part_Of => State;
   C3 : constant CA := (1, 2, Get_In) with Part_Of => State;

   --  Constrained record

   C4 : constant CR := Get_CR with Part_Of => State;
   C5 : constant CR :=
          (Discr => True, Comp_1 => 1, Comp_2 => Get_In) with Part_Of => State;

   --  Scalar

   C6 : constant Integer := Get_In with Part_Of => State;

   --  Unconstrained array

   C7 : constant UA := Get_UA with Part_Of => State;
   C8 : constant UA (1 .. 3) := (others => Get_In) with Part_Of => State;
   C9 : constant UA := (1, 2, Get_In) with Part_Of => State;

   --  Variant record

   C10 : constant VR := Get_VR with Part_Of => State;
   C11 : constant VR :=
           (Discr => False, Comp_1 => Get_In) with Part_Of => State;
   C12 : constant VR (False) :=
           (Discr => False, Comp_1 => Get_In) with Part_Of => State;
end Legal_Hidden_State;

--  legal_hidden_state.adb

package body Legal_Hidden_State
  with SPARK_Mode,
       Refined_State =>
         (State =>
           (C1,  C2,  C3,  C4,  C5,  C6,  C7,  C8,  C9,  C10, C11, C12,
            C13, C14, C15, C16, C17, C18, C19, C20, C21, C22, C23, C24))
is
   --  Constrained array

   C13 : constant CA := Get_CA;
   C14 : constant CA := (others => Get_In);
   C15 : constant CA := (1, 2, Get_In);

   --  Constrained record

   C16 : constant CR := Get_CR;
   C17 : constant CR := (Discr => True, Comp_1 => 17, Comp_2 => Get_In);

   --  Scalar

   C18 : constant Integer := Get_In;

   --  Unconstrained array

   C19 : constant UA := Get_UA;
   C20 : constant UA (1 .. 3) := (others => Get_In);
   C21 : constant UA := (1, 2, Get_In);

   --  Variant record

   C22 : constant VR := Get_VR;
   C23 : constant VR := (Discr => False, Comp_1 => Get_In);
   C24 : constant VR (False) := (Discr => False, Comp_1 => Get_In);

   procedure Force_Body is begin null; end Force_Body;
end Legal_Hidden_State;

-----------------
-- Compilation --
-----------------

$ gcc -c legal_hidden_state.adb

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

2015-05-22  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Pragma): Constants without variable
	input do not require indicator Part_Of.
	(Check_Missing_Part_Of): Constants without variable input do not
	requrie indicator Part_Of.
	(Collect_Visible_States): Constants without variable input are
	not part of the hidden state of a package.
	* sem_util.ads, sem_util.adb (Has_Variable_Input): New routine.

Attachment: difs
Description: Text document


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]