===================================================================
@@ -137,7 +137,8 @@
-- there are no tasks.
function Caller_Known_Size
- (Func_Call : Node_Id; Result_Subt : Entity_Id) return Boolean;
+ (Func_Call : Node_Id;
+ Result_Subt : Entity_Id) return Boolean;
-- True if result subtype is definite, or has a size that does not require
-- secondary stack usage (i.e. no variant part or components whose type
-- depends on discriminants). In particular, untagged types with only
@@ -837,11 +838,14 @@
-----------------------
function Caller_Known_Size
- (Func_Call : Node_Id; Result_Subt : Entity_Id) return Boolean is
+ (Func_Call : Node_Id;
+ Result_Subt : Entity_Id) return Boolean
+ is
begin
- return (Is_Definite_Subtype (Underlying_Type (Result_Subt))
- and then No (Controlling_Argument (Func_Call)))
- or else not Requires_Transient_Scope (Underlying_Type (Result_Subt));
+ return
+ (Is_Definite_Subtype (Underlying_Type (Result_Subt))
+ and then No (Controlling_Argument (Func_Call)))
+ or else not Requires_Transient_Scope (Underlying_Type (Result_Subt));
end Caller_Known_Size;
--------------------------------
@@ -8081,7 +8085,8 @@
declare
Definite : constant Boolean :=
- Caller_Known_Size (Func_Call, Result_Subt);
+ Caller_Known_Size (Func_Call, Result_Subt);
+
begin
-- Create an access type designating the function's result subtype.
-- We use the type of the original call because it may be a call to
===================================================================
@@ -281,6 +281,13 @@
if Chars (Subp_Id) = Name_uPostconditions then
return True;
+ -- The context is the internally built predicate function,
+ -- which is OK because the real check was done before the
+ -- predicate function was generated.
+
+ elsif Is_Predicate_Function (Subp_Id) then
+ return True;
+
else
Subp_Decl :=
Original_Node (Unit_Declaration_Node (Subp_Id));
@@ -362,10 +369,12 @@
return True;
-- An assertion expression pragma is Ghost when it contains a
- -- reference to a Ghost entity (SPARK RM 6.9(10)).
+ -- reference to a Ghost entity (SPARK RM 6.9(10)), except for
+ -- predicate pragmas (SPARK RM 6.9(11)).
- elsif Assertion_Expression_Pragma (Prag_Id) then
-
+ elsif Assertion_Expression_Pragma (Prag_Id)
+ and then Prag_Id /= Pragma_Predicate
+ then
-- Ensure that the assertion policy and the Ghost policy are
-- compatible (SPARK RM 6.9(18)).
@@ -464,9 +473,16 @@
return True;
-- A reference to a Ghost entity can appear within an aspect
- -- specification (SPARK RM 6.9(10)).
+ -- specification (SPARK RM 6.9(10)). The precise checking will
+ -- occur when analyzing the corresponding pragma. We make an
+ -- exception for predicate aspects that only allow referencing
+ -- a Ghost entity when the corresponding type declaration is
+ -- Ghost (SPARK RM 6.9(11)).
- elsif Nkind (Par) = N_Aspect_Specification then
+ elsif Nkind (Par) = N_Aspect_Specification
+ and then not Same_Aspect
+ (Get_Aspect_Id (Par), Aspect_Predicate)
+ then
return True;
elsif Is_OK_Declaration (Par) then
===================================================================
@@ -855,13 +855,14 @@
if Is_Non_Empty_List (Aspects) then
if Func then
- Error_Msg ("aspect specifications must come after "
- & "parenthesized expression",
- Sloc (First (Aspects)));
+ Error_Msg
+ ("aspect specifications must come after "
+ & "parenthesized expression",
+ Sloc (First (Aspects)));
else
- Error_Msg ("aspect specifications must come after "
- & "subprogram specification",
- Sloc (First (Aspects)));
+ Error_Msg
+ ("aspect specifications must come after subprogram "
+ & "specification", Sloc (First (Aspects)));
end if;
end if;
===================================================================
@@ -12649,7 +12649,6 @@
--------------------------------
procedure Resolve_Aspect_Expressions (E : Entity_Id) is
-
function Resolve_Name (N : Node_Id) return Traverse_Result;
-- Verify that all identifiers in the expression, with the exception
-- of references to the current entity, denote visible entities. This
@@ -12668,6 +12667,7 @@
function Resolve_Name (N : Node_Id) return Traverse_Result is
Dummy : Traverse_Result;
+
begin
if Nkind (N) = N_Selected_Component then
if Nkind (Prefix (N)) = N_Identifier
@@ -12700,6 +12700,8 @@
procedure Resolve_Aspect_Expression is new Traverse_Proc (Resolve_Name);
+ -- Local variables
+
ASN : Node_Id := First_Rep_Item (E);
-- Start of processing for Resolve_Aspect_Expressions
===================================================================
@@ -1205,126 +1205,173 @@
Item_Is_Output : out Boolean)
is
begin
- Item_Is_Input := False;
- Item_Is_Output := False;
+ case Ekind (Item_Id) is
- -- Abstract states
+ -- Abstract states
- if Ekind (Item_Id) = E_Abstract_State then
+ when E_Abstract_State =>
- -- When pragma Global is present, the mode of the state may be
- -- further constrained by setting a more restrictive mode.
+ -- When pragma Global is present it determines the mode of
+ -- the abstract state.
- if Global_Seen then
- if Appears_In (Subp_Inputs, Item_Id) then
- Item_Is_Input := True;
- end if;
+ if Global_Seen then
+ Item_Is_Input := Appears_In (Subp_Inputs, Item_Id);
+ Item_Is_Output := Appears_In (Subp_Outputs, Item_Id);
- if Appears_In (Subp_Outputs, Item_Id) then
+ -- Otherwise the state has a default IN OUT mode, because it
+ -- behaves as a variable.
+
+ else
+ Item_Is_Input := True;
Item_Is_Output := True;
end if;
- -- Otherwise the state has a default IN OUT mode
+ -- Constants and IN parameters
- else
- Item_Is_Input := True;
- Item_Is_Output := True;
- end if;
+ when E_Constant
+ | E_Generic_In_Parameter
+ | E_In_Parameter
+ | E_Loop_Parameter
+ =>
+ -- When pragma Global is present it determines the mode
+ -- of constant objects as inputs (and such objects cannot
+ -- appear as outputs in the Global contract).
- -- Constants
+ if Global_Seen then
+ Item_Is_Input := Appears_In (Subp_Inputs, Item_Id);
+ else
+ Item_Is_Input := True;
+ end if;
- elsif Ekind_In (Item_Id, E_Constant,
- E_Loop_Parameter)
- then
- Item_Is_Input := True;
+ Item_Is_Output := False;
- -- Parameters
+ -- Variables and IN OUT parameters
- elsif Ekind_In (Item_Id, E_Generic_In_Parameter,
- E_In_Parameter)
- then
- Item_Is_Input := True;
+ when E_Generic_In_Out_Parameter
+ | E_In_Out_Parameter
+ | E_Variable
+ =>
+ -- When pragma Global is present it determines the mode of
+ -- the object.
- elsif Ekind_In (Item_Id, E_Generic_In_Out_Parameter,
- E_In_Out_Parameter)
- then
- Item_Is_Input := True;
- Item_Is_Output := True;
+ if Global_Seen then
- elsif Ekind (Item_Id) = E_Out_Parameter then
- if Scope (Item_Id) = Spec_Id then
+ -- A variable has mode IN when its type is unconstrained
+ -- or tagged because array bounds, discriminants or tags
+ -- can be read.
- -- An OUT parameter of the related subprogram has mode IN
- -- if its type is unconstrained or tagged because array
- -- bounds, discriminants or tags can be read.
+ Item_Is_Input :=
+ Appears_In (Subp_Inputs, Item_Id)
+ or else Is_Unconstrained_Or_Tagged_Item (Item_Id);
- if Is_Unconstrained_Or_Tagged_Item (Item_Id) then
- Item_Is_Input := True;
+ Item_Is_Output := Appears_In (Subp_Outputs, Item_Id);
+
+ -- Otherwise the variable has a default IN OUT mode
+
+ else
+ Item_Is_Input := True;
+ Item_Is_Output := True;
end if;
- Item_Is_Output := True;
+ when E_Out_Parameter =>
- -- An OUT parameter of an enclosing subprogram behaves as a
- -- read-write variable in which case the mode is IN OUT.
+ -- An OUT parameter of the related subprogram; it cannot
+ -- appear in Global.
- else
- Item_Is_Input := True;
- Item_Is_Output := True;
- end if;
+ if Scope (Item_Id) = Spec_Id then
- -- Protected types
+ -- The parameter has mode IN if its type is unconstrained
+ -- or tagged because array bounds, discriminants or tags
+ -- can be read.
- elsif Ekind (Item_Id) = E_Protected_Type then
+ Item_Is_Input :=
+ Is_Unconstrained_Or_Tagged_Item (Item_Id);
- -- A protected type acts as a formal parameter of mode IN when
- -- it applies to a protected function.
+ Item_Is_Output := True;
- if Ekind (Spec_Id) = E_Function then
- Item_Is_Input := True;
+ -- An OUT parameter of an enclosing subprogram; it can
+ -- appear in Global and behaves as a read-write variable.
- -- Otherwise the protected type acts as a formal of mode IN OUT
+ else
+ -- When pragma Global is present it determines the mode
+ -- of the object.
- else
- Item_Is_Input := True;
- Item_Is_Output := True;
- end if;
+ if Global_Seen then
- -- Task types
+ -- A variable has mode IN when its type is
+ -- unconstrained or tagged because array
+ -- bounds, discriminants or tags can be read.
- elsif Ekind (Item_Id) = E_Task_Type then
- Item_Is_Input := True;
- Item_Is_Output := True;
+ Item_Is_Input :=
+ Appears_In (Subp_Inputs, Item_Id)
+ or else Is_Unconstrained_Or_Tagged_Item (Item_Id);
- -- Variable case
+ Item_Is_Output := Appears_In (Subp_Outputs, Item_Id);
- else pragma Assert (Ekind (Item_Id) = E_Variable);
+ -- Otherwise the variable has a default IN OUT mode
- -- When pragma Global is present, the mode of the variable may
- -- be further constrained by setting a more restrictive mode.
+ else
+ Item_Is_Input := True;
+ Item_Is_Output := True;
+ end if;
+ end if;
- if Global_Seen then
+ -- Protected types
- -- A variable has mode IN when its type is unconstrained or
- -- tagged because array bounds, discriminants or tags can be
- -- read.
+ when E_Protected_Type =>
+ if Global_Seen then
- if Appears_In (Subp_Inputs, Item_Id)
- or else Is_Unconstrained_Or_Tagged_Item (Item_Id)
- then
- Item_Is_Input := True;
+ -- A variable has mode IN when its type is unconstrained
+ -- or tagged because array bounds, discriminants or tags
+ -- can be read.
+
+ Item_Is_Input :=
+ Appears_In (Subp_Inputs, Item_Id)
+ or else Is_Unconstrained_Or_Tagged_Item (Item_Id);
+
+ Item_Is_Output := Appears_In (Subp_Outputs, Item_Id);
+
+ else
+ -- A protected type acts as a formal parameter of mode IN
+ -- when it applies to a protected function.
+
+ if Ekind (Spec_Id) = E_Function then
+ Item_Is_Input := True;
+ Item_Is_Output := False;
+
+ -- Otherwise the protected type acts as a formal of mode
+ -- IN OUT.
+
+ else
+ Item_Is_Input := True;
+ Item_Is_Output := True;
+ end if;
end if;
- if Appears_In (Subp_Outputs, Item_Id) then
+ -- Task types
+
+ when E_Task_Type =>
+
+ -- When pragma Global is present it determines the mode of
+ -- the object.
+
+ if Global_Seen then
+ Item_Is_Input :=
+ Appears_In (Subp_Inputs, Item_Id)
+ or else Is_Unconstrained_Or_Tagged_Item (Item_Id);
+
+ Item_Is_Output := Appears_In (Subp_Outputs, Item_Id);
+
+ -- Otherwise task types act as IN OUT parameters
+
+ else
+ Item_Is_Input := True;
Item_Is_Output := True;
end if;
- -- Otherwise the variable has a default IN OUT mode
-
- else
- Item_Is_Input := True;
- Item_Is_Output := True;
- end if;
- end if;
+ when others =>
+ raise Program_Error;
+ end case;
end Find_Role;
----------------
@@ -5069,7 +5116,7 @@
-- pragma is inserted in its declarative part.
elsif From_Aspect_Specification (N)
- and then Ent = Current_Scope
+ and then Ent = Current_Scope
and then
Nkind (Unit_Declaration_Node (Ent)) = N_Subprogram_Body
then
@@ -28300,7 +28347,7 @@
if Nkind (Clause) = N_Null then
null;
- -- A dependency cause appears as component association
+ -- A dependency clause appears as component association
elsif Nkind (Clause) = N_Component_Association then
Collect_Dependency_Item
@@ -28424,21 +28471,15 @@
Subp_Decl := Unit_Declaration_Node (Subp_Id);
Spec_Id := Unique_Defining_Entity (Subp_Decl);
- -- Process all [generic] formal parameters
+ -- Process all formal parameters
Formal := First_Entity (Spec_Id);
while Present (Formal) loop
- if Ekind_In (Formal, E_Generic_In_Parameter,
- E_In_Out_Parameter,
- E_In_Parameter)
- then
+ if Ekind_In (Formal, E_In_Out_Parameter, E_In_Parameter) then
Append_New_Elmt (Formal, Subp_Inputs);
end if;
- if Ekind_In (Formal, E_Generic_In_Out_Parameter,
- E_In_Out_Parameter,
- E_Out_Parameter)
- then
+ if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then
Append_New_Elmt (Formal, Subp_Outputs);
-- Out parameters can act as inputs when the related type is