+2015-10-20 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * aspects.adb Add aspect Volatile_Function to table
+ Canonical_Aspect.
+ * aspect.ads Add aspect Volatile_Function to tables
+ Aspect_Argument, Aspect_Delay, Aspect_Id, Aspect_Names
+ and Implementation_Defined_Aspect. Aspects Async_Readers,
+ Async_Writers, Effective_Reads and Effective_Writes are no
+ longer Boolean.
+ * einfo.adb (Get_Pragma): Add an entry for pragma
+ Volatile_Function.
+ * par-prag.adb (Prag): Pragma Volatile_Function does not need
+ special processing by the parser.
+ * rtsfind.ads Add an entry for Ada.Synchronous_Task_Control in
+ table RTU_Id. Add an entry for Suspension_Object in table RE_Id.
+ * sem_ch3.adb Fix SPARK RM references.
+ (Analyze_Object_Contract): Update the error guard.
+ * sem_ch5.adb Fix SPARK RM references.
+ * sem_ch6.adb (Analyze_Subprogram_Body_Contract): Ensure
+ that a non-volatile function does not contain an effectively
+ volatile parameter.
+ (Analyze_Subprogram_Contract): Ensure
+ that a non-volatile function does not contain an effectively
+ volatile parameter.
+ * sem_ch12.adb (Instantiate_Object): Remove the reference to
+ the SPARK RM from the error message.
+ * sem_ch13.adb (Analyze_Aspect_Specifications): Add
+ processing for aspects Async_Readers, Async_Writers,
+ Effective_Reads, Effective_Writes and Volatile_Function.
+ (Check_Aspect_At_Freeze_Point): Aspects Async_Readers,
+ Async_Writers, Effective_Reads, Effective_Writes and
+ Volatile_Function do not need special processing at the freeze
+ point.
+ * sem_prag.adb Add an entry for pragma Volatile_Function in
+ table Sig_Flags.
+ (Analyze_External_Property_In_Decl_Part):
+ Reimplemented as Async_Readers, Async_Writers, Effective_Reads
+ and Effective_Writes are no longer Boolean pragmas.
+ (Analyze_Global_Item): An external state or effectively
+ volatile object cannot appear as an item in pragma
+ [Refined_]Global.
+ (Analyze_Pragma): Change the implementation
+ of Async_Readers, Async_Writers, Effective_Reads and
+ Effective_Writes as these are no longer Boolean pragmas.
+ Use routine Check_Static_Boolean_Expression to verify the
+ optional Boolean expression of Async_Readers, Async_Writers,
+ Constant_After_Elaboration, Effective_Reads, Effective_Writes,
+ Extensions_Visible and Volatile_Function. Add processing for
+ pragma Volatile_Function.
+ (Check_Static_Boolean_Expression): New routine.
+ (Find_Related_Context): Update the comment on usage.
+ (Is_Enabled_Pragma): New routine.
+ * sem_prag.ads (Is_Enabled_Pragma): New routine.
+ * sem_res.adb Fix SPARK RM references.
+ (Is_OK_Volatile_Context): Add detection for return statements.
+ (Resolve_Actuals): Remove the check concerning an effectively volatile
+ OUT actual parameter as this is now done by the SPARK flow analyzer.
+ (Resolve_Entity_Name): Remove the check concerning an effectively
+ volatile OUT formal parameter as this is now done by the SPARK
+ flow analyzer. (Within_Volatile_Function): New routine.
+ * sem_util.adb (Add_Contract_Item): Add processing for pragma
+ Volatile_Function.
+ (Check_Nonvolatile_Function_Profile): New routine.
+ (Is_Descendant_Of_Suspension_Object): New routine.
+ (Is_Effectively_Volatile): Protected types and descendants of
+ Suspension_Object are now treated as effectively volatile.
+ (Is_Enabled): The optional Boolean expression of pragmas
+ Async_Readers, Async_Writers, Effective_Reads and Effective_Writes
+ now appears as the first argument.
+ (Is_Volatile_Function): New routine.
+ * sem_util.ads Add SPARK RM references.
+ (Add_Contract_Item): Update the comment on usage.
+ (Check_Nonvolatile_Function_Profile): New routine.
+ (Is_Effectively_Volatile): Update the comment on usage.
+ (Is_Volatile_Function): New routine.
+ * snames.ads-tmpl Add a predefined name and pragma id for
+ Volatile_Function.
+
2015-10-20 Arnaud Charlet <charlet@adacore.com>
* gnat_ugn.texi, gnat_rm.texi: Regenerate.
Aspect_Volatile => Aspect_Volatile,
Aspect_Volatile_Components => Aspect_Volatile_Components,
Aspect_Volatile_Full_Access => Aspect_Volatile_Full_Access,
+ Aspect_Volatile_Function => Aspect_Volatile_Function,
Aspect_Warnings => Aspect_Warnings,
Aspect_Write => Aspect_Write);
Aspect_Address,
Aspect_Alignment,
Aspect_Annotate, -- GNAT
+ Aspect_Async_Readers, -- GNAT
+ Aspect_Async_Writers, -- GNAT
Aspect_Attach_Handler,
Aspect_Bit_Order,
Aspect_Component_Size,
Aspect_Dimension_System, -- GNAT
Aspect_Dispatching_Domain,
Aspect_Dynamic_Predicate,
+ Aspect_Effective_Reads, -- GNAT
+ Aspect_Effective_Writes, -- GNAT
Aspect_Extensions_Visible, -- GNAT
Aspect_External_Name,
Aspect_External_Tag,
Aspect_Unsuppress,
Aspect_Value_Size, -- GNAT
Aspect_Variable_Indexing,
+ Aspect_Volatile_Function, -- GNAT
Aspect_Warnings, -- GNAT
Aspect_Write,
-- the aspect value is inherited from the parent, in which case, we do
-- not allow False if we inherit a True value from the parent.
- Aspect_Async_Readers, -- GNAT
- Aspect_Async_Writers, -- GNAT
Aspect_Asynchronous,
Aspect_Atomic,
Aspect_Atomic_Components,
Aspect_Disable_Controlled, -- GNAT
Aspect_Discard_Names,
- Aspect_Effective_Reads, -- GNAT
- Aspect_Effective_Writes, -- GNAT
Aspect_Export,
Aspect_Favor_Top_Level, -- GNAT
Aspect_Independent,
Aspect_Unreferenced => True,
Aspect_Unreferenced_Objects => True,
Aspect_Value_Size => True,
+ Aspect_Volatile_Function => True,
Aspect_Warnings => True,
others => False);
-- aspect is enabled. If it is False, the aspect is disabled.
subtype Boolean_Aspects is
- Aspect_Id range Aspect_Async_Readers .. Aspect_Id'Last;
+ Aspect_Id range Aspect_Asynchronous .. Aspect_Id'Last;
subtype Pre_Post_Aspects is
Aspect_Id range Aspect_Post .. Aspect_Precondition;
Aspect_Address => Expression,
Aspect_Alignment => Expression,
Aspect_Annotate => Expression,
+ Aspect_Async_Readers => Optional_Expression,
+ Aspect_Async_Writers => Optional_Expression,
Aspect_Attach_Handler => Expression,
Aspect_Bit_Order => Expression,
Aspect_Component_Size => Expression,
Aspect_Dimension_System => Expression,
Aspect_Dispatching_Domain => Expression,
Aspect_Dynamic_Predicate => Expression,
+ Aspect_Effective_Reads => Optional_Expression,
+ Aspect_Effective_Writes => Optional_Expression,
Aspect_Extensions_Visible => Optional_Expression,
Aspect_External_Name => Expression,
Aspect_External_Tag => Expression,
Aspect_Unsuppress => Name,
Aspect_Value_Size => Expression,
Aspect_Variable_Indexing => Name,
+ Aspect_Volatile_Function => Optional_Expression,
Aspect_Warnings => Name,
Aspect_Write => Name,
Aspect_Volatile => Name_Volatile,
Aspect_Volatile_Components => Name_Volatile_Components,
Aspect_Volatile_Full_Access => Name_Volatile_Full_Access,
+ Aspect_Volatile_Function => Name_Volatile_Function,
Aspect_Warnings => Name_Warnings,
Aspect_Write => Name_Write);
Aspect_Synchronization => Never_Delay,
Aspect_Test_Case => Never_Delay,
Aspect_Unimplemented => Never_Delay,
+ Aspect_Volatile_Function => Never_Delay,
Aspect_Warnings => Never_Delay,
Aspect_Alignment => Rep_Aspect,
Id = Pragma_Part_Of or else
Id = Pragma_Refined_Depends or else
Id = Pragma_Refined_Global or else
- Id = Pragma_Refined_State;
+ Id = Pragma_Refined_State or else
+ Id = Pragma_Volatile_Function;
-- Contract / test case pragmas
Pragma_Volatile |
Pragma_Volatile_Components |
Pragma_Volatile_Full_Access |
+ Pragma_Volatile_Function |
Pragma_Warning_As_Error |
Pragma_Weak_External |
Pragma_Validity_Checks =>
-- --
------------------------------------------------------------------------------
-with Types; use Types;
-
-package Rtsfind is
-
-- This package contains the routine that is used to obtain runtime library
-- entities, loading in the required runtime library packages on demand. It
-- is also used for such purposes as finding System.Address when System has
-- not been explicitly With'ed.
+with Types; use Types;
+
+package Rtsfind is
+
------------------------
-- Runtime Unit Table --
------------------------
Ada_Real_Time,
Ada_Streams,
Ada_Strings,
+ Ada_Synchronous_Task_Control,
Ada_Tags,
Ada_Task_Identification,
Ada_Task_Termination,
RE_Unbounded_String, -- Ada.Strings.Unbounded
+ RE_Suspension_Object, -- Ada.Synchronous_Task_Control
+
RE_Access_Level, -- Ada.Tags
RE_Alignment, -- Ada.Tags
RE_Address_Array, -- Ada.Tags
RE_Unbounded_String => Ada_Strings_Unbounded,
+ RE_Suspension_Object => Ada_Synchronous_Task_Control,
+
RE_Access_Level => Ada_Tags,
RE_Alignment => Ada_Tags,
RE_Address_Array => Ada_Tags,
if Need_Subprogram_Instance_Body (N, Act_Decl_Id) then
Check_Forward_Instantiation (Gen_Decl);
- -- The wrapper package is always delayed, because it does not
- -- constitute a freeze point, but to insure that the freeze
- -- node is placed properly, it is created directly when
- -- instantiating the body (otherwise the freeze node might
- -- appear to early for nested instantiations).
+ -- The wrapper package is always delayed, because it does not
+ -- constitute a freeze point, but to insure that the freeze node
+ -- is placed properly, it is created directly when instantiating
+ -- the body (otherwise the freeze node might appear to early for
+ -- nested instantiations). For ASIS purposes, indicate that the
+ -- wrapper package has replaced the instantiation node.
elsif Nkind (Parent (N)) = N_Compilation_Unit then
-
- -- For ASIS purposes, indicate that the wrapper package has
- -- replaced the instantiation node.
-
Rewrite (N, Unit (Parent (N)));
Set_Unit (Parent (N), N);
end if;
- elsif Nkind (Parent (N)) = N_Compilation_Unit then
+ -- Replace instance node for library-level instantiations of
+ -- intrinsic subprograms, for ASIS use.
- -- Replace instance node for library-level instantiations of
- -- intrinsic subprograms, for ASIS use.
-
- Rewrite (N, Unit (Parent (N)));
- Set_Unit (Parent (N), N);
+ elsif Nkind (Parent (N)) = N_Compilation_Unit then
+ Rewrite (N, Unit (Parent (N)));
+ Set_Unit (Parent (N), N);
end if;
if Parent_Installed then
if SPARK_Mode = On then
Dynamic_Elaboration_Checks := False;
end if;
-
end if;
<<Leave>>
("actual must exclude null to match generic formal#", Actual);
end if;
- -- An effectively volatile object cannot be used as an actual in
- -- a generic instance. The following check is only relevant when
- -- SPARK_Mode is on as it is not a standard Ada legality rule.
+ -- An effectively volatile object cannot be used as an actual in a
+ -- generic instantiation (SPARK RM 7.1.3(7)). The following check is
+ -- relevant only when SPARK_Mode is on as it is not a standard Ada
+ -- legality rule.
if SPARK_Mode = On
and then Present (Actual)
and then Is_Effectively_Volatile_Object (Actual)
then
Error_Msg_N
- ("volatile object cannot act as actual in generic instantiation "
- & "(SPARK RM 7.1.3(8))", Actual);
+ ("volatile object cannot act as actual in generic instantiation",
+ Actual);
end if;
return List;
goto Continue;
end Abstract_State;
+ -- Aspect Async_Readers is never delayed because it is
+ -- equivalent to a source pragma which appears after the
+ -- related object declaration.
+
+ when Aspect_Async_Readers =>
+ Make_Aitem_Pragma
+ (Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))),
+ Pragma_Name => Name_Async_Readers);
+
+ Decorate (Aspect, Aitem);
+ Insert_Pragma (Aitem);
+ goto Continue;
+
+ -- Aspect Async_Writers is never delayed because it is
+ -- equivalent to a source pragma which appears after the
+ -- related object declaration.
+
+ when Aspect_Async_Writers =>
+ Make_Aitem_Pragma
+ (Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))),
+ Pragma_Name => Name_Async_Writers);
+
+ Decorate (Aspect, Aitem);
+ Insert_Pragma (Aitem);
+ goto Continue;
+
-- Aspect Constant_After_Elaboration is never delayed because
-- it is equivalent to a source pragma which appears after the
-- related object declaration.
Insert_Pragma (Aitem);
goto Continue;
+ -- Aspect Effecitve_Reads is never delayed because it is
+ -- equivalent to a source pragma which appears after the
+ -- related object declaration.
+
+ when Aspect_Effective_Reads =>
+ Make_Aitem_Pragma
+ (Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))),
+ Pragma_Name => Name_Effective_Reads);
+
+ Decorate (Aspect, Aitem);
+ Insert_Pragma (Aitem);
+ goto Continue;
+
+ -- Aspect Effective_Writes is never delayed because it is
+ -- equivalent to a source pragma which appears after the
+ -- related object declaration.
+
+ when Aspect_Effective_Writes =>
+ Make_Aitem_Pragma
+ (Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))),
+ Pragma_Name => Name_Effective_Writes);
+
+ Decorate (Aspect, Aitem);
+ Insert_Pragma (Aitem);
+ goto Continue;
+
-- Aspect Extensions_Visible is never delayed because it is
-- equivalent to a source pragma which appears after the
-- related subprogram.
end;
end if;
+ -- Aspect Volatile_Function is never delayed because it is
+ -- equivalent to a source pragma which appears after the
+ -- related subprogram.
+
+ when Aspect_Volatile_Function =>
+ Make_Aitem_Pragma
+ (Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))),
+ Pragma_Name => Name_Volatile_Function);
+
+ Decorate (Aspect, Aitem);
+ Insert_Pragma (Aitem);
+ goto Continue;
+
-- Case 2e: Annotate aspect
when Aspect_Annotate =>
goto Continue;
end if;
- -- External property aspects are Boolean by nature, but
- -- their pragmas must contain two arguments, the second
- -- being the optional Boolean expression.
-
- if A_Id = Aspect_Async_Readers or else
- A_Id = Aspect_Async_Writers or else
- A_Id = Aspect_Effective_Reads or else
- A_Id = Aspect_Effective_Writes
- then
- declare
- Args : List_Id;
-
- begin
- -- The first argument of the external property pragma
- -- is the related object.
-
- Args :=
- New_List (
- Make_Pragma_Argument_Association (Sloc (Ent),
- Expression => Ent));
-
- -- The second argument is the optional Boolean
- -- expression which must be propagated even if it
- -- evaluates to False as this has special semantic
- -- meaning.
-
- if Present (Expr) then
- Append_To (Args,
- Make_Pragma_Argument_Association (Loc,
- Expression => Relocate_Node (Expr)));
- end if;
-
- Make_Aitem_Pragma
- (Pragma_Argument_Associations => Args,
- Pragma_Name => Nam);
- end;
-
-- Cases where we do not delay, includes all cases where the
-- expression is missing other than the above cases.
- elsif not Delay_Required or else No (Expr) then
+ if not Delay_Required or else No (Expr) then
Make_Aitem_Pragma
(Pragma_Argument_Associations => New_List (
Make_Pragma_Argument_Association (Sloc (Ent),
when Aspect_Abstract_State |
Aspect_Annotate |
+ Aspect_Async_Readers |
+ Aspect_Async_Writers |
Aspect_Constant_After_Elaboration |
Aspect_Contract_Cases |
Aspect_Default_Initial_Condition |
Aspect_Depends |
Aspect_Dimension |
Aspect_Dimension_System |
+ Aspect_Effective_Reads |
+ Aspect_Effective_Writes |
Aspect_Extensions_Visible |
Aspect_Ghost |
Aspect_Global |
Aspect_Refined_State |
Aspect_SPARK_Mode |
Aspect_Test_Case |
- Aspect_Unimplemented =>
+ Aspect_Unimplemented |
+ Aspect_Volatile_Function =>
raise Program_Error;
end case;
if Ekind (Obj_Id) = E_Constant then
- -- A constant cannot be effectively volatile. This check is only
- -- relevant with SPARK_Mode on as it is not a standard Ada legality
- -- rule. Do not flag internally-generated constants that map generic
- -- formals to actuals in instantiations (SPARK RM 7.1.3(6)).
+ -- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)).
+ -- This check is relevant only when SPARK_Mode is on as it is not a
+ -- standard Ada legality rule. Internally-generated constants that
+ -- map generic formals to actuals in instantiations are allowed to
+ -- be volatile.
if SPARK_Mode = On
+ and then Comes_From_Source (Obj_Id)
and then Is_Effectively_Volatile (Obj_Id)
and then No (Corresponding_Generic_Association (Parent (Obj_Id)))
-
- -- Don't give this for internally generated entities (such as the
- -- FIRST and LAST temporaries generated for bounds).
-
- and then Comes_From_Source (Obj_Id)
then
Error_Msg_N ("constant cannot be volatile", Obj_Id);
end if;
else pragma Assert (Ekind (Obj_Id) = E_Variable);
- -- The following checks are only relevant when SPARK_Mode is on as
+ -- The following checks are relevant only when SPARK_Mode is on as
-- they are not standard Ada legality rules. Internally generated
-- temporaries are ignored.
if Is_Effectively_Volatile (Obj_Id) then
-- The declaration of an effectively volatile object must
- -- appear at the library level (SPARK RM 7.1.3(7), C.6(6)).
+ -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
if not Is_Library_Level_Entity (Obj_Id) then
Error_Msg_N
else
-- A non-effectively volatile object cannot have effectively
- -- volatile components (SPARK RM 7.1.3(7)).
+ -- volatile components (SPARK RM 7.1.3(6)).
if not Is_Effectively_Volatile (Obj_Id)
and then Has_Volatile_Component (Obj_Typ)
end if;
end if;
- -- A discriminant cannot be effectively volatile. This check is only
- -- relevant when SPARK_Mode is on as it is not standard Ada legality
- -- rule (SPARK RM 7.1.3(6)).
+ -- A discriminant cannot be effectively volatile (SPARK RM 7.1.3(6)).
+ -- This check is relevant only when SPARK_Mode is on as it is not a
+ -- standard Ada legality rule.
if SPARK_Mode = On
and then Is_Effectively_Volatile (Defining_Identifier (Discr))
end if;
end if;
- -- A loop parameter cannot be effectively volatile. This check is
- -- peformed only when SPARK_Mode is on as it is not a standard Ada
- -- legality check (SPARK RM 7.1.3(6)).
+ -- A loop parameter cannot be effectively volatile (SPARK RM 7.1.3(4)).
+ -- This check is relevant only when SPARK_Mode is on as it is not a
+ -- standard Ada legality check.
-- Not clear whether this applies to element iterators, where the
-- cursor is not an explicit entity ???
end;
end if;
- -- A loop parameter cannot be effectively volatile. This check is
- -- peformed only when SPARK_Mode is on as it is not a standard Ada
- -- legality check (SPARK RM 7.1.3(6)).
+ -- A loop parameter cannot be effectively volatile (SPARK RM 7.1.3(4)).
+ -- This check is relevant only when SPARK_Mode is on as it is not a
+ -- standard Ada legality check.
if SPARK_Mode = On and then Is_Effectively_Volatile (Id) then
Error_Msg_N ("loop parameter cannot be volatile", Id);
Check_Result_And_Post_State (Body_Id);
+ -- A stand alone non-volatile function body cannot have an effectively
+ -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
+ -- check is relevant only when SPARK_Mode is on as it is not a standard
+ -- legality rule. The check is performed here because Volatile_Function
+ -- is processed after the analysis of the related subprogram body.
+
+ if SPARK_Mode = On
+ and then Ekind_In (Body_Id, E_Function, E_Generic_Function)
+ and then not Is_Volatile_Function (Body_Id)
+ then
+ Check_Nonvolatile_Function_Profile (Body_Id);
+ end if;
+
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
Check_Result_And_Post_State (Subp_Id);
end if;
+ -- A non-volatile function cannot have an effectively volatile formal
+ -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
+ -- only when SPARK_Mode is on as it is not a standard legality rule. The
+ -- check is performed here because pragma Volatile_Function is processed
+ -- after the analysis of the related subprogram declaration.
+
+ if SPARK_Mode = On
+ and then Ekind_In (Subp_Id, E_Function, E_Generic_Function)
+ and then not Is_Volatile_Function (Subp_Id)
+ then
+ Check_Nonvolatile_Function_Profile (Subp_Id);
+ end if;
+
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
-- the check is applied later (see Analyze_Subprogram_Declaration).
if not Nkind_In (Original_Node (Parent (N)),
- N_Subprogram_Renaming_Declaration,
N_Abstract_Subprogram_Declaration,
- N_Formal_Abstract_Subprogram_Declaration)
+ N_Formal_Abstract_Subprogram_Declaration,
+ N_Subprogram_Renaming_Declaration)
then
if Is_Abstract_Type (Etype (Designator))
and then not Is_Interface (Etype (Designator))
-- Ada 2012 (AI-0073): Extend this test to subprograms with an
-- access result whose designated type is abstract.
- elsif Nkind (Result_Definition (N)) = N_Access_Definition
+ elsif Ada_Version >= Ada_2012
+ and then Nkind (Result_Definition (N)) = N_Access_Definition
and then
not Is_Class_Wide_Type (Designated_Type (Etype (Designator)))
and then Is_Abstract_Type (Designated_Type (Etype (Designator)))
- and then Ada_Version >= Ada_2012
then
- Error_Msg_N ("function whose access result designates "
- & "abstract type must be abstract", N);
+ Error_Msg_N
+ ("function whose access result designates abstract type "
+ & "must be abstract", N);
end if;
end if;
end if;
(T : List_Id;
Related_Nod : Node_Id)
is
- Context : constant Node_Id := Parent (Parent (T));
- Param_Spec : Node_Id;
- Formal : Entity_Id;
- Formal_Type : Entity_Id;
- Default : Node_Id;
- Ptype : Entity_Id;
-
- Num_Out_Params : Nat := 0;
- First_Out_Param : Entity_Id := Empty;
- -- Used for setting Is_Only_Out_Parameter
-
function Designates_From_Limited_With (Typ : Entity_Id) return Boolean;
-- Determine whether an access type designates a type coming from a
-- limited view.
and then Is_Class_Wide_Type (Etype (Prefix (D))));
end Is_Class_Wide_Default;
+ -- Local variables
+
+ Context : constant Node_Id := Parent (Parent (T));
+ Default : Node_Id;
+ Formal : Entity_Id;
+ Formal_Type : Entity_Id;
+ Param_Spec : Node_Id;
+ Ptype : Entity_Id;
+
+ Num_Out_Params : Nat := 0;
+ First_Out_Param : Entity_Id := Empty;
+ -- Used for setting Is_Only_Out_Parameter
+
-- Start of processing for Process_Formals
begin
Null_Exclusion_Static_Checks (Param_Spec);
end if;
- -- The following checks are relevant when SPARK_Mode is on as these
- -- are not standard Ada legality rules.
+ -- The following checks are relevant only when SPARK_Mode is on as
+ -- these are not standard Ada legality rules.
if SPARK_Mode = On then
if Ekind_In (Scope (Formal), E_Function, E_Generic_Function) then
Error_Msg_N
("function cannot have parameter of mode `OUT` or "
& "`IN OUT`", Formal);
-
- -- A function cannot have an effectively volatile formal
- -- parameter (SPARK RM 7.1.3(10)).
-
- elsif Is_Effectively_Volatile (Formal) then
- Error_Msg_N
- ("function cannot have a volatile formal parameter",
- Formal);
end if;
-- A procedure cannot have an effectively volatile formal
function Find_Related_Context
(Prag : Node_Id;
Do_Checks : Boolean := False) return Node_Id;
- -- Subsidiaty to the analysis of pragmas Constant_After_Elaboration and
+ -- Subsidiaty to the analysis of pragmas Async_Readers, Async_Writers,
+ -- Constant_After_Elaboration, Effective_Reads, Effective_Writers and
-- Part_Of. Find the first source declaration or statement found while
-- traversing the previous node chain starting from pragma Prag. If flag
-- Do_Checks is set, the routine reports duplicate pragmas. The routine
(N : Node_Id;
Expr_Val : out Boolean)
is
- Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N));
- Expr : constant Node_Id := Get_Pragma_Arg (Next (Arg1));
- Obj_Id : constant Entity_Id := Entity (Get_Pragma_Arg (Arg1));
-
- Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N));
+ Obj_Decl : constant Node_Id := Find_Related_Context (N);
+ Obj_Id : constant Entity_Id := Defining_Entity (Obj_Decl);
+ Expr : Node_Id;
begin
- -- Set the Ghost mode in effect from the pragma. Due to the delayed
- -- analysis of the pragma, the Ghost mode at point of declaration and
- -- point of analysis may not necessarely be the same. Use the mode in
- -- effect at the point of declaration.
-
- Set_Ghost_Mode (N);
Error_Msg_Name_1 := Pragma_Name (N);
-- An external property pragma must apply to an effectively volatile
Expr_Val := True;
- if Present (Expr) then
- Analyze_And_Resolve (Expr, Standard_Boolean);
+ if Present (Arg1) then
+ Expr := Get_Pragma_Arg (Arg1);
if Is_OK_Static_Expression (Expr) then
Expr_Val := Is_True (Expr_Value (Expr));
- else
- SPARK_Msg_N ("expression of % must be static", Expr);
end if;
end if;
-
- Ghost_Mode := Save_Ghost_Mode;
end Analyze_External_Property_In_Decl_Part;
---------------------------------
SPARK_Msg_N ("\use its constituents instead", Item);
return;
+ -- An external state cannot appear as a global item of a
+ -- nonvolatile function (SPARK RM 7.1.3(8)).
+
+ elsif Is_External_State (Item_Id)
+ and then Ekind_In (Spec_Id, E_Function, E_Generic_Function)
+ and then not Is_Volatile_Function (Spec_Id)
+ then
+ SPARK_Msg_NE
+ ("external state & cannot act as global item of "
+ & "nonvolatile function", Item, Item_Id);
+ return;
+
-- If the reference to the abstract state appears in an
-- enclosing package body that will eventually refine the
-- state, record the reference for future checks.
and then Is_Effectively_Volatile (Item_Id)
then
-- An effectively volatile object cannot appear as a global
- -- item of a function (SPARK RM 7.1.3(9)).
+ -- item of a nonvolatile function (SPARK RM 7.1.3(8)).
- if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
+ if Ekind_In (Spec_Id, E_Function, E_Generic_Function)
+ and then not Is_Volatile_Function (Spec_Id)
+ then
Error_Msg_NE
("volatile object & cannot act as global item of a "
& "function", Item, Item_Id);
-- In this version of the procedure, the identifier name is given as
-- a string with lower case letters.
+ procedure Check_Static_Boolean_Expression (Expr : Node_Id);
+ -- Subsidiary to the analysis of pragmas Async_Readers, Async_Writers,
+ -- Constant_After_Elaboration, Effective_Reads, Effective_Writes,
+ -- Extensions_Visible and Volatile_Function. Ensure that expression Expr
+ -- is an OK static boolean expression. Emit an error if this is not the
+ -- case.
+
procedure Check_Static_Constraint (Constr : Node_Id);
-- Constr is a constraint from an N_Subtype_Indication node from a
-- component constraint in an Unchecked_Union type. This routine checks
Check_Optional_Identifier (Arg, Name_Find);
end Check_Optional_Identifier;
+ -------------------------------------
+ -- Check_Static_Boolean_Expression --
+ -------------------------------------
+
+ procedure Check_Static_Boolean_Expression (Expr : Node_Id) is
+ begin
+ if Present (Expr) then
+ Analyze_And_Resolve (Expr, Standard_Boolean);
+
+ if not Is_OK_Static_Expression (Expr) then
+ Error_Pragma_Arg
+ ("expression of pragma % must be static", Expr);
+ end if;
+ end if;
+ end Check_Static_Boolean_Expression;
+
-----------------------------
-- Check_Static_Constraint --
-----------------------------
-- Async_Readers/Async_Writers/Effective_Reads/Effective_Writes --
------------------------------------------------------------------
- -- pragma Asynch_Readers ( object_LOCAL_NAME [, FLAG] );
- -- pragma Asynch_Writers ( object_LOCAL_NAME [, FLAG] );
- -- pragma Effective_Reads ( object_LOCAL_NAME [, FLAG] );
- -- pragma Effective_Writes ( object_LOCAL_NAME [, FLAG] );
-
- -- FLAG ::= boolean_EXPRESSION
+ -- pragma Asynch_Readers [ (boolean_EXPRESSION) ];
+ -- pragma Asynch_Writers [ (boolean_EXPRESSION) ];
+ -- pragma Effective_Reads [ (boolean_EXPRESSION) ];
+ -- pragma Effective_Writes [ (boolean_EXPRESSION) ];
when Pragma_Async_Readers |
Pragma_Async_Writers |
Pragma_Effective_Reads |
Pragma_Effective_Writes =>
Async_Effective : declare
- Duplic : Node_Id;
- Expr : Node_Id;
- Obj : Node_Id;
- Obj_Id : Entity_Id;
+ Obj_Decl : Node_Id;
+ Obj_Id : Entity_Id;
begin
GNAT_Pragma;
Check_No_Identifiers;
- Check_At_Least_N_Arguments (1);
- Check_At_Most_N_Arguments (2);
- Check_Arg_Is_Local_Name (Arg1);
- Error_Msg_Name_1 := Pname;
+ Check_At_Most_N_Arguments (1);
- Obj := Get_Pragma_Arg (Arg1);
- Expr := Get_Pragma_Arg (Arg2);
+ Obj_Decl := Find_Related_Context (N, Do_Checks => True);
+
+ -- Object declaration
+
+ if Nkind (Obj_Decl) = N_Object_Declaration then
+ null;
+
+ -- Otherwise the pragma is associated with an illegal construact
+
+ else
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ Obj_Id := Defining_Entity (Obj_Decl);
-- Perform minimal verification to ensure that the argument is at
-- least a variable. Subsequent finer grained checks will be done
-- at the end of the declarative region the contains the pragma.
- if Is_Entity_Name (Obj)
- and then Present (Entity (Obj))
- and then Ekind (Entity (Obj)) = E_Variable
- then
- Obj_Id := Entity (Obj);
+ if Ekind (Obj_Id) = E_Variable then
-- A pragma that applies to a Ghost entity becomes Ghost for
-- the purposes of legality checks and removal of ignored Ghost
Mark_Pragma_As_Ghost (N, Obj_Id);
- -- Detect a duplicate pragma. Note that it is not efficient to
- -- examine preceding statements as Boolean aspects may appear
- -- anywhere between the related object declaration and its
- -- freeze point. As an alternative, inspect the contents of the
- -- variable contract.
-
- Duplic := Get_Pragma (Obj_Id, Prag_Id);
+ -- Analyze the Boolean expression (if any)
- if Present (Duplic) then
- Error_Msg_Sloc := Sloc (Duplic);
- Error_Msg_N ("pragma % duplicates pragma declared #", N);
+ if Present (Arg1) then
+ Check_Static_Boolean_Expression (Get_Pragma_Arg (Arg1));
+ end if;
- -- No duplicate detected
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_External_Property_In_Decl_Part.
- else
- if Present (Expr) then
- Preanalyze_And_Resolve (Expr, Standard_Boolean);
- end if;
+ Add_Contract_Item (N, Obj_Id);
- -- Chain the pragma on the contract for further processing
- -- by Analyze_External_Property_In_Decl_Part.
+ -- Otherwise the external property applies to a constant
- Add_Contract_Item (N, Obj_Id);
- end if;
else
Error_Pragma ("pragma % must apply to a volatile object");
end if;
when Pragma_Constant_After_Elaboration => Constant_After_Elaboration :
declare
- Expr : Node_Id;
Obj_Decl : Node_Id;
Obj_Id : Entity_Id;
-- Analyze the Boolean expression (if any)
if Present (Arg1) then
- Expr := Get_Pragma_Arg (Arg1);
-
- Analyze_And_Resolve (Expr, Standard_Boolean);
-
- if not Is_OK_Static_Expression (Expr) then
- Error_Pragma_Arg
- ("expression of pragma % must be static", Expr);
- return;
- end if;
+ Check_Static_Boolean_Expression (Get_Pragma_Arg (Arg1));
end if;
-- Chain the pragma on the contract for completeness
-- the annotation must instantiate itself.
when Pragma_Extensions_Visible => Extensions_Visible : declare
- Expr : Node_Id;
Formal : Entity_Id;
Has_OK_Formal : Boolean := False;
Spec_Id : Entity_Id;
-- Analyze the Boolean expression (if any)
if Present (Arg1) then
- Expr := Expression (Get_Argument (N, Spec_Id));
-
- Analyze_And_Resolve (Expr, Standard_Boolean);
-
- if not Is_OK_Static_Expression (Expr) then
- Error_Pragma_Arg
- ("expression of pragma % must be static", Expr);
- return;
- end if;
+ Check_Static_Boolean_Expression
+ (Expression (Get_Argument (N, Spec_Id)));
end if;
-- Chain the pragma on the contract for completeness
when Pragma_Volatile =>
Process_Atomic_Independent_Shared_Volatile;
+ -------------------------
+ -- Volatile_Components --
+ -------------------------
+
+ -- pragma Volatile_Components (array_LOCAL_NAME);
+
+ -- Volatile is handled by the same circuit as Atomic_Components
+
--------------------------
-- Volatile_Full_Access --
--------------------------
GNAT_Pragma;
Process_Atomic_Independent_Shared_Volatile;
- -------------------------
- -- Volatile_Components --
- -------------------------
+ -----------------------
+ -- Volatile_Function --
+ -----------------------
- -- pragma Volatile_Components (array_LOCAL_NAME);
+ -- pragma Volatile_Function [ (boolean_EXPRESSION) ];
- -- Volatile is handled by the same circuit as Atomic_Components
+ when Pragma_Volatile_Function => Volatile_Function : declare
+ Over_Id : Entity_Id;
+ Spec_Id : Entity_Id;
+ Subp_Decl : Node_Id;
+
+ begin
+ GNAT_Pragma;
+ Check_No_Identifiers;
+ Check_At_Most_N_Arguments (1);
+
+ Subp_Decl :=
+ Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
+
+ -- Function instantiation
+
+ if Nkind (Subp_Decl) = N_Function_Instantiation then
+ null;
+
+ -- Generic subprogram
+
+ elsif Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
+ null;
+
+ -- Body acts as spec
+
+ elsif Nkind (Subp_Decl) = N_Subprogram_Body
+ and then No (Corresponding_Spec (Subp_Decl))
+ then
+ null;
+
+ -- Body stub acts as spec
+
+ elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
+ and then No (Corresponding_Spec_Of_Stub (Subp_Decl))
+ then
+ null;
+
+ -- Subprogram
+
+ elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then
+ null;
+
+ else
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ Spec_Id := Corresponding_Spec_Of (Subp_Decl);
+ Over_Id := Overridden_Operation (Spec_Id);
+
+ -- A pragma that applies to a Ghost entity becomes Ghost for the
+ -- purposes of legality checks and removal of ignored Ghost code.
+
+ Mark_Pragma_As_Ghost (N, Spec_Id);
+
+ -- A volatile function cannot override a non-volatile function
+ -- (SPARK RM 7.1.2(15)). Overriding checks are usually performed
+ -- in New_Overloaded_Entity, however at that point the pragma has
+ -- not been processed yet.
+
+ if Present (Over_Id)
+ and then not Is_Volatile_Function (Over_Id)
+ then
+ Error_Msg_N
+ ("incompatible volatile function values in effect", Spec_Id);
+
+ Error_Msg_Sloc := Sloc (Over_Id);
+ Error_Msg_N
+ ("\& declared # with Volatile_Function value `False`",
+ Spec_Id);
+
+ Error_Msg_Sloc := Sloc (Spec_Id);
+ Error_Msg_N
+ ("\overridden # with Volatile_Function value `True`",
+ Spec_Id);
+ end if;
+
+ -- Analyze the Boolean expression (if any)
+
+ if Present (Arg1) then
+ Check_Static_Boolean_Expression (Get_Pragma_Arg (Arg1));
+ end if;
+
+ Add_Contract_Item (N, Spec_Id);
+ end Volatile_Function;
----------------------
-- Warning_As_Error --
and then Nkind (Parent (Parent (N))) = N_Package_Body;
end Is_Elaboration_SPARK_Mode;
+ -----------------------
+ -- Is_Enabled_Pragma --
+ -----------------------
+
+ function Is_Enabled_Pragma (Prag : Node_Id) return Boolean is
+ Arg : Node_Id;
+
+ begin
+ if Present (Prag) then
+ Arg := First (Pragma_Argument_Associations (Prag));
+
+ if Present (Arg) then
+ return Is_True (Expr_Value (Get_Pragma_Arg (Arg)));
+
+ -- The lack of a Boolean argument automatically enables the pragma
+
+ else
+ return True;
+ end if;
+
+ -- The pragma is missing, therefore it is not enabled
+
+ else
+ return False;
+ end if;
+ end Is_Enabled_Pragma;
+
-----------------------------------------
-- Is_Non_Significant_Pragma_Reference --
-----------------------------------------
Pragma_Volatile => 0,
Pragma_Volatile_Components => 0,
Pragma_Volatile_Full_Access => 0,
+ Pragma_Volatile_Function => 0,
Pragma_Warning_As_Error => 0,
Pragma_Warnings => 0,
Pragma_Weak_External => 0,
-- Determine whether pragma SPARK_Mode appears in the statement part of a
-- package body.
+ function Is_Enabled_Pragma (Prag : Node_Id) return Boolean;
+ -- Determine whether a Boolean-like SPARK pragma Prag is enabled. To be
+ -- considered enabled, the pragma must either:
+ -- * Appear without its Boolean expression
+ -- * The Boolean expression evaluates to "True"
+ --
+ -- Boolean-like SPARK pragmas differ from pure Boolean Ada pragmas in that
+ -- their optional Boolean expression must be static and cannot benefit from
+ -- forward references. The following are Boolean-like SPARK pragmas:
+ -- Async_Readers
+ -- Async_Writers
+ -- Constant_After_Elaboration
+ -- Effective_Reads
+ -- Effective_Writes
+ -- Extensions_Visible
+ -- Volatile_Function
+
function Is_Non_Significant_Pragma_Reference (N : Node_Id) return Boolean;
-- The node N is a node for an entity and the issue is whether the
-- occurrence is a reference for the purposes of giving warnings about
-- actual to a nested call, since this constitutes a reading of
-- the parameter, which is not allowed.
- if Is_Entity_Name (A)
+ if Ada_Version = Ada_83
+ and then Is_Entity_Name (A)
and then Ekind (Entity (A)) = E_Out_Parameter
then
- if Ada_Version = Ada_83 then
- Error_Msg_N
- ("(Ada 83) illegal reading of out parameter", A);
-
- -- An effectively volatile OUT parameter cannot act as IN or
- -- IN OUT actual in a call (SPARK RM 7.1.3(11)).
-
- elsif SPARK_Mode = On
- and then Is_Effectively_Volatile (Entity (A))
- then
- Error_Msg_N
- ("illegal reading of volatile OUT parameter", A);
- end if;
+ Error_Msg_N ("(Ada 83) illegal reading of out parameter", A);
end if;
end if;
-- temporaries are ignored.
if SPARK_Mode = On
- and then Is_Effectively_Volatile_Object (A)
and then Comes_From_Source (A)
+ and then Is_Effectively_Volatile_Object (A)
then
-- An effectively volatile object may act as an actual
-- parameter when the corresponding formal is of a non-scalar
(Context : Node_Id;
Obj_Ref : Node_Id) return Boolean;
-- Determine whether node Context denotes a "non-interfering context"
- -- (as defined in SPARK RM 7.1.3(13)) where volatile reference Obj_Ref
+ -- (as defined in SPARK RM 7.1.3(12)) where volatile reference Obj_Ref
-- can safely reside.
----------------------------------------
function Within_Procedure_Call (Nod : Node_Id) return Boolean;
-- Determine whether an arbitrary node appears in a procedure call
+ function Within_Volatile_Function (Id : Entity_Id) return Boolean;
+ -- Determine whether an arbitrary entity appears in a volatile
+ -- function.
+
------------------
-- Within_Check --
------------------
return False;
end Within_Procedure_Call;
+ ------------------------------
+ -- Within_Volatile_Function --
+ ------------------------------
+
+ function Within_Volatile_Function (Id : Entity_Id) return Boolean is
+ Func_Id : Entity_Id;
+
+ begin
+ -- Traverse the scope stack looking for a [generic] function
+
+ Func_Id := Id;
+ while Present (Func_Id) and then Func_Id /= Standard_Standard loop
+ if Ekind_In (Func_Id, E_Function, E_Generic_Function) then
+ return Is_Volatile_Function (Func_Id);
+ end if;
+
+ Func_Id := Scope (Func_Id);
+ end loop;
+
+ return False;
+ end Within_Volatile_Function;
+
+ -- Local variables
+
+ Obj_Id : Entity_Id;
+
-- Start of processing for Is_OK_Volatile_Context
begin
return True;
-- The volatile object is part of the initialization expression of
- -- another object. Ensure that the climb of the parent chain came
- -- from the expression side and not from the name side.
+ -- another object.
elsif Nkind (Context) = N_Object_Declaration
and then Present (Expression (Context))
and then Expression (Context) = Obj_Ref
then
- return True;
+ Obj_Id := Defining_Entity (Context);
+
+ -- The volatile object acts as the initialization expression of an
+ -- extended return statement. This is valid context as long as the
+ -- function is volatile.
+
+ if Is_Return_Object (Obj_Id) then
+ return Within_Volatile_Function (Obj_Id);
+
+ -- Otherwise this is a normal object initialization
+
+ else
+ return True;
+ end if;
-- The volatile object appears as an actual parameter in a call to an
-- instance of Unchecked_Conversion whose result is renamed.
then
return True;
+ -- The volatile object appears as the expression of a simple return
+ -- statement that applies to a volatile function.
+
+ elsif Nkind (Context) = N_Simple_Return_Statement
+ and then Expression (Context) = Obj_Ref
+ then
+ return
+ Within_Volatile_Function (Return_Statement_Entity (Context));
+
-- The volatile object appears as the prefix of a name occurring
-- in a non-interfering context.
then
if Ada_Version = Ada_83 then
Error_Msg_N ("(Ada 83) illegal reading of out parameter", N);
-
- -- An effectively volatile OUT parameter cannot be read
- -- (SPARK RM 7.1.3(11)).
-
- elsif SPARK_Mode = On
- and then Is_Effectively_Volatile (E)
- then
- Error_Msg_N ("illegal reading of volatile OUT parameter", N);
end if;
-- In all other cases, just do the possible static evaluation
and then Comes_From_Source (N)
then
-- The effectively volatile objects appears in a "non-interfering
- -- context" as defined in SPARK RM 7.1.3(13).
+ -- context" as defined in SPARK RM 7.1.3(12).
if Is_OK_Volatile_Context (Par, N) then
null;
else
SPARK_Msg_N
("volatile object cannot appear in this context "
- & "(SPARK RM 7.1.3(13))", N);
+ & "(SPARK RM 7.1.3(12))", N);
end if;
end if;
-- Postcondition
-- Precondition
-- Test_Case
+ -- Volatile_Function
elsif Ekind_In (Id, E_Entry, E_Entry_Family)
or else Is_Generic_Subprogram (Id)
then
Add_Classification;
+ elsif Prag_Nam = Name_Volatile_Function
+ and then Ekind_In (Id, E_Function, E_Generic_Function)
+ then
+ Add_Classification;
+
-- The pragma is not a proper contract item
else
end if;
end Check_No_Hidden_State;
+ ----------------------------------------
+ -- Check_Nonvolatile_Function_Profile --
+ ----------------------------------------
+
+ procedure Check_Nonvolatile_Function_Profile (Func_Id : Entity_Id) is
+ Formal : Entity_Id;
+
+ begin
+ -- Inspect all formal parameters
+
+ Formal := First_Formal (Func_Id);
+ while Present (Formal) loop
+ if Is_Effectively_Volatile (Etype (Formal)) then
+ Error_Msg_NE
+ ("nonvolatile function & cannot have a volatile parameter",
+ Formal, Func_Id);
+ end if;
+
+ Next_Formal (Formal);
+ end loop;
+
+ -- Inspect the return type
+
+ if Is_Effectively_Volatile (Etype (Func_Id)) then
+ Error_Msg_N
+ ("nonvolatile function & cannot have a volatile return type",
+ Func_Id);
+ end if;
+ end Check_Nonvolatile_Function_Profile;
+
------------------------------------------
-- Check_Potentially_Blocking_Operation --
------------------------------------------
----------------
function Is_Enabled (Prag : Node_Id) return Boolean is
- Arg2 : Node_Id;
+ Arg1 : Node_Id;
begin
if Present (Prag) then
- Arg2 := Next (First (Pragma_Argument_Associations (Prag)));
+ Arg1 := First (Pragma_Argument_Associations (Prag));
-- The pragma has an optional Boolean expression, the related
-- property is enabled only when the expression evaluates to
-- True.
- if Present (Arg2) then
- return Is_True (Expr_Value (Get_Pragma_Arg (Arg2)));
+ if Present (Arg1) then
+ return Is_True (Expr_Value (Get_Pragma_Arg (Arg1)));
-- Otherwise the lack of expression enables the property by
-- default.
-----------------------------
function Is_Effectively_Volatile (Id : Entity_Id) return Boolean is
+ function Is_Descendant_Of_Suspension_Object
+ (Typ : Entity_Id) return Boolean;
+ -- Determine whether type Typ is a descendant of type Suspension_Object
+ -- defined in Ada.Synchronous_Task_Control. This routine is similar to
+ -- Sem_Util.Is_Descendent_Of, however this version does not load unit
+ -- Ada.Synchronous_Task_Control.
+
+ ----------------------------------------
+ -- Is_Descendant_Of_Suspension_Object --
+ ----------------------------------------
+
+ function Is_Descendant_Of_Suspension_Object
+ (Typ : Entity_Id) return Boolean
+ is
+ Cur_Typ : Entity_Id;
+ Par_Typ : Entity_Id;
+
+ begin
+ -- Do not attempt to load Ada.Synchronous_Task_Control in No_Run_Time
+ -- mode. The unit contains tagged types and those are not allowed in
+ -- this mode.
+
+ if No_Run_Time_Mode then
+ return False;
+
+ -- Unit Ada.Synchronous_Task_Control is not available, the type
+ -- cannot possibly be a descendant of Suspension_Object.
+
+ elsif not RTE_Available (RE_Suspension_Object) then
+ return False;
+ end if;
+
+ -- Climb the type derivation chain checking each parent type against
+ -- Suspension_Object.
+
+ Cur_Typ := Base_Type (Typ);
+ while Present (Cur_Typ) loop
+ Par_Typ := Etype (Cur_Typ);
+
+ -- The current type is a match
+
+ if Is_RTE (Cur_Typ, RE_Suspension_Object) then
+ return True;
+
+ -- Stop the traversal once the root of the derivation chain has
+ -- been reached. In that case the current type is its own base
+ -- type.
+
+ elsif Cur_Typ = Par_Typ then
+ exit;
+ end if;
+
+ Cur_Typ := Base_Type (Par_Typ);
+ end loop;
+
+ return False;
+ end Is_Descendant_Of_Suspension_Object;
+
+ -- Start of processing for Is_Effectively_Volatile
+
begin
if Is_Type (Id) then
or else
Is_Effectively_Volatile (Component_Type (Base_Type (Id)));
+ -- A protected type is always volatile
+
+ elsif Is_Protected_Type (Id) then
+ return True;
+
+ -- A descendant of Ada.Synchronous_Task_Control.Suspension_Object is
+ -- automatically volatile.
+
+ elsif Is_Descendant_Of_Suspension_Object (Id) then
+ return True;
+
+ -- Otherwise the type is not effectively volatile
+
else
return False;
end if;
and then Scope (Scope (Scope (Root))) = Standard_Standard;
end Is_Visibly_Controlled;
+ --------------------------
+ -- Is_Volatile_Function --
+ --------------------------
+
+ function Is_Volatile_Function (Func_Id : Entity_Id) return Boolean is
+ begin
+ -- The caller must ensure that Func_Id denotes a function
+
+ pragma Assert (Ekind_In (Func_Id, E_Function, E_Generic_Function));
+
+ -- A protected function is automatically volatile
+
+ if Is_Primitive (Func_Id)
+ and then Present (First_Formal (Func_Id))
+ and then Is_Protected_Type (Etype (First_Formal (Func_Id)))
+ then
+ return True;
+
+ -- Otherwise the function is treated as volatile if it is subject to
+ -- enabled pragma Volatile_Function.
+
+ else
+ return
+ Is_Enabled_Pragma (Get_Pragma (Func_Id, Pragma_Volatile_Function));
+ end if;
+ end Is_Volatile_Function;
+
------------------------
-- Is_Volatile_Object --
------------------------
-- Refined_Post
-- Refined_States
-- Test_Case
+ -- Volatile_Function
procedure Add_Global_Declaration (N : Node_Id);
-- These procedures adds a declaration N at the library level, to be
-- Determine whether object or state Id introduces a hidden state. If this
-- is the case, emit an error.
+ procedure Check_Nonvolatile_Function_Profile (Func_Id : Entity_Id);
+ -- Verify that the profile of nonvolatile function Func_Id does not contain
+ -- effectively volatile parameters or return type.
+
procedure Check_Potentially_Blocking_Operation (N : Node_Id);
-- N is one of the statement forms that is a potentially blocking
-- operation. If it appears within a protected action, emit warning.
function Enclosing_Declaration (N : Node_Id) return Node_Id;
-- Returns the declaration node enclosing N (including possibly N itself),
- -- if any, or Empty otherwise
+ -- if any, or Empty otherwise.
function Enclosing_Generic_Body
(N : Node_Id) return Node_Id;
-- . machine_emin = 3 - machine_emax
function Is_Effectively_Volatile (Id : Entity_Id) return Boolean;
- -- The SPARK property "effectively volatile" applies to both types and
- -- objects. To qualify as such, an entity must be either volatile or be
- -- (of) an array type subject to aspect Volatile_Components.
+ -- Determine whether a type or object denoted by entity Id is effectively
+ -- volatile (SPARK RM 7.1.2). To qualify as such, the entity must be either
+ -- * Volatile
+ -- * An array type subject to aspect Volatile_Components
+ -- * An array type whose component type is effectively volatile
+ -- * A protected type
+ -- * Descendant of type Ada.Synchronous_Task_Control.Suspension_Object
function Is_Effectively_Volatile_Object (N : Node_Id) return Boolean;
-- Determine whether an arbitrary node denotes an effectively volatile
- -- object.
+ -- object (SPARK RM 7.1.2).
function Is_Expression_Function (Subp : Entity_Id) return Boolean;
-- Predicate to determine whether a scope entity comes from a rewritten
function Is_EVF_Expression (N : Node_Id) return Boolean;
-- Determine whether node N denotes a reference to a formal parameter of
-- a specific tagged type whose related subprogram is subject to pragma
- -- Extensions_Visible with value "False". Several other constructs fall
- -- under this category:
+ -- Extensions_Visible with value "False" (SPARK RM 6.1.7). Several other
+ -- constructs fall under this category:
-- 1) A qualified expression whose operand is EVF
-- 2) A type conversion whose operand is EVF
-- 3) An if expression with at least one EVF dependent_expression
-- Initialize/Adjust/Finalize subprogram does not override the inherited
-- one.
+ function Is_Volatile_Function (Func_Id : Entity_Id) return Boolean;
+ -- Determine whether [generic] function Func_Id is subject to enabled
+ -- pragma Volatile_Function. Protected functions are treated as volatile
+ -- (SPARK RM 7.1.2).
+
function Is_Volatile_Object (N : Node_Id) return Boolean;
-- Determines if the given node denotes an volatile object in the sense of
-- the legality checks described in RM C.6(12). Note that the test here is
Name_Volatile : constant Name_Id := N + $;
Name_Volatile_Components : constant Name_Id := N + $;
Name_Volatile_Full_Access : constant Name_Id := N + $; -- GNAT
+ Name_Volatile_Function : constant Name_Id := N + $; -- GNAT
Name_Weak_External : constant Name_Id := N + $; -- GNAT
Last_Pragma_Name : constant Name_Id := N + $;
Pragma_Volatile,
Pragma_Volatile_Components,
Pragma_Volatile_Full_Access,
+ Pragma_Volatile_Function,
Pragma_Weak_External,
-- The following pragmas are on their own, out of order, because of the
projects / gcc.git / commitdiff