[multiple changes]
2014-07-31 Hristian Kirtchev <kirtchev@adacore.com> * freeze.adb (Freeze_Record_Type): Replace all calls to Is_SPARK_Volatile with Is_Effectively_Volatile and update related comments. * sem_ch3.adb (Analyze_Object_Contract, Process_Discriminants): Replace all calls to Is_SPARK_Volatile with Is_Effectively_Volatile and update related comments. * sem_ch5.adb (Analyze_Iterator_Specification, Analyze_Loop_Parameter_Specification): Replace all calls to Is_SPARK_Volatile with Is_Effectively_Volatile and update related comments. * sem_ch6.adb (Process_Formals): Replace all calls to Is_SPARK_Volatile with Is_Effectively_Volatile and update related comments. * sem_ch12.adb (Instantiate_Object): Replace the call to Is_SPARK_Volatile_Object with Is_Effectively_Volatile_Object and update related comment. * sem_prag.adb (Analyze_External_Property_In_Decl_Part, Analyze_Global_Item): Replace all calls to Is_SPARK_Volatile with Is_Effectively_Volatile and update related comments. * sem_res.adb (Resolve_Actuals, Resolve_Entity_Name): Replace all calls to Is_SPARK_Volatile with Is_Effectively_Volatile and update related comments. * sem_util.adb (Has_Enabled_Property, Variable_Has_Enabled_Property): Replace all calls to Is_SPARK_Volatile with Is_Effectively_Volatile and update related comments. (Is_Effectively_Volatile): New routine. (Is_Effectively_Volatile_Object): New routine. (Is_SPARK_Volatile): Removed. (Is_SPARK_Volatile_Object): Removed. * sem_util.ads (Is_Effectively_Volatile): New routine. (Is_Effectively_Volatile_Object): New routine. (Is_SPARK_Volatile): Removed. (Is_SPARK_Volatile_Object): Removed. 2014-07-31 Pascal Obry <obry@adacore.com> * s-fileio.adb (Open): Make sure a shared file gets inserted into the global list atomically. This ensures that the file descriptor won't be freed because another tasks is closing the file. From-SVN: r213352
This commit is contained in:
parent
16b5e0b7c5
commit
d780e54fa0
@ -1,3 +1,46 @@
|
||||
2014-07-31 Hristian Kirtchev <kirtchev@adacore.com>
|
||||
|
||||
* freeze.adb (Freeze_Record_Type): Replace all calls to
|
||||
Is_SPARK_Volatile with Is_Effectively_Volatile and update
|
||||
related comments.
|
||||
* sem_ch3.adb (Analyze_Object_Contract, Process_Discriminants):
|
||||
Replace all calls to Is_SPARK_Volatile with
|
||||
Is_Effectively_Volatile and update related comments.
|
||||
* sem_ch5.adb (Analyze_Iterator_Specification,
|
||||
Analyze_Loop_Parameter_Specification): Replace all calls to
|
||||
Is_SPARK_Volatile with Is_Effectively_Volatile and update
|
||||
related comments.
|
||||
* sem_ch6.adb (Process_Formals): Replace all calls to
|
||||
Is_SPARK_Volatile with Is_Effectively_Volatile and update
|
||||
related comments.
|
||||
* sem_ch12.adb (Instantiate_Object): Replace the call to
|
||||
Is_SPARK_Volatile_Object with Is_Effectively_Volatile_Object
|
||||
and update related comment.
|
||||
* sem_prag.adb (Analyze_External_Property_In_Decl_Part,
|
||||
Analyze_Global_Item): Replace all calls to Is_SPARK_Volatile
|
||||
with Is_Effectively_Volatile and update related comments.
|
||||
* sem_res.adb (Resolve_Actuals, Resolve_Entity_Name): Replace
|
||||
all calls to Is_SPARK_Volatile with Is_Effectively_Volatile and
|
||||
update related comments.
|
||||
* sem_util.adb (Has_Enabled_Property,
|
||||
Variable_Has_Enabled_Property): Replace all calls
|
||||
to Is_SPARK_Volatile with Is_Effectively_Volatile and
|
||||
update related comments.
|
||||
(Is_Effectively_Volatile): New routine.
|
||||
(Is_Effectively_Volatile_Object): New routine.
|
||||
(Is_SPARK_Volatile): Removed.
|
||||
(Is_SPARK_Volatile_Object): Removed.
|
||||
* sem_util.ads (Is_Effectively_Volatile): New routine.
|
||||
(Is_Effectively_Volatile_Object): New routine.
|
||||
(Is_SPARK_Volatile): Removed.
|
||||
(Is_SPARK_Volatile_Object): Removed.
|
||||
|
||||
2014-07-31 Pascal Obry <obry@adacore.com>
|
||||
|
||||
* s-fileio.adb (Open): Make sure a shared file gets inserted into
|
||||
the global list atomically. This ensures that the file descriptor
|
||||
won't be freed because another tasks is closing the file.
|
||||
|
||||
2014-07-31 Robert Dewar <dewar@adacore.com>
|
||||
|
||||
* sem_ch3.adb (Process_Range_Expr_In_Decl): Add comments on
|
||||
|
@ -3472,27 +3472,29 @@ package body Freeze is
|
||||
-- they are not standard Ada legality rules.
|
||||
|
||||
if SPARK_Mode = On then
|
||||
if Is_SPARK_Volatile (Rec) then
|
||||
if Is_Effectively_Volatile (Rec) then
|
||||
|
||||
-- A discriminated type cannot be volatile (SPARK RM C.6(4))
|
||||
-- A discriminated type cannot be effectively volatile
|
||||
-- (SPARK RM C.6(4)).
|
||||
|
||||
if Has_Discriminants (Rec) then
|
||||
Error_Msg_N ("discriminated type & cannot be volatile", Rec);
|
||||
|
||||
-- A tagged type cannot be volatile (SPARK RM C.6(5))
|
||||
-- A tagged type cannot be effectively volatile
|
||||
-- (SPARK RM C.6(5)).
|
||||
|
||||
elsif Is_Tagged_Type (Rec) then
|
||||
Error_Msg_N ("tagged type & cannot be volatile", Rec);
|
||||
end if;
|
||||
|
||||
-- A non-volatile record type cannot contain volatile components
|
||||
-- (SPARK RM C.6(2))
|
||||
-- A non-effectively volatile record type cannot contain
|
||||
-- effectively volatile components (SPARK RM C.6(2)).
|
||||
|
||||
else
|
||||
Comp := First_Component (Rec);
|
||||
while Present (Comp) loop
|
||||
if Comes_From_Source (Comp)
|
||||
and then Is_SPARK_Volatile (Etype (Comp))
|
||||
and then Is_Effectively_Volatile (Etype (Comp))
|
||||
then
|
||||
Error_Msg_Name_1 := Chars (Rec);
|
||||
Error_Msg_N
|
||||
|
@ -933,6 +933,11 @@ package body System.File_IO is
|
||||
pragma Import (C, Get_Case_Sensitive,
|
||||
"__gnat_get_file_names_case_sensitive");
|
||||
|
||||
procedure Record_AFCB;
|
||||
-- Create and record new AFCB into the runtime, note that the
|
||||
-- implementation uses the variables below which corresponds to the
|
||||
-- status of the opened file.
|
||||
|
||||
File_Names_Case_Sensitive : constant Boolean := Get_Case_Sensitive /= 0;
|
||||
-- Set to indicate whether the operating system convention is for file
|
||||
-- names to be case sensitive (e.g., in Unix, set True), or not case
|
||||
@ -975,6 +980,33 @@ package body System.File_IO is
|
||||
Encoding : CRTL.Filename_Encoding;
|
||||
-- Filename encoding specified into the form parameter
|
||||
|
||||
------------------
|
||||
-- Record_AFCB --
|
||||
------------------
|
||||
|
||||
procedure Record_AFCB is
|
||||
begin
|
||||
File_Ptr := AFCB_Allocate (Dummy_FCB);
|
||||
|
||||
File_Ptr.Is_Regular_File :=
|
||||
(is_regular_file (fileno (Stream)) /= 0);
|
||||
File_Ptr.Is_System_File := False;
|
||||
File_Ptr.Text_Encoding := Text_Encoding;
|
||||
File_Ptr.Shared_Status := Shared;
|
||||
File_Ptr.Access_Method := Amethod;
|
||||
File_Ptr.Stream := Stream;
|
||||
File_Ptr.Form :=
|
||||
new String'(Formstr);
|
||||
File_Ptr.Name :=
|
||||
new String'(Fullname (1 .. Full_Name_Len));
|
||||
File_Ptr.Mode := Mode;
|
||||
File_Ptr.Is_Temporary_File := Tempfile;
|
||||
File_Ptr.Encoding := Encoding;
|
||||
|
||||
Chain_File (File_Ptr);
|
||||
Append_Set (File_Ptr);
|
||||
end Record_AFCB;
|
||||
|
||||
begin
|
||||
if File_Ptr /= null then
|
||||
raise Status_Error with "file already open";
|
||||
@ -1156,17 +1188,6 @@ package body System.File_IO is
|
||||
To_Lower (Fullname (1 .. Full_Name_Len));
|
||||
end if;
|
||||
|
||||
-- We need to lock all tasks from this point. This is needed as in
|
||||
-- the case of a shared file we want to ensure that the file is
|
||||
-- inserted into the chain with the shared status. We must be sure
|
||||
-- that this file won't be closed (and then the runtime file
|
||||
-- descriptor removed from the chain and released) before we leave
|
||||
-- this routine.
|
||||
|
||||
-- Take a task lock to protect Open_Files
|
||||
|
||||
SSL.Lock_Task.all;
|
||||
|
||||
-- If Shared=None or Shared=Yes, then check for the existence of
|
||||
-- another file with exactly the same full name.
|
||||
|
||||
@ -1175,6 +1196,10 @@ package body System.File_IO is
|
||||
P : AFCB_Ptr;
|
||||
|
||||
begin
|
||||
-- Take a task lock to protect Open_Files
|
||||
|
||||
SSL.Lock_Task.all;
|
||||
|
||||
-- Search list of open files
|
||||
|
||||
P := Open_Files;
|
||||
@ -1198,6 +1223,9 @@ package body System.File_IO is
|
||||
and then P.Shared_Status = Yes
|
||||
then
|
||||
Stream := P.Stream;
|
||||
|
||||
Record_AFCB;
|
||||
|
||||
exit;
|
||||
|
||||
-- Otherwise one of the files has Shared=Yes and one has
|
||||
@ -1214,12 +1242,23 @@ package body System.File_IO is
|
||||
|
||||
P := P.Next;
|
||||
end loop;
|
||||
|
||||
SSL.Unlock_Task.all;
|
||||
|
||||
exception
|
||||
when others =>
|
||||
SSL.Unlock_Task.all;
|
||||
raise;
|
||||
end;
|
||||
end if;
|
||||
|
||||
-- Open specified file if we did not find an existing stream
|
||||
-- Open specified file if we did not find an existing stream,
|
||||
-- otherwise we just return as there is nothing more to be done.
|
||||
|
||||
if Stream = NULL_Stream then
|
||||
if Stream /= NULL_Stream then
|
||||
return;
|
||||
|
||||
else
|
||||
Fopen_Mode
|
||||
(Mode, Text_Encoding in Text_Content_Encoding,
|
||||
Creat, Amethod, Fopstr);
|
||||
@ -1292,32 +1331,7 @@ package body System.File_IO is
|
||||
-- committed to completing the opening of the file. Allocate block on
|
||||
-- heap and fill in its fields.
|
||||
|
||||
File_Ptr := AFCB_Allocate (Dummy_FCB);
|
||||
|
||||
File_Ptr.Is_Regular_File := (is_regular_file (fileno (Stream)) /= 0);
|
||||
File_Ptr.Is_System_File := False;
|
||||
File_Ptr.Text_Encoding := Text_Encoding;
|
||||
File_Ptr.Shared_Status := Shared;
|
||||
File_Ptr.Access_Method := Amethod;
|
||||
File_Ptr.Stream := Stream;
|
||||
File_Ptr.Form := new String'(Formstr);
|
||||
File_Ptr.Name := new String'(Fullname (1 .. Full_Name_Len));
|
||||
File_Ptr.Mode := Mode;
|
||||
File_Ptr.Is_Temporary_File := Tempfile;
|
||||
File_Ptr.Encoding := Encoding;
|
||||
|
||||
Chain_File (File_Ptr);
|
||||
Append_Set (File_Ptr);
|
||||
|
||||
-- We can now safely release the global lock, as the File_Ptr is
|
||||
-- inserted into the global file list.
|
||||
|
||||
SSL.Unlock_Task.all;
|
||||
|
||||
exception
|
||||
when others =>
|
||||
SSL.Unlock_Task.all;
|
||||
raise;
|
||||
Record_AFCB;
|
||||
end Open;
|
||||
|
||||
------------------------
|
||||
|
@ -9905,13 +9905,13 @@ package body Sem_Ch12 is
|
||||
("actual must exclude null to match generic formal#", Actual);
|
||||
end if;
|
||||
|
||||
-- A 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 instance. The following check is only relevant 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_SPARK_Volatile_Object (Actual)
|
||||
and then Is_Effectively_Volatile_Object (Actual)
|
||||
then
|
||||
Error_Msg_N
|
||||
("volatile object cannot act as actual in generic instantiation "
|
||||
|
@ -3018,13 +3018,13 @@ package body Sem_Ch3 is
|
||||
begin
|
||||
if Ekind (Obj_Id) = E_Constant then
|
||||
|
||||
-- A constant cannot be volatile. This check is only relevant when
|
||||
-- SPARK_Mode is on as it is not 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. 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)).
|
||||
|
||||
if SPARK_Mode = On
|
||||
and then Is_SPARK_Volatile (Obj_Id)
|
||||
and then Is_Effectively_Volatile (Obj_Id)
|
||||
and then No (Corresponding_Generic_Association (Parent (Obj_Id)))
|
||||
then
|
||||
Error_Msg_N ("constant cannot be volatile", Obj_Id);
|
||||
@ -3036,37 +3036,37 @@ package body Sem_Ch3 is
|
||||
-- they are not standard Ada legality rules.
|
||||
|
||||
if SPARK_Mode = On then
|
||||
if Is_SPARK_Volatile (Obj_Id) then
|
||||
if Is_Effectively_Volatile (Obj_Id) then
|
||||
|
||||
-- The declaration of a volatile object must appear at the
|
||||
-- library level (SPARK RM 7.1.3(7), C.6(6)).
|
||||
-- The declaration of an effectively volatile object must
|
||||
-- appear at the library level (SPARK RM 7.1.3(7), C.6(6)).
|
||||
|
||||
if not Is_Library_Level_Entity (Obj_Id) then
|
||||
Error_Msg_N
|
||||
("volatile variable & must be declared at library level",
|
||||
Obj_Id);
|
||||
|
||||
-- An object of a discriminated type cannot be volatile
|
||||
-- (SPARK RM C.6(4)).
|
||||
-- An object of a discriminated type cannot be effectively
|
||||
-- volatile (SPARK RM C.6(4)).
|
||||
|
||||
elsif Has_Discriminants (Obj_Typ) then
|
||||
Error_Msg_N
|
||||
("discriminated object & cannot be volatile", Obj_Id);
|
||||
|
||||
-- An object of a tagged type cannot be volatile
|
||||
-- An object of a tagged type cannot be effectively volatile
|
||||
-- (SPARK RM C.6(5)).
|
||||
|
||||
elsif Is_Tagged_Type (Obj_Typ) then
|
||||
Error_Msg_N ("tagged object & cannot be volatile", Obj_Id);
|
||||
end if;
|
||||
|
||||
-- The object is not volatile
|
||||
-- The object is not effectively volatile
|
||||
|
||||
else
|
||||
-- A non-volatile object cannot have volatile components
|
||||
-- (SPARK RM 7.1.3(7)).
|
||||
-- A non-effectively volatile object cannot have effectively
|
||||
-- volatile components (SPARK RM 7.1.3(7)).
|
||||
|
||||
if not Is_SPARK_Volatile (Obj_Id)
|
||||
if not Is_Effectively_Volatile (Obj_Id)
|
||||
and then Has_Volatile_Component (Obj_Typ)
|
||||
then
|
||||
Error_Msg_N
|
||||
@ -18123,12 +18123,12 @@ package body Sem_Ch3 is
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- A discriminant cannot be 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. This check is only
|
||||
-- relevant when SPARK_Mode is on as it is not standard Ada legality
|
||||
-- rule (SPARK RM 7.1.3(6)).
|
||||
|
||||
if SPARK_Mode = On
|
||||
and then Is_SPARK_Volatile (Defining_Identifier (Discr))
|
||||
and then Is_Effectively_Volatile (Defining_Identifier (Discr))
|
||||
then
|
||||
Error_Msg_N ("discriminant cannot be volatile", Discr);
|
||||
end if;
|
||||
|
@ -2007,16 +2007,16 @@ package body Sem_Ch5 is
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- A loop parameter cannot be 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. 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)).
|
||||
|
||||
-- Not clear whether this applies to element iterators, where the
|
||||
-- cursor is not an explicit entity ???
|
||||
|
||||
if SPARK_Mode = On
|
||||
and then not Of_Present (N)
|
||||
and then Is_SPARK_Volatile (Ent)
|
||||
and then Is_Effectively_Volatile (Ent)
|
||||
then
|
||||
Error_Msg_N ("loop parameter cannot be volatile", Ent);
|
||||
end if;
|
||||
@ -2732,11 +2732,11 @@ package body Sem_Ch5 is
|
||||
end;
|
||||
end if;
|
||||
|
||||
-- A loop parameter cannot be 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. 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)).
|
||||
|
||||
if SPARK_Mode = On and then Is_SPARK_Volatile (Id) then
|
||||
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;
|
||||
|
@ -10095,21 +10095,22 @@ package body Sem_Ch6 is
|
||||
("function cannot have parameter of mode `OUT` or "
|
||||
& "`IN OUT`", Formal);
|
||||
|
||||
-- A function cannot have a volatile formal parameter
|
||||
-- (SPARK RM 7.1.3(10)).
|
||||
-- A function cannot have an effectively volatile formal
|
||||
-- parameter (SPARK RM 7.1.3(10)).
|
||||
|
||||
elsif Is_SPARK_Volatile (Formal) then
|
||||
elsif Is_Effectively_Volatile (Formal) then
|
||||
Error_Msg_N
|
||||
("function cannot have a volatile formal parameter",
|
||||
Formal);
|
||||
end if;
|
||||
|
||||
-- A procedure cannot have a formal parameter of mode IN because
|
||||
-- it behaves as a constant (SPARK RM 7.1.3(6)).
|
||||
-- A procedure cannot have an effectively volatile formal
|
||||
-- parameter of mode IN because it behaves as a constant
|
||||
-- (SPARK RM 7.1.3(6)).
|
||||
|
||||
elsif Ekind (Scope (Formal)) = E_Procedure
|
||||
and then Ekind (Formal) = E_In_Parameter
|
||||
and then Is_SPARK_Volatile (Formal)
|
||||
and then Is_Effectively_Volatile (Formal)
|
||||
then
|
||||
Error_Msg_N
|
||||
("formal parameter of mode `IN` cannot be volatile", Formal);
|
||||
|
@ -1830,16 +1830,16 @@ package body Sem_Prag is
|
||||
begin
|
||||
Error_Msg_Name_1 := Pragma_Name (N);
|
||||
|
||||
-- An external property pragma must apply to a volatile object other
|
||||
-- than a formal subprogram parameter (SPARK RM 7.1.3(2)). The check
|
||||
-- is performed at the end of the declarative region due to a possible
|
||||
-- out-of-order arrangement of pragmas:
|
||||
-- An external property pragma must apply to an effectively volatile
|
||||
-- object other than a formal subprogram parameter (SPARK RM 7.1.3(2)).
|
||||
-- The check is performed at the end of the declarative region due to a
|
||||
-- possible out-of-order arrangement of pragmas:
|
||||
|
||||
-- Obj : ...;
|
||||
-- pragma Async_Readers (Obj);
|
||||
-- pragma Volatile (Obj);
|
||||
|
||||
if not Is_SPARK_Volatile (Obj_Id) then
|
||||
if not Is_Effectively_Volatile (Obj_Id) then
|
||||
SPARK_Msg_N
|
||||
("external property % must apply to a volatile object", N);
|
||||
end if;
|
||||
@ -2021,10 +2021,11 @@ package body Sem_Prag is
|
||||
-- SPARK_Mode is on as they are not standard Ada legality
|
||||
-- rules.
|
||||
|
||||
elsif SPARK_Mode = On and then Is_SPARK_Volatile (Item_Id) then
|
||||
|
||||
-- A volatile object cannot appear as a global item of a
|
||||
-- function (SPARK RM 7.1.3(9)).
|
||||
elsif SPARK_Mode = On
|
||||
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)).
|
||||
|
||||
if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
|
||||
Error_Msg_NE
|
||||
@ -2032,8 +2033,9 @@ package body Sem_Prag is
|
||||
& "function", Item, Item_Id);
|
||||
return;
|
||||
|
||||
-- A volatile object with property Effective_Reads set to
|
||||
-- True must have mode Output or In_Out.
|
||||
-- An effectively volatile object with external property
|
||||
-- Effective_Reads set to True must have mode Output or
|
||||
-- In_Out.
|
||||
|
||||
elsif Effective_Reads_Enabled (Item_Id)
|
||||
and then Global_Mode = Name_Input
|
||||
|
@ -4329,18 +4329,19 @@ package body Sem_Res is
|
||||
-- they are not standard Ada legality rule.
|
||||
|
||||
if SPARK_Mode = On
|
||||
and then Is_SPARK_Volatile_Object (A)
|
||||
and then Is_Effectively_Volatile_Object (A)
|
||||
then
|
||||
-- A volatile object may act as an actual parameter when the
|
||||
-- corresponding formal is of a non-scalar volatile type.
|
||||
-- An effectively volatile object may act as an actual
|
||||
-- parameter when the corresponding formal is of a non-scalar
|
||||
-- volatile type.
|
||||
|
||||
if Is_Volatile (Etype (F))
|
||||
and then not Is_Scalar_Type (Etype (F))
|
||||
then
|
||||
null;
|
||||
|
||||
-- A volatile object may act as an actual parameter in a call
|
||||
-- to an instance of Unchecked_Conversion.
|
||||
-- An effectively volatile object may act as an actual
|
||||
-- parameter in a call to an instance of Unchecked_Conversion.
|
||||
|
||||
elsif Is_Unchecked_Conversion_Instance (Nam) then
|
||||
null;
|
||||
@ -6785,33 +6786,33 @@ package body Sem_Res is
|
||||
Eval_Entity_Name (N);
|
||||
end if;
|
||||
|
||||
-- A volatile object subject to enabled properties Async_Writers or
|
||||
-- Effective_Reads must appear in a specific context. The following
|
||||
-- checks are only relevant when SPARK_Mode is on as they are not
|
||||
-- standard Ada legality rules.
|
||||
-- An effectively volatile object subject to enabled properties
|
||||
-- Async_Writers or Effective_Reads must appear in a specific context.
|
||||
-- The following checks are only relevant when SPARK_Mode is on as they
|
||||
-- are not standard Ada legality rules.
|
||||
|
||||
if SPARK_Mode = On
|
||||
and then Is_Object (E)
|
||||
and then Is_SPARK_Volatile (E)
|
||||
and then Is_Effectively_Volatile (E)
|
||||
and then Comes_From_Source (E)
|
||||
and then
|
||||
(Async_Writers_Enabled (E) or else Effective_Reads_Enabled (E))
|
||||
then
|
||||
-- The volatile objects appears in a "non-interfering context" as
|
||||
-- defined in SPARK RM 7.1.3(13).
|
||||
-- The effectively volatile objects appears in a "non-interfering
|
||||
-- context" as defined in SPARK RM 7.1.3(13).
|
||||
|
||||
if Is_OK_Volatile_Context (Par, N) then
|
||||
null;
|
||||
|
||||
-- Assume that references to volatile objects that appear as actual
|
||||
-- parameters in a procedure call are always legal. The full legality
|
||||
-- check is done when the actuals are resolved.
|
||||
-- Assume that references to effectively volatile objects that appear
|
||||
-- as actual parameters in a procedure call are always legal. The
|
||||
-- full legality check is done when the actuals are resolved.
|
||||
|
||||
elsif Nkind (Par) = N_Procedure_Call_Statement then
|
||||
null;
|
||||
|
||||
-- Otherwise the context causes a side effect with respect to the
|
||||
-- volatile object.
|
||||
-- effectively volatile object.
|
||||
|
||||
else
|
||||
Error_Msg_N
|
||||
|
@ -7605,9 +7605,10 @@ package body Sem_Util is
|
||||
-- Start of processing for Variable_Has_Enabled_Property
|
||||
|
||||
begin
|
||||
-- A non-volatile object can never possess external properties
|
||||
-- A non-effectively volatile object can never possess external
|
||||
-- properties.
|
||||
|
||||
if not Is_SPARK_Volatile (Item_Id) then
|
||||
if not Is_Effectively_Volatile (Item_Id) then
|
||||
return False;
|
||||
|
||||
-- External properties related to variables come in two flavors -
|
||||
@ -7650,10 +7651,11 @@ package body Sem_Util is
|
||||
elsif Ekind (Item_Id) = E_Variable then
|
||||
return Variable_Has_Enabled_Property;
|
||||
|
||||
-- Otherwise a property is enabled when the related object is volatile
|
||||
-- Otherwise a property is enabled when the related item is effectively
|
||||
-- volatile.
|
||||
|
||||
else
|
||||
return Is_SPARK_Volatile (Item_Id);
|
||||
return Is_Effectively_Volatile (Item_Id);
|
||||
end if;
|
||||
end Has_Enabled_Property;
|
||||
|
||||
@ -10117,6 +10119,67 @@ package body Sem_Util is
|
||||
end if;
|
||||
end Is_Descendent_Of;
|
||||
|
||||
-----------------------------
|
||||
-- Is_Effectively_Volatile --
|
||||
-----------------------------
|
||||
|
||||
function Is_Effectively_Volatile (Id : Entity_Id) return Boolean is
|
||||
begin
|
||||
if Is_Type (Id) then
|
||||
|
||||
-- An arbitrary type is effectively volatile when it is subject to
|
||||
-- pragma Atomic or Volatile.
|
||||
|
||||
if Is_Volatile (Id) then
|
||||
return True;
|
||||
|
||||
-- An array type is effectively volatile when it is subject to pragma
|
||||
-- Atomic_Components or Volatile_Components or its compolent type is
|
||||
-- effectively volatile.
|
||||
|
||||
elsif Is_Array_Type (Id) then
|
||||
return
|
||||
Has_Volatile_Components (Id)
|
||||
or else
|
||||
Is_Effectively_Volatile (Component_Type (Base_Type (Id)));
|
||||
|
||||
else
|
||||
return False;
|
||||
end if;
|
||||
|
||||
-- Otherwise Id denotes an object
|
||||
|
||||
else
|
||||
return Is_Volatile (Id) or else Is_Effectively_Volatile (Etype (Id));
|
||||
end if;
|
||||
end Is_Effectively_Volatile;
|
||||
|
||||
------------------------------------
|
||||
-- Is_Effectively_Volatile_Object --
|
||||
------------------------------------
|
||||
|
||||
function Is_Effectively_Volatile_Object (N : Node_Id) return Boolean is
|
||||
begin
|
||||
if Is_Entity_Name (N) then
|
||||
return Is_Effectively_Volatile (Entity (N));
|
||||
|
||||
elsif Nkind (N) = N_Expanded_Name then
|
||||
return Is_Effectively_Volatile (Entity (N));
|
||||
|
||||
elsif Nkind (N) = N_Indexed_Component then
|
||||
return Is_Effectively_Volatile_Object (Prefix (N));
|
||||
|
||||
elsif Nkind (N) = N_Selected_Component then
|
||||
return
|
||||
Is_Effectively_Volatile_Object (Prefix (N))
|
||||
or else
|
||||
Is_Effectively_Volatile_Object (Selector_Name (N));
|
||||
|
||||
else
|
||||
return False;
|
||||
end if;
|
||||
end Is_Effectively_Volatile_Object;
|
||||
|
||||
----------------------------
|
||||
-- Is_Expression_Function --
|
||||
----------------------------
|
||||
@ -11491,41 +11554,6 @@ package body Sem_Util is
|
||||
end if;
|
||||
end Is_SPARK_Object_Reference;
|
||||
|
||||
-----------------------
|
||||
-- Is_SPARK_Volatile --
|
||||
-----------------------
|
||||
|
||||
function Is_SPARK_Volatile (Id : Entity_Id) return Boolean is
|
||||
begin
|
||||
return Is_Volatile (Id) or else Is_Volatile (Etype (Id));
|
||||
end Is_SPARK_Volatile;
|
||||
|
||||
------------------------------
|
||||
-- Is_SPARK_Volatile_Object --
|
||||
------------------------------
|
||||
|
||||
function Is_SPARK_Volatile_Object (N : Node_Id) return Boolean is
|
||||
begin
|
||||
if Is_Entity_Name (N) then
|
||||
return Is_SPARK_Volatile (Entity (N));
|
||||
|
||||
elsif Nkind (N) = N_Expanded_Name then
|
||||
return Is_SPARK_Volatile (Entity (N));
|
||||
|
||||
elsif Nkind (N) = N_Indexed_Component then
|
||||
return Is_SPARK_Volatile_Object (Prefix (N));
|
||||
|
||||
elsif Nkind (N) = N_Selected_Component then
|
||||
return
|
||||
Is_SPARK_Volatile_Object (Prefix (N))
|
||||
or else
|
||||
Is_SPARK_Volatile_Object (Selector_Name (N));
|
||||
|
||||
else
|
||||
return False;
|
||||
end if;
|
||||
end Is_SPARK_Volatile_Object;
|
||||
|
||||
------------------
|
||||
-- Is_Statement --
|
||||
------------------
|
||||
|
@ -1171,6 +1171,15 @@ package Sem_Util is
|
||||
-- This is the RM definition, a type is a descendent of another type if it
|
||||
-- is the same type or is derived from a descendent of the other type.
|
||||
|
||||
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.
|
||||
|
||||
function Is_Effectively_Volatile_Object (N : Node_Id) return Boolean;
|
||||
-- Determine whether an arbitrary node denotes an effectively volatile
|
||||
-- object.
|
||||
|
||||
function Is_Expression_Function (Subp : Entity_Id) return Boolean;
|
||||
-- Predicate to determine whether a scope entity comes from a rewritten
|
||||
-- expression function call, and should be inlined unconditionally. Also
|
||||
@ -1310,18 +1319,6 @@ package Sem_Util is
|
||||
function Is_SPARK_Object_Reference (N : Node_Id) return Boolean;
|
||||
-- Determines if the tree referenced by N represents an object in SPARK
|
||||
|
||||
function Is_SPARK_Volatile (Id : Entity_Id) return Boolean;
|
||||
-- This routine is similar to predicate Is_Volatile, but it takes SPARK
|
||||
-- semantics into account. In SPARK volatile components to not render a
|
||||
-- type volatile.
|
||||
|
||||
function Is_SPARK_Volatile_Object (N : Node_Id) return Boolean;
|
||||
-- Determine whether an arbitrary node denotes a volatile object reference
|
||||
-- according to the semantics of SPARK. To qualify as volatile, an object
|
||||
-- must be subject to aspect/pragma Volatile or Atomic, or have a [sub]type
|
||||
-- subject to the same attributes. Note that volatile components do not
|
||||
-- render an object volatile.
|
||||
|
||||
function Is_Statement (N : Node_Id) return Boolean;
|
||||
pragma Inline (Is_Statement);
|
||||
-- Check if the node N is a statement node. Note that this includes
|
||||
|
Loading…
Reference in New Issue
Block a user