+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
-- 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
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
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";
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.
P : AFCB_Ptr;
begin
+ -- Take a task lock to protect Open_Files
+
+ SSL.Lock_Task.all;
+
-- Search list of open files
P := Open_Files;
and then P.Shared_Status = Yes
then
Stream := P.Stream;
+
+ Record_AFCB;
+
exit;
-- Otherwise one of the files has Shared=Yes and one has
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
+ return;
- if Stream = NULL_Stream then
+ else
Fopen_Mode
(Mode, Text_Encoding in Text_Content_Encoding,
Creat, Amethod, Fopstr);
-- 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;
------------------------
("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 "
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);
-- 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
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;
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;
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;
("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);
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;
-- 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
& "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
-- 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;
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
-- 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 -
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;
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 --
----------------------------
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 --
------------------
-- 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
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
projects / gcc.git / commitdiff