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 <kirtc...@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.
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 203505)
+++ sem_prag.adb (working copy)
@@ -236,6 +236,12 @@
-- Get_SPARK_Mode_Id. Convert a name into a corresponding value of type
-- SPARK_Mode_Id.
+ function Is_Unconstrained_Or_Tagged_Item (Item : Entity_Id) return Boolean;
+ -- Subsidiary to Collect_Subprogram_Inputs_Outputs and the analysis of
+ -- pragma Depends. Determine whether the type of dependency item Item is
+ -- tagged, unconstrained array, unconstrained record or a record with at
+ -- least one unconstrained component.
+
procedure Preanalyze_CTC_Args (N, Arg_Req, Arg_Ens : Node_Id);
-- Preanalyze the boolean expressions in the Requires and Ensures arguments
-- of a Test_Case pragma if present (possibly Empty). We treat these as
@@ -839,9 +845,10 @@
-- Input
if Is_Input then
- if Ekind (Item_Id) = E_Out_Parameter
- or else (Global_Seen
- and then not Appears_In (Subp_Inputs, Item_Id))
+ if (Ekind (Item_Id) = E_Out_Parameter
+ and then not Is_Unconstrained_Or_Tagged_Item (Item_Id))
+ or else
+ (Global_Seen and then not Appears_In (Subp_Inputs, Item_Id))
then
Error_Msg_NE
("item & must have mode in or in out", Item, Item_Id);
@@ -1538,7 +1545,7 @@
Context := Scope (Subp_Id);
while Present (Context) and then Context /= Standard_Standard loop
if Is_Subprogram (Context)
- and then Has_Aspect (Context, Aspect_Global)
+ and then Present (Get_Pragma (Context, Pragma_Global))
then
Collect_Subprogram_Inputs_Outputs
(Subp_Id => Context,
@@ -20407,6 +20414,16 @@
if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then
Add_Item (Formal, Subp_Outputs);
+
+ -- Out parameters can act as inputs when the related type is
+ -- tagged, unconstrained array, unconstrained record or record
+ -- with unconstrained components.
+
+ if Ekind (Formal) = E_Out_Parameter
+ and then Is_Unconstrained_Or_Tagged_Item (Formal)
+ then
+ Add_Item (Formal, Subp_Inputs);
+ end if;
end if;
Next_Formal (Formal);
@@ -20415,15 +20432,11 @@
-- If the subprogram is subject to pragma Global, traverse all global
-- lists and gather the relevant items.
- Global := Find_Aspect (Subp_Id, Aspect_Global);
+ Global := Get_Pragma (Subp_Id, Pragma_Global);
if Present (Global) then
Global_Seen := True;
+ List := Expression (First (Pragma_Argument_Associations (Global)));
- -- Retrieve the pragma as it contains the analyzed lists
-
- Global := Aspect_Rep_Item (Global);
- List := Expression (First (Pragma_Argument_Associations (Global)));
-
-- The pragma may not have been analyzed because of the arbitrary
-- declaration order of aspects. Make sure that it is analyzed for
-- the purposes of item extraction.
@@ -21074,6 +21087,62 @@
and then List_Containing (N) = Private_Declarations (Parent (N));
end Is_Private_SPARK_Mode;
+ -------------------------------------
+ -- Is_Unconstrained_Or_Tagged_Item --
+ -------------------------------------
+
+ function Is_Unconstrained_Or_Tagged_Item
+ (Item : Entity_Id) return Boolean
+ is
+ function Has_Unconstrained_Component (Typ : Entity_Id) return Boolean;
+ -- Determine whether record type Typ has at least one unconstrained
+ -- component.
+
+ ---------------------------------
+ -- Has_Unconstrained_Component --
+ ---------------------------------
+
+ function Has_Unconstrained_Component (Typ : Entity_Id) return Boolean is
+ Comp : Entity_Id;
+
+ begin
+ Comp := First_Component (Typ);
+ while Present (Comp) loop
+ if Is_Unconstrained_Or_Tagged_Item (Comp) then
+ return True;
+ end if;
+
+ Next_Component (Comp);
+ end loop;
+
+ return False;
+ end Has_Unconstrained_Component;
+
+ -- Local variables
+
+ Typ : constant Entity_Id := Etype (Item);
+
+ -- Start of processing for Is_Unconstrained_Or_Tagged_Item
+
+ begin
+ if Is_Tagged_Type (Typ) then
+ return True;
+
+ elsif Is_Array_Type (Typ) and then not Is_Constrained (Typ) then
+ return True;
+
+ elsif Is_Record_Type (Typ) then
+ if Has_Discriminants (Typ) and then not Is_Constrained (Typ) then
+ return True;
+ else
+ return Has_Unconstrained_Component (Typ);
+ end if;
+
+ else
+ return False;
+ end if;
+ end Is_Unconstrained_Or_Tagged_Item;
+
-----------------------------
-- Is_Valid_Assertion_Kind --
-----------------------------
