@@ -590,10 +590,6 @@ package body Contracts is
Items : constant Node_Id := Contract (Body_Id);
Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl);
- Saved_SM : constant SPARK_Mode_Type := SPARK_Mode;
- Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
- -- Save the SPARK_Mode-related data to restore on exit
-
begin
-- When a subprogram body declaration is illegal, its defining entity is
-- left unanalyzed. There is nothing left to do in this case because the
@@ -628,39 +624,11 @@ package body Contracts is
Analyze_Entry_Or_Subprogram_Contract (Corresponding_Spec (Body_Decl));
end if;
- -- Due to the timing of contract analysis, delayed pragmas may be
- -- subject to the wrong SPARK_Mode, usually that of the enclosing
- -- context. To remedy this, restore the original SPARK_Mode of the
- -- related subprogram body.
-
- Set_SPARK_Mode (Body_Id);
-
-- Ensure that the contract cases or postconditions mention 'Result or
-- define a post-state.
Check_Result_And_Post_State (Body_Id);
- -- A stand-alone nonvolatile 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. The
- -- check only applies to source subprograms and not to generated TSS
- -- subprograms.
-
- if SPARK_Mode = On
- and then Ekind (Body_Id) in E_Function | E_Generic_Function
- and then Comes_From_Source (Spec_Id)
- 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.
-
- Restore_SPARK_Mode (Saved_SM, Saved_SMP);
-
-- Capture all global references in a generic subprogram body now that
-- the contract has been analyzed.
@@ -865,20 +833,6 @@ package body Contracts is
Check_Result_And_Post_State (Subp_Id);
end if;
- -- A nonvolatile 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 (Subp_Id) in E_Function | E_Generic_Function
- and then Comes_From_Source (Subp_Id)
- 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.
@@ -902,19 +856,16 @@ package body Contracts is
(Type_Or_Obj_Id : Entity_Id)
is
Is_Type_Id : constant Boolean := Is_Type (Type_Or_Obj_Id);
- Decl_Kind : constant String :=
- (if Is_Type_Id then "type" else "object");
-- Local variables
- AR_Val : Boolean := False;
- AW_Val : Boolean := False;
- ER_Val : Boolean := False;
- EW_Val : Boolean := False;
- NC_Val : Boolean;
- Seen : Boolean := False;
- Prag : Node_Id;
- Obj_Typ : Entity_Id;
+ AR_Val : Boolean := False;
+ AW_Val : Boolean := False;
+ ER_Val : Boolean := False;
+ EW_Val : Boolean := False;
+ NC_Val : Boolean;
+ Seen : Boolean := False;
+ Prag : Node_Id;
-- Start of processing for Check_Type_Or_Object_External_Properties
@@ -922,8 +873,6 @@ package body Contracts is
-- Analyze all external properties
if Is_Type_Id then
- Obj_Typ := Type_Or_Obj_Id;
-
-- If the parent type of a derived type is volatile
-- then the derived type inherits volatility-related flags.
@@ -940,8 +889,6 @@ package body Contracts is
end if;
end;
end if;
- else
- Obj_Typ := Etype (Type_Or_Obj_Id);
end if;
Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Async_Readers);
@@ -1027,96 +974,6 @@ package body Contracts is
if Present (Prag) then
Analyze_External_Property_In_Decl_Part (Prag, NC_Val);
end if;
-
- -- The following checks are relevant only when SPARK_Mode is on, as
- -- they are not standard Ada legality rules. Internally generated
- -- temporaries are ignored, as well as return objects.
-
- if SPARK_Mode = On
- and then Comes_From_Source (Type_Or_Obj_Id)
- and then not Is_Return_Object (Type_Or_Obj_Id)
- then
- if Is_Effectively_Volatile (Type_Or_Obj_Id) then
-
- -- The declaration of an effectively volatile object or type must
- -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
-
- if not Is_Library_Level_Entity (Type_Or_Obj_Id) then
- Error_Msg_Code := GEC_Volatile_At_Library_Level;
- Error_Msg_N
- ("effectively volatile "
- & Decl_Kind
- & " & must be declared at library level '[[]']",
- Type_Or_Obj_Id);
-
- -- An object of a discriminated type cannot be effectively
- -- volatile except for protected objects (SPARK RM 7.1.3(5)).
-
- elsif Has_Discriminants (Obj_Typ)
- and then not Is_Protected_Type (Obj_Typ)
- then
- Error_Msg_N
- ("discriminated " & Decl_Kind & " & cannot be volatile",
- Type_Or_Obj_Id);
- end if;
-
- -- An object decl shall be compatible with respect to volatility
- -- with its type (SPARK RM 7.1.3(2)).
-
- if not Is_Type_Id then
- if Is_Effectively_Volatile (Obj_Typ) then
- Check_Volatility_Compatibility
- (Type_Or_Obj_Id, Obj_Typ,
- "volatile object", "its type",
- Srcpos_Bearer => Type_Or_Obj_Id);
- end if;
-
- -- A component of a composite type (in this case, the composite
- -- type is an array type) shall be compatible with respect to
- -- volatility with the composite type (SPARK RM 7.1.3(6)).
-
- elsif Is_Array_Type (Obj_Typ) then
- Check_Volatility_Compatibility
- (Component_Type (Obj_Typ), Obj_Typ,
- "component type", "its enclosing array type",
- Srcpos_Bearer => Obj_Typ);
-
- -- A component of a composite type (in this case, the composite
- -- type is a record type) shall be compatible with respect to
- -- volatility with the composite type (SPARK RM 7.1.3(6)).
-
- elsif Is_Record_Type (Obj_Typ) then
- declare
- Comp : Entity_Id := First_Component (Obj_Typ);
- begin
- while Present (Comp) loop
- Check_Volatility_Compatibility
- (Etype (Comp), Obj_Typ,
- "record component " & Get_Name_String (Chars (Comp)),
- "its enclosing record type",
- Srcpos_Bearer => Comp);
- Next_Component (Comp);
- end loop;
- end;
- end if;
-
- -- The type or object is not effectively volatile
-
- else
- -- A non-effectively volatile type cannot have effectively
- -- volatile components (SPARK RM 7.1.3(6)).
-
- if Is_Type_Id
- and then not Is_Effectively_Volatile (Type_Or_Obj_Id)
- and then Has_Effectively_Volatile_Component (Type_Or_Obj_Id)
- then
- Error_Msg_N
- ("non-volatile type & cannot have effectively volatile"
- & " components",
- Type_Or_Obj_Id);
- end if;
- end if;
- end if;
end Check_Type_Or_Object_External_Properties;
-----------------------------
@@ -1263,12 +1120,6 @@ package body Contracts is
if Yields_Synchronized_Object (Obj_Typ) then
Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id);
- -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and
- -- SPARK RM 6.9(19)).
-
- elsif SPARK_Mode = On and then Is_Effectively_Volatile (Obj_Id) then
- Error_Msg_N ("ghost object & cannot be volatile", Obj_Id);
-
-- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)).
-- One exception to this is the object that represents the dispatch
-- table of a Ghost tagged type, as the symbol needs to be exported.
@@ -5689,77 +5689,6 @@ package body Freeze is
end if;
end if;
- -- The following checks are relevant only when SPARK_Mode is on as
- -- they are not standard Ada legality rules.
-
- if SPARK_Mode = On then
-
- -- A discriminated type cannot be effectively volatile
- -- (SPARK RM 7.1.3(5)).
-
- if Is_Effectively_Volatile (Rec) then
- if Has_Discriminants (Rec) then
- Error_Msg_N ("discriminated type & cannot be volatile", Rec);
- end if;
-
- -- A non-effectively volatile record type cannot contain
- -- effectively volatile components (SPARK RM 7.1.3(6)).
-
- else
- Comp := First_Component (Rec);
- while Present (Comp) loop
- if Comes_From_Source (Comp)
- and then Is_Effectively_Volatile (Etype (Comp))
- then
- Error_Msg_Name_1 := Chars (Rec);
- Error_Msg_N
- ("component & of non-volatile type % cannot be "
- & "volatile", Comp);
- end if;
-
- Next_Component (Comp);
- end loop;
- end if;
-
- -- A type which does not yield a synchronized object cannot have
- -- a component that yields a synchronized object (SPARK RM 9.5).
-
- if not Yields_Synchronized_Object (Rec) then
- Comp := First_Component (Rec);
- while Present (Comp) loop
- if Comes_From_Source (Comp)
- and then Yields_Synchronized_Object (Etype (Comp))
- then
- Error_Msg_Name_1 := Chars (Rec);
- Error_Msg_N
- ("component & of non-synchronized type % cannot be "
- & "synchronized", Comp);
- end if;
-
- Next_Component (Comp);
- end loop;
- end if;
-
- -- A Ghost type cannot have a component of protected or task type
- -- (SPARK RM 6.9(19)).
-
- if Is_Ghost_Entity (Rec) then
- Comp := First_Component (Rec);
- while Present (Comp) loop
- if Comes_From_Source (Comp)
- and then Is_Concurrent_Type (Etype (Comp))
- then
- Error_Msg_Name_1 := Chars (Rec);
- Error_Msg_N
- ("component & of ghost type % cannot be concurrent",
- Comp);
- end if;
-
- Next_Component (Comp);
- end loop;
- end if;
- end if;
-
-- Make sure that if we have an iterator aspect, then we have
-- either Constant_Indexing or Variable_Indexing.
@@ -11526,19 +11526,6 @@ package body Sem_Ch12 is
Actual);
end if;
- -- Check actual/formal compatibility with respect to the four
- -- volatility refinement aspects.
-
- declare
- Actual_Obj : constant Entity_Id :=
- Get_Enclosing_Deep_Object (Actual);
- begin
- Check_Volatility_Compatibility
- (Actual_Obj, A_Gen_Obj, "actual object",
- "its corresponding formal object of mode in out",
- Srcpos_Bearer => Actual);
- end;
-
-- The actual for a ghost generic formal IN OUT parameter should be a
-- ghost object (SPARK RM 6.9(14)).
@@ -11746,22 +11733,6 @@ package body Sem_Ch12 is
("actual must exclude null to match generic formal#", Actual);
end if;
- -- 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, and also verifies that the actual is an object.
-
- if SPARK_Mode = On
- and then Present (Actual)
- and then Is_Object_Reference (Actual)
- and then Is_Effectively_Volatile_Object (Actual)
- and then not Is_Effectively_Volatile (A_Gen_Obj)
- then
- Error_Msg_N
- ("volatile object cannot act as actual in generic instantiation",
- Actual);
- end if;
-
return List;
end Instantiate_Object;
@@ -12944,14 +12915,6 @@ package body Sem_Ch12 is
("actual for& must have Independent_Components specified",
Actual, A_Gen_T);
end if;
-
- -- Check actual/formal compatibility with respect to the four
- -- volatility refinement aspects.
-
- Check_Volatility_Compatibility
- (Act_T, A_Gen_T,
- "actual type", "its corresponding formal type",
- Srcpos_Bearer => Actual);
end if;
end Check_Shared_Variable_Control_Aspects;
@@ -1442,26 +1442,6 @@ package body Sem_Ch3 is
end if;
Set_Etype (T, T);
-
- -- For SPARK, check that the designated type is compatible with
- -- respect to volatility with the access type.
-
- if SPARK_Mode /= Off
- and then Comes_From_Source (T)
- then
- -- ??? UNIMPLEMENTED
- -- In the case where the designated type is incomplete at this
- -- point, performing this check here is harmless but the check
- -- will need to be repeated when the designated type is complete.
-
- -- The preceding call to Comes_From_Source is needed because the
- -- FE sometimes introduces implicitly declared access types. See,
- -- for example, the expansion of nested_po.ads in OA28-015.
-
- Check_Volatility_Compatibility
- (Full_Desig, T, "designated type", "access type",
- Srcpos_Bearer => T);
- end if;
end if;
-- If the type has appeared already in a with_type clause, it is frozen
@@ -17337,29 +17317,6 @@ package body Sem_Ch3 is
begin
Parent_Type := Find_Type_Of_Subtype_Indic (Indic);
- if SPARK_Mode = On
- and then Is_Tagged_Type (Parent_Type)
- then
- declare
- Partial_View : constant Entity_Id :=
- Incomplete_Or_Partial_View (Parent_Type);
-
- begin
- -- If the partial view was not found then the parent type is not
- -- a private type. Otherwise check if the partial view is a tagged
- -- private type.
-
- if Present (Partial_View)
- and then Is_Private_Type (Partial_View)
- and then not Is_Tagged_Type (Partial_View)
- then
- Error_Msg_NE
- ("cannot derive from & declared as untagged private "
- & "(SPARK RM 3.4(1))", N, Partial_View);
- end if;
- end;
- end if;
-
-- Ada 2005 (AI-251): In case of interface derivation check that the
-- parent is also an interface.
@@ -21014,19 +20971,6 @@ package body Sem_Ch3 is
end if;
end if;
- -- A discriminant 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. The only way for a discriminant to be
- -- effectively volatile is to have an effectively volatile type, so
- -- we check this directly, because the Ekind of Discr might not be
- -- set yet (to help preventing cascaded errors on derived types).
-
- if SPARK_Mode = On
- and then Is_Effectively_Volatile (Discr_Type)
- then
- Error_Msg_N ("discriminant cannot be volatile", Discr);
- end if;
-
Next (Discr);
end loop;
@@ -3452,14 +3452,6 @@ package body Sem_Ch5 is
if Present (Iterator_Filter (N)) then
Preanalyze_And_Resolve (Iterator_Filter (N), Standard_Boolean);
end if;
-
- -- 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);
- end if;
end Analyze_Loop_Parameter_Specification;
----------------------------
@@ -1753,11 +1753,11 @@ package body Sem_Ch6 is
and then Ekind (Entity (Selector_Name (P)))
in E_Entry | E_Function | E_Procedure
then
- -- When front-end inlining is enabled, as with SPARK_Mode, a call
+ -- When front-end inlining is enabled, as with GNATprove mode, a call
-- in prefix notation may still be missing its controlling argument,
-- so perform the transformation now.
- if SPARK_Mode = On and then In_Inlined_Body then
+ if GNATprove_Mode and then In_Inlined_Body then
declare
Subp : constant Entity_Id := Entity (Selector_Name (P));
Typ : constant Entity_Id := Etype (Prefix (P));
@@ -2581,6 +2581,7 @@ package body Sem_Disp is
loop
Parent_Op := Overridden_Operation (Parent_Op);
exit when No (Parent_Op)
+ or else No (Find_DT (Parent_Op))
or else (No_Interfaces
and then Is_Interface (Find_DT (Parent_Op)));
@@ -2827,21 +2827,6 @@ package body Sem_Prag is
SPARK_Msg_N ("\use its constituents instead", Item);
return;
- -- An external state which has Async_Writers or
- -- Effective_Reads enabled cannot appear as a global item
- -- of a nonvolatile function (SPARK RM 7.1.3(8)).
-
- elsif Is_External_State (Item_Id)
- and then (Async_Writers_Enabled (Item_Id)
- or else Effective_Reads_Enabled (Item_Id))
- and then Ekind (Spec_Id) in 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.
@@ -2894,50 +2879,6 @@ package body Sem_Prag is
Item, Item_Id);
return;
end if;
-
- -- Variable related checks. These are only relevant when
- -- SPARK_Mode is on as they are not standard Ada legality
- -- rules.
-
- elsif SPARK_Mode = On
- and then Ekind (Item_Id) = E_Variable
- and then Is_Effectively_Volatile_For_Reading (Item_Id)
- then
- -- The current instance of a protected unit is not an
- -- effectively volatile object, unless the protected unit
- -- is already volatile for another reason (SPARK RM 7.1.2).
-
- if Is_Single_Protected_Object (Item_Id)
- and then Is_CCT_Instance (Etype (Item_Id), Spec_Id)
- and then not Is_Effectively_Volatile_For_Reading
- (Item_Id, Ignore_Protected => True)
- then
- null;
-
- -- An effectively volatile object for reading cannot appear
- -- as a global item of a nonvolatile function (SPARK RM
- -- 7.1.3(8)).
-
- elsif Ekind (Spec_Id) in 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);
- return;
-
- -- An effectively volatile object with external property
- -- Effective_Reads set to True must have mode Output or
- -- In_Out (SPARK RM 7.1.3(10)).
-
- elsif Effective_Reads_Enabled (Item_Id)
- and then Global_Mode = Name_Input
- then
- Error_Msg_NE
- ("volatile object & with property Effective_Reads must "
- & "have mode In_Out or Output", Item, Item_Id);
- return;
- end if;
end if;
-- When the item renames an entire object, replace the item
@@ -8128,27 +8069,6 @@ package body Sem_Prag is
Check_Full_Access_Only (E);
end if;
- -- The following check is only relevant when SPARK_Mode is on as
- -- this is not a standard Ada legality rule. Pragma Volatile can
- -- only apply to a full type declaration or an object declaration
- -- (SPARK RM 7.1.3(2)). Original_Node is necessary to account for
- -- untagged derived types that are rewritten as subtypes of their
- -- respective root types.
-
- if SPARK_Mode = On
- and then Prag_Id = Pragma_Volatile
- and then Nkind (Original_Node (Decl)) not in
- N_Full_Type_Declaration |
- N_Formal_Type_Declaration |
- N_Object_Declaration |
- N_Single_Protected_Declaration |
- N_Single_Task_Declaration
- then
- Error_Pragma_Arg
- ("argument of pragma % must denote a full type or object "
- & "declaration", Arg1);
- end if;
-
-- Deal with the case where the pragma/attribute is applied to a type
if Is_Type (E) then
@@ -3620,10 +3620,6 @@ package body Sem_Res is
-- interpretation, but the form of the actual can only be determined
-- once the primitive operation is identified.
- procedure Flag_Effectively_Volatile_Objects (Expr : Node_Id);
- -- Emit an error concerning the illegal usage of an effectively volatile
- -- object for reading in interfering context (SPARK RM 7.1.3(10)).
-
procedure Insert_Default;
-- If the actual is missing in a call, insert in the actuals list
-- an instance of the default expression. The insertion is always
@@ -3874,68 +3870,6 @@ package body Sem_Res is
end if;
end Check_Prefixed_Call;
- ---------------------------------------
- -- Flag_Effectively_Volatile_Objects --
- ---------------------------------------
-
- procedure Flag_Effectively_Volatile_Objects (Expr : Node_Id) is
- function Flag_Object (N : Node_Id) return Traverse_Result;
- -- Determine whether arbitrary node N denotes an effectively volatile
- -- object for reading and if it does, emit an error.
-
- -----------------
- -- Flag_Object --
- -----------------
-
- function Flag_Object (N : Node_Id) return Traverse_Result is
- Id : Entity_Id;
-
- begin
- case Nkind (N) is
- -- Do not consider nested function calls because they have
- -- already been processed during their own resolution.
-
- when N_Function_Call =>
- return Skip;
-
- when N_Identifier | N_Expanded_Name =>
- Id := Entity (N);
-
- -- Identifiers of components and discriminants are not names
- -- in the sense of Ada RM 4.1. They can only occur as a
- -- selector_name in selected_component or as a choice in
- -- component_association.
-
- if Present (Id)
- and then Is_Object (Id)
- and then Ekind (Id) not in E_Component | E_Discriminant
- and then Is_Effectively_Volatile_For_Reading (Id)
- and then
- not Is_OK_Volatile_Context (Context => Parent (N),
- Obj_Ref => N,
- Check_Actuals => True)
- then
- Error_Msg_Code := GEC_Volatile_Non_Interfering_Context;
- Error_Msg_N
- ("volatile object cannot appear in this context '[[]']",
- N);
- end if;
-
- return Skip;
-
- when others =>
- return OK;
- end case;
- end Flag_Object;
-
- procedure Flag_Objects is new Traverse_Proc (Flag_Object);
-
- -- Start of processing for Flag_Effectively_Volatile_Objects
-
- begin
- Flag_Objects (Expr);
- end Flag_Effectively_Volatile_Objects;
-
--------------------
-- Insert_Default --
--------------------
@@ -5128,22 +5062,6 @@ package body Sem_Res is
Check_Unset_Reference (A);
end if;
- -- The following checks are only relevant when SPARK_Mode is on as
- -- they are not standard Ada legality rule. Internally generated
- -- temporaries are ignored.
-
- if SPARK_Mode = On and then Comes_From_Source (A) then
-
- -- Inspect the expression and flag each effectively volatile
- -- object for reading as illegal because it appears within
- -- an interfering context. Note that this is usually done
- -- in Resolve_Entity_Name, but when the effectively volatile
- -- object for reading appears as an actual in a call, the call
- -- must be resolved first.
-
- Flag_Effectively_Volatile_Objects (A);
- end if;
-
-- A formal parameter of a specific tagged type whose related
-- subprogram is subject to pragma Extensions_Visible with value
-- "False" cannot act as an actual in a subprogram with value
@@ -8130,19 +8048,6 @@ package body Sem_Res is
if SPARK_Mode = On then
- -- An effectively volatile object for reading must appear in
- -- non-interfering context (SPARK RM 7.1.3(10)).
-
- if Is_Object (E)
- and then Is_Effectively_Volatile_For_Reading (E)
- and then
- not Is_OK_Volatile_Context (Par, N, Check_Actuals => False)
- then
- Error_Msg_Code := GEC_Volatile_Non_Interfering_Context;
- SPARK_Msg_N
- ("volatile object cannot appear in this context '[[]']", N);
- end if;
-
-- Parameters of modes OUT or IN OUT of the subprogram shall not
-- occur in the consequences of an exceptional contract unless
-- they are either passed by reference or occur in the prefix
@@ -3795,36 +3795,6 @@ package body Sem_Util is
end loop;
end Check_Inherited_Nonoverridable_Aspects;
- ----------------------------------------
- -- 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_For_Reading (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_For_Reading (Etype (Func_Id)) then
- Error_Msg_NE
- ("nonvolatile function & cannot have a volatile return type",
- Result_Definition (Parent (Func_Id)), Func_Id);
- end if;
- end Check_Nonvolatile_Function_Profile;
-
-------------------
-- Check_Parents --
-------------------
@@ -5153,96 +5123,6 @@ package body Sem_Util is
end if;
end Check_Unused_Body_States;
- ------------------------------------
- -- Check_Volatility_Compatibility --
- ------------------------------------
-
- procedure Check_Volatility_Compatibility
- (Id1, Id2 : Entity_Id;
- Description_1, Description_2 : String;
- Srcpos_Bearer : Node_Id) is
-
- begin
- if SPARK_Mode /= On then
- return;
- end if;
-
- declare
- AR1 : constant Boolean := Async_Readers_Enabled (Id1);
- AW1 : constant Boolean := Async_Writers_Enabled (Id1);
- ER1 : constant Boolean := Effective_Reads_Enabled (Id1);
- EW1 : constant Boolean := Effective_Writes_Enabled (Id1);
- AR2 : constant Boolean := Async_Readers_Enabled (Id2);
- AW2 : constant Boolean := Async_Writers_Enabled (Id2);
- ER2 : constant Boolean := Effective_Reads_Enabled (Id2);
- EW2 : constant Boolean := Effective_Writes_Enabled (Id2);
-
- AR_Check_Failed : constant Boolean := AR1 and not AR2;
- AW_Check_Failed : constant Boolean := AW1 and not AW2;
- ER_Check_Failed : constant Boolean := ER1 and not ER2;
- EW_Check_Failed : constant Boolean := EW1 and not EW2;
-
- package Failure_Description is
- procedure Note_If_Failure
- (Failed : Boolean; Aspect_Name : String);
- -- If Failed is False, do nothing.
- -- If Failed is True, add Aspect_Name to the failure description.
-
- function Failure_Text return String;
- -- returns accumulated list of failing aspects
- end Failure_Description;
-
- package body Failure_Description is
- Description_Buffer : Bounded_String;
-
- ---------------------
- -- Note_If_Failure --
- ---------------------
-
- procedure Note_If_Failure
- (Failed : Boolean; Aspect_Name : String) is
- begin
- if Failed then
- if Description_Buffer.Length /= 0 then
- Append (Description_Buffer, ", ");
- end if;
- Append (Description_Buffer, Aspect_Name);
- end if;
- end Note_If_Failure;
-
- ------------------
- -- Failure_Text --
- ------------------
-
- function Failure_Text return String is
- begin
- return +Description_Buffer;
- end Failure_Text;
- end Failure_Description;
-
- use Failure_Description;
- begin
- if AR_Check_Failed
- or AW_Check_Failed
- or ER_Check_Failed
- or EW_Check_Failed
- then
- Note_If_Failure (AR_Check_Failed, "Async_Readers");
- Note_If_Failure (AW_Check_Failed, "Async_Writers");
- Note_If_Failure (ER_Check_Failed, "Effective_Reads");
- Note_If_Failure (EW_Check_Failed, "Effective_Writes");
-
- Error_Msg_N
- (Description_1
- & " and "
- & Description_2
- & " are not compatible with respect to volatility due to "
- & Failure_Text,
- Srcpos_Bearer);
- end if;
- end;
- end Check_Volatility_Compatibility;
-
-----------------
-- Choice_List --
-----------------
@@ -19326,7 +19206,7 @@ package body Sem_Util is
-- An effectively volatile object may act as an actual when the
-- corresponding formal is of a non-scalar effectively volatile
- -- type (SPARK RM 7.1.3(10)).
+ -- type (SPARK RM 7.1.3(9)).
if not Is_Scalar_Type (Etype (Formal))
and then Is_Effectively_Volatile_For_Reading (Etype (Formal))
@@ -19335,7 +19215,7 @@ package body Sem_Util is
-- An effectively volatile object may act as an actual in a
-- call to an instance of Unchecked_Conversion. (SPARK RM
- -- 7.1.3(10)).
+ -- 7.1.3(9)).
elsif Is_Unchecked_Conversion_Instance (Subp) then
return True;
@@ -415,10 +415,6 @@ package Sem_Util is
-- In the error case, error message is associate with Inheritor;
-- Inheritor parameter is otherwise unused.
- 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 for reading.
-
function Check_Parents (N : Node_Id; List : Elist_Id) return Boolean;
-- Return True if all the occurrences of subtree N referencing entities in
-- the given List have the right value in their Parent field.
@@ -467,19 +463,6 @@ package Sem_Util is
-- and the context is external to the protected operation, to warn against
-- a possible unlocked access to data.
- procedure Check_Volatility_Compatibility
- (Id1, Id2 : Entity_Id;
- Description_1, Description_2 : String;
- Srcpos_Bearer : Node_Id);
- -- Id1 and Id2 should each be the entity of a state abstraction, a
- -- variable, or a type (i.e., something suitable for passing to
- -- Async_Readers_Enabled and similar functions).
- -- Does nothing if SPARK_Mode /= On. Otherwise, flags a legality violation
- -- if one or more of the four volatility-related aspects is False for Id1
- -- and True for Id2. The two descriptions are included in the error message
- -- text; the source position for the generated message is determined by
- -- Srcpos_Bearer.
-
function Choice_List (N : Node_Id) return List_Id;
-- Utility to retrieve the choices of a Component_Association or the
-- Discrete_Choices of an Iterated_Component_Association. For various
@@ -2199,7 +2182,7 @@ package Sem_Util is
Obj_Ref : Node_Id;
Check_Actuals : Boolean) return Boolean;
-- Determine whether node Context denotes a "non-interfering context" (as
- -- defined in SPARK RM 7.1.3(10)) where volatile reference Obj_Ref can
+ -- defined in SPARK RM 7.1.3(9)) where volatile reference Obj_Ref can
-- safely reside. When examining references that might be located within
-- actual parameters of a subprogram call that has not been resolved yet,
-- Check_Actuals should be False; such references will be assumed to be