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] Use of unconstrained or tagged items in aspect Depends


This patch implements the following semantic rule of aspect Depends:

The input set of a subprogram is the explicit input set of the subprogram
augmented with those formal parameters of mode out having discriminants, array
bounds, or a tag which can be read and whose values are not implied by the
subtype of the parameter. More specifically, it includes formal parameters of
mode out which are of an unconstrained array subtype, an unconstrained
discriminated subtype, a tagged type, or a type having a subcomponent of an
unconstrained discriminated subtype. [Tagged types are mentioned in this rule
in anticipation of a later version of SPARK 2014 in which the current
x restriction on uses of the 'Class attribute is relaxed; currently there is no
way to read or otherwise depend on the underlying tag of an out mode formal
parameter of a tagged type.]

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

--  types.ads

package Types is
   type Tag_Typ is tagged null record;

   type Unc_Array is array (Positive range <>) of Integer;

   type Constr_Kind is (One, Two, Three, Four);

   type Discr_Rec (Discr : Constr_Kind) is record
      Data : Integer;
   end record;

   type Var_Rec (Discr : Constr_Kind) is record
      Data : Integer;

      case Discr is
         when One =>
            Data_One : Integer;
         when Two =>
            Data_Two : Discr_Rec (Discr);
         when others =>
            Data_Others : Integer;
      end case;
   end record;

   type Constr_Array is array (Positive range 1 .. 10) of Integer;

   type Rec is record
      Data : Integer;
   end record;

   subtype Constr_Rec is Var_Rec (Two);
end Types;

--  main.adb

with Types; use Types;

procedure Main is
   procedure OK
     (Init     : Integer;
      Formal_1 : out Tag_Typ;
      Formal_2 : out Unc_Array;
      Formal_3 : out Discr_Rec;
      Formal_4 : out Var_Rec;
      Result   : out Integer)
   with Depends =>
     (Result => (Formal_1, Formal_2, Formal_3, Formal_4),
     (Formal_1, Formal_2, Formal_3, Formal_4) => Init)
   is begin null; end OK;

   procedure Error
     (Init     : Integer;
      Formal_1 : out Constr_Array;
      Formal_2 : out Rec;
      Formal_3 : out Constr_Rec;
      Result   : out Integer)
   with Depends =>
     (Result => (Formal_1, Formal_2, Formal_3),
     (Formal_1, Formal_2, Formal_3) => Init)
   is begin null; end Error;

begin null; end Main;

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

$ gcc -c -gnat12 -gnatd.V main.adb
main.adb:23:18: item "Formal_1" must have mode in or in out
main.adb:23:28: item "Formal_2" must have mode in or in out
main.adb:23:38: item "Formal_3" must have mode in or in out

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

2013-10-13  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Check_Mode): Do
	not emit an error when we are looking at inputs and
	the item is an unconstrained or tagged out parameter.
	(Check_Mode_Restriction_In_Enclosing_Context): Use Get_Pragma
	to find whether the context is subject to aspect/pragma Global.
	(Collect_Subprogram_Inputs_Outputs): Unconstrained or tagged
	out parameters are now considered inputs. Use Get_Pragma to
	find wheher the subprogram is subject to aspect/pragma Global.
	(Is_Unconstrained_Or_Tagged_Item): 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]