--
-- Part_Of
+ procedure Check_Type_Or_Object_External_Properties
+ (Type_Or_Obj_Id : Entity_Id);
+ -- Perform checking of external properties pragmas that is common to both
+ -- type declarations and object declarations.
+
procedure Expand_Subprogram_Contract (Body_Id : Entity_Id);
-- Expand the contracts of a subprogram body and its correspoding spec (if
-- any). This routine processes all [refined] pre- and postconditions as
raise Program_Error;
end if;
- -- Protected units, the applicable pragmas are:
- -- Part_Of
-
- elsif Ekind (Id) = E_Protected_Type then
- if Prag_Nam = Name_Part_Of then
- Add_Classification;
+ -- The four volatility refinement pragmas are ok for all types.
+ -- Part_Of is ok for task types and protected types.
+ -- Depends and Global are ok for task types.
+
+ elsif Is_Type (Id) then
+ declare
+ Is_OK : constant Boolean :=
+ Nam_In (Prag_Nam, Name_Async_Readers,
+ Name_Async_Writers,
+ Name_Effective_Reads,
+ Name_Effective_Writes)
+ or else (Ekind (Id) = E_Task_Type
+ and Nam_In (Prag_Nam, Name_Part_Of,
+ Name_Depends,
+ Name_Global))
+ or else (Ekind (Id) = E_Protected_Type
+ and Prag_Nam = Name_Part_Of);
+ begin
+ if Is_OK then
+ Add_Classification;
+ else
- -- The pragma is not a proper contract item
+ -- The pragma is not a proper contract item
- else
- raise Program_Error;
- end if;
+ raise Program_Error;
+ end if;
+ end;
-- Subprogram bodies, the applicable pragmas are:
-- Postcondition
-- Global
-- Part_Of
- elsif Ekind (Id) = E_Task_Type then
- if Nam_In (Prag_Nam, Name_Depends, Name_Global, Name_Part_Of) then
- Add_Classification;
-
- -- The pragma is not a proper contract item
-
- else
- raise Program_Error;
- end if;
-
-- Variables, the applicable pragmas are:
-- Async_Readers
-- Async_Writers
else
raise Program_Error;
end if;
+
+ else
+ raise Program_Error;
end if;
end Add_Contract_Item;
end;
end if;
+ if Nkind_In (Decl, N_Full_Type_Declaration,
+ N_Private_Type_Declaration,
+ N_Task_Type_Declaration,
+ N_Protected_Type_Declaration,
+ N_Formal_Type_Declaration)
+ then
+ Analyze_Type_Contract (Defining_Identifier (Decl));
+ end if;
+
Next (Decl);
end loop;
end Analyze_Contracts;
end if;
end Analyze_Entry_Or_Subprogram_Contract;
+ ----------------------------------------------
+ -- Check_Type_Or_Object_External_Properties --
+ ----------------------------------------------
+
+ procedure Check_Type_Or_Object_External_Properties
+ (Type_Or_Obj_Id : Entity_Id)
+ is
+ function Decl_Kind (Is_Type : Boolean;
+ Object_Kind : String) return String;
+ -- Returns "type" or Object_Kind, depending on Is_Type
+
+ ---------------
+ -- Decl_Kind --
+ ---------------
+
+ function Decl_Kind (Is_Type : Boolean;
+ Object_Kind : String) return String is
+ begin
+ if Is_Type then
+ return "type";
+ else
+ return Object_Kind;
+ end if;
+ end Decl_Kind;
+
+ Is_Type_Id : constant Boolean := Is_Type (Type_Or_Obj_Id);
+
+ -- Local variables
+
+ AR_Val : Boolean := False;
+ AW_Val : Boolean := False;
+ ER_Val : Boolean := False;
+ EW_Val : Boolean := False;
+ Seen : Boolean := False;
+ Prag : Node_Id;
+ Obj_Typ : Entity_Id;
+
+ -- Start of processing for Check_Type_Or_Object_External_Properties
+
+ begin
+ -- 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.
+
+ if Is_Derived_Type (Type_Or_Obj_Id) then
+ declare
+ Parent_Type : constant Entity_Id :=
+ Etype (Base_Type (Type_Or_Obj_Id));
+ begin
+ if Is_Effectively_Volatile (Parent_Type) then
+ AR_Val := Async_Readers_Enabled (Parent_Type);
+ AW_Val := Async_Writers_Enabled (Parent_Type);
+ ER_Val := Effective_Reads_Enabled (Parent_Type);
+ EW_Val := Effective_Writes_Enabled (Parent_Type);
+ 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);
+
+ if Present (Prag) then
+ declare
+ Saved_AR_Val : constant Boolean := AR_Val;
+ begin
+ Analyze_External_Property_In_Decl_Part (Prag, AR_Val);
+ Seen := True;
+ if Saved_AR_Val and not AR_Val then
+ Error_Msg_N
+ ("illegal non-confirming Async_Readers specification",
+ Prag);
+ end if;
+ end;
+ end if;
+
+ Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Async_Writers);
+
+ if Present (Prag) then
+ declare
+ Saved_AW_Val : constant Boolean := AW_Val;
+ begin
+ Analyze_External_Property_In_Decl_Part (Prag, AW_Val);
+ Seen := True;
+ if Saved_AW_Val and not AW_Val then
+ Error_Msg_N
+ ("illegal non-confirming Async_Writers specification",
+ Prag);
+ end if;
+ end;
+ end if;
+
+ Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Effective_Reads);
+
+ if Present (Prag) then
+ declare
+ Saved_ER_Val : constant Boolean := ER_Val;
+ begin
+ Analyze_External_Property_In_Decl_Part (Prag, ER_Val);
+ Seen := True;
+ if Saved_ER_Val and not ER_Val then
+ Error_Msg_N
+ ("illegal non-confirming Effective_Reads specification",
+ Prag);
+ end if;
+ end;
+ end if;
+
+ Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Effective_Writes);
+
+ if Present (Prag) then
+ declare
+ Saved_EW_Val : constant Boolean := EW_Val;
+ begin
+ Analyze_External_Property_In_Decl_Part (Prag, EW_Val);
+ Seen := True;
+ if Saved_EW_Val and not EW_Val then
+ Error_Msg_N
+ ("illegal non-confirming Effective_Writes specification",
+ Prag);
+ end if;
+ end;
+ end if;
+
+ -- Verify the mutual interaction of the various external properties
+
+ if Seen then
+ Check_External_Properties
+ (Type_Or_Obj_Id, AR_Val, AW_Val, ER_Val, EW_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.
+
+ if SPARK_Mode = On and then Comes_From_Source (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_N
+ ("effectively volatile "
+ & Decl_Kind (Is_Type => Is_Type_Id,
+ Object_Kind => "variable")
+ & " & must be declared at library level "
+ & "(SPARK RM 7.1.3(3))", 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 (Is_Type => Is_Type_Id,
+ Object_Kind => "object")
+ & " & 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_Volatile_Component (Type_Or_Obj_Id)
+ then
+ Error_Msg_N
+ ("non-volatile type & cannot have volatile"
+ & " components",
+ Type_Or_Obj_Id);
+ end if;
+ end if;
+ end if;
+ end Check_Type_Or_Object_External_Properties;
+
-----------------------------
-- Analyze_Object_Contract --
-----------------------------
Saved_SMP : constant Node_Id := SPARK_Mode_Pragma;
-- Save the SPARK_Mode-related data to restore on exit
- AR_Val : Boolean := False;
- AW_Val : Boolean := False;
- ER_Val : Boolean := False;
- EW_Val : Boolean := False;
NC_Val : Boolean := False;
Items : Node_Id;
Prag : Node_Id;
Ref_Elmt : Elmt_Id;
- Seen : Boolean := False;
begin
-- The loop parameter in an element iterator over a formal container
else pragma Assert (Ekind (Obj_Id) = E_Variable);
- -- Analyze all external properties
-
- Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers);
-
- if Present (Prag) then
- Analyze_External_Property_In_Decl_Part (Prag, AR_Val);
- Seen := True;
- end if;
-
- Prag := Get_Pragma (Obj_Id, Pragma_Async_Writers);
-
- if Present (Prag) then
- Analyze_External_Property_In_Decl_Part (Prag, AW_Val);
- Seen := True;
- end if;
-
- Prag := Get_Pragma (Obj_Id, Pragma_Effective_Reads);
-
- if Present (Prag) then
- Analyze_External_Property_In_Decl_Part (Prag, ER_Val);
- Seen := True;
- end if;
-
- Prag := Get_Pragma (Obj_Id, Pragma_Effective_Writes);
-
- if Present (Prag) then
- Analyze_External_Property_In_Decl_Part (Prag, EW_Val);
- Seen := True;
- end if;
-
- -- Verify the mutual interaction of the various external properties
-
- if Seen then
- Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
- end if;
+ Check_Type_Or_Object_External_Properties
+ (Type_Or_Obj_Id => Obj_Id);
-- Analyze the non-external volatility property No_Caching
else
Check_Missing_Part_Of (Obj_Id);
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.
-
- if SPARK_Mode = On and then Comes_From_Source (Obj_Id) then
- 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(3), C.6(6)).
-
- if not Is_Library_Level_Entity (Obj_Id) then
- Error_Msg_N
- ("volatile variable & must be declared at library level "
- & "(SPARK RM 7.1.3(3))", 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 object & cannot be volatile", Obj_Id);
- end if;
-
- -- The object is not effectively volatile
-
- else
- -- A non-effectively volatile object cannot have effectively
- -- volatile components (SPARK RM 7.1.3(6)).
-
- if not Is_Effectively_Volatile (Obj_Id)
- and then Has_Volatile_Component (Obj_Typ)
- then
- Error_Msg_N
- ("non-volatile object & cannot have volatile components",
- Obj_Id);
- end if;
- end if;
- end if;
end if;
-- Common checks
Restore_SPARK_Mode (Saved_SM, Saved_SMP);
end Analyze_Task_Contract;
+ ---------------------------
+ -- Analyze_Type_Contract --
+ ---------------------------
+
+ procedure Analyze_Type_Contract (Type_Id : Entity_Id) is
+ begin
+ Check_Type_Or_Object_External_Properties
+ (Type_Or_Obj_Id => Type_Id);
+ end Analyze_Type_Contract;
+
-----------------------------
-- Create_Generic_Contract --
-----------------------------
Analyze_Task_Contract (Defining_Entity (Decl));
end if;
+ if Nkind_In (Decl, N_Full_Type_Declaration,
+ N_Private_Type_Declaration,
+ N_Task_Type_Declaration,
+ N_Protected_Type_Declaration,
+ N_Formal_Type_Declaration)
+ then
+ Analyze_Type_Contract (Defining_Identifier (Decl));
+ end if;
+
Prev (Decl);
end loop;
end Freeze_Contracts;
procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id);
-- Add pragma Prag to the contract of a constant, entry, entry family,
-- [generic] package, package body, protected unit, [generic] subprogram,
- -- subprogram body, variable or task unit denoted by Id. The following are
- -- valid pragmas:
+ -- subprogram body, variable, task unit, or type denoted by Id.
+ -- The following are valid pragmas:
--
-- Abstract_State
-- Async_Readers
-- Freeze_Id is the entity of a [generic] package body or a [generic]
-- subprogram body which "freezes" the contract of Obj_Id.
+ procedure Analyze_Type_Contract (Type_Id : Entity_Id);
+ -- Analyze all delayed pragmas chained on the contract of object Obj_Id as
+ -- if they appeared at the end of the declarative region. The pragmas to be
+ -- considered are:
+ --
+ -- Async_Readers
+ -- Async_Writers
+ -- Effective_Reads
+ -- Effective_Writes
+ --
+ -- In the case of a protected or task type, there will also be
+ -- a call to Analyze_Protected_Contract or Analyze_Task_Contract.
+
procedure Analyze_Package_Body_Contract
(Body_Id : Entity_Id;
Freeze_Id : Entity_Id := Empty);
E_Package,
E_Package_Body)
or else
+ Is_Type (Id) -- types
+ or else
Ekind (Id) = E_Void); -- special purpose
return Node34 (Id);
end Contract;
Ekind_In (Id, E_Generic_Package, -- packages
E_Package,
E_Package_Body)
+
+ or else
+ Is_Type (Id) -- types
+
or else
Ekind (Id) = E_Void); -- special purpose
Set_Node34 (Id, V);
| E_Package
| E_Package_Body
| E_Procedure
- | E_Protected_Type
| E_Subprogram_Body
| E_Task_Body
- | E_Task_Type
| E_Variable
+ | Type_Kind
| E_Void
=>
Write_Str ("Contract");
-- Contract (Node34)
-- Defined in constant, entry, entry family, operator, [generic] package,
--- package body, protected type, [generic] subprogram, subprogram body,
--- variable and task type entities. Points to the contract of the entity,
--- holding various assertion items and data classifiers.
+-- package body, protected unit, [generic] subprogram, subprogram body,
+-- variable, task unit, and type entities. Points to the contract of the
+-- entity, holding various assertion items and data classifiers.
-- Contract_Wrapper (Node25)
-- Defined in entry and entry family entities. Set only when the entry
Actual);
end if;
+ -- Check actual/formal compatibility with respect to the four
+ -- volatility refinement aspects.
+
+ declare
+ Actual_Obj : Entity_Id;
+ N : Node_Id := Actual;
+ begin
+ -- Similar to Sem_Util.Get_Enclosing_Object, but treat
+ -- pointer dereference like component selection.
+ loop
+ if Is_Entity_Name (N) then
+ Actual_Obj := Entity (N);
+ exit;
+ end if;
+
+ case Nkind (N) is
+ when N_Indexed_Component
+ | N_Selected_Component
+ | N_Slice
+ | N_Explicit_Dereference
+ =>
+ N := Prefix (N);
+
+ when N_Type_Conversion =>
+ N := Expression (N);
+
+ when others =>
+ Actual_Obj := Etype (N);
+ exit;
+ end case;
+ end loop;
+
+ Check_Volatility_Compatibility
+ (Actual_Obj, A_Gen_Obj, "actual object",
+ "its corresponding formal object of mode in out",
+ Srcpos_Bearer => Actual);
+ end;
+
-- Formal in-parameter
else
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 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 => Act_T);
end if;
end Check_Shared_Variable_Control_Aspects;
-- Check some general restrictions on language defined aspects
- if not Implementation_Defined_Aspect (A_Id) then
+ if not Implementation_Defined_Aspect (A_Id)
+ or else 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_Reads
+ then
Error_Msg_Name_1 := Nam;
-- Not allowed for renaming declarations. Examine the original
and then A_Id /= Aspect_Atomic_Components
and then A_Id /= Aspect_Independent_Components
and then A_Id /= Aspect_Volatile_Components
+ and then A_Id /= Aspect_Async_Readers
+ and then A_Id /= Aspect_Async_Writers
+ and then A_Id /= Aspect_Effective_Reads
+ and then A_Id /= Aspect_Effective_Reads
then
Error_Msg_N
("aspect % not allowed for formal type declaration",
Set_Is_Tagged_Type (T, False);
end if;
+ -- 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;
+
Set_Etype (T, T);
-- If the type has appeared already in a with_type clause, it is frozen
Set_First_Rep_Item (Implicit_Base, First_Rep_Item (Parent_Base));
Set_Parent (Implicit_Base, Parent (Derived_Type));
Set_Is_Known_Valid (Implicit_Base, Is_Known_Valid (Parent_Base));
+ Set_Is_Volatile (Implicit_Base, Is_Volatile (Parent_Base));
-- Set RM Size for discrete type or decimal fixed-point type
-- Ordinary fixed-point is excluded, why???
& """No_Caching"" (SPARK RM 7.1.2(6))", N);
else
SPARK_Msg_N
- ("external property % must apply to a volatile object", N);
+ ("external property % must apply to a volatile type or object",
+ N);
end if;
-- Pragma No_Caching should only apply to volatile variables of
and then Prag_Id = Pragma_Volatile
and then not Nkind_In (Original_Node (Decl),
N_Full_Type_Declaration,
+ N_Formal_Type_Declaration,
N_Object_Declaration,
N_Single_Protected_Declaration,
N_Single_Task_Declaration)
| Pragma_No_Caching
=>
Async_Effective : declare
- Obj_Decl : Node_Id;
- Obj_Id : Entity_Id;
-
+ Obj_Or_Type_Decl : Node_Id;
+ Obj_Or_Type_Id : Entity_Id;
begin
GNAT_Pragma;
Check_No_Identifiers;
Check_At_Most_N_Arguments (1);
- Obj_Decl := Find_Related_Context (N, Do_Checks => True);
-
- -- Object declaration
-
- if Nkind (Obj_Decl) /= N_Object_Declaration then
- Pragma_Misplaced;
- return;
+ Obj_Or_Type_Decl := Find_Related_Context (N, Do_Checks => True);
+
+ -- Pragma must apply to a object declaration or to a type
+ -- declaration (only the former in the No_Caching case).
+ -- Original_Node is necessary to account for untagged derived
+ -- types that are rewritten as subtypes of their
+ -- respective root types.
+
+ if Nkind (Obj_Or_Type_Decl) /= N_Object_Declaration then
+ if (Prag_Id = Pragma_No_Caching)
+ or not Nkind_In (Original_Node (Obj_Or_Type_Decl),
+ N_Full_Type_Declaration,
+ N_Private_Type_Declaration,
+ N_Formal_Type_Declaration,
+ N_Task_Type_Declaration,
+ N_Protected_Type_Declaration)
+ then
+ Pragma_Misplaced;
+ return;
+ end if;
end if;
- Obj_Id := Defining_Entity (Obj_Decl);
+ Obj_Or_Type_Id := Defining_Entity (Obj_Or_Type_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.
+ -- least a variable or a type. Subsequent finer grained checks
+ -- will be done at the end of the declarative region that
+ -- contains the pragma.
- if Ekind (Obj_Id) = E_Variable then
+ if Ekind (Obj_Or_Type_Id) = E_Variable or Is_Type (Obj_Or_Type_Id)
+ then
+
+ -- In the case of a type, pragma is a type-related
+ -- representation item and so requires checks common to
+ -- all type-related representation items.
+
+ if Is_Type (Obj_Or_Type_Id)
+ and then Rep_Item_Too_Late (Obj_Or_Type_Id, N)
+ then
+ return;
+ end if;
-- A pragma that applies to a Ghost entity becomes Ghost for
-- the purposes of legality checks and removal of ignored Ghost
-- code.
- Mark_Ghost_Pragma (N, Obj_Id);
+ Mark_Ghost_Pragma (N, Obj_Or_Type_Id);
-- Chain the pragma on the contract for further processing by
-- Analyze_External_Property_In_Decl_Part.
- Add_Contract_Item (N, Obj_Id);
+ Add_Contract_Item (N, Obj_Or_Type_Id);
-- Analyze the Boolean expression (if any)
-- Otherwise the external property applies to a constant
else
- Error_Pragma ("pragma % must apply to a volatile object");
+ Error_Pragma
+ ("pragma % must apply to a volatile type or object");
end if;
end Async_Effective;
-- Skip internally generated code
- elsif not Comes_From_Source (Stmt) then
+ elsif not Comes_From_Source (Stmt)
+ and then not Comes_From_Source (Original_Node (Stmt))
+ then
-- The anonymous object created for a single concurrent type is a
-- suitable context.
(Item_Id : Entity_Id;
Property : Name_Id) return Boolean;
-- Subsidiary to routines Async_xxx_Enabled and Effective_xxx_Enabled.
- -- Determine whether an abstract state or a variable denoted by entity
- -- Item_Id has enabled property Property.
+ -- Determine whether the state abstraction, variable, or type denoted by
+ -- entity Item_Id has enabled property Property.
function Has_Null_Extension (T : Entity_Id) return Boolean;
-- T is a derived tagged type. Check whether the type extension is null.
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 --
-----------------
(Item_Id : Entity_Id;
Property : Name_Id) return Boolean
is
- function Protected_Object_Has_Enabled_Property return Boolean;
- -- Determine whether a protected object denoted by Item_Id has the
- -- property enabled.
+ function Protected_Type_Or_Variable_Has_Enabled_Property return Boolean;
+ -- Determine whether a protected type or variable denoted by Item_Id
+ -- has the property enabled.
function State_Has_Enabled_Property return Boolean;
-- Determine whether a state denoted by Item_Id has the property enabled
- function Variable_Has_Enabled_Property return Boolean;
- -- Determine whether a variable denoted by Item_Id has the property
- -- enabled.
-
- -------------------------------------------
- -- Protected_Object_Has_Enabled_Property --
- -------------------------------------------
+ function Type_Or_Variable_Has_Enabled_Property
+ (Item_Id : Entity_Id) return Boolean;
+ -- Determine whether type or variable denoted by Item_Id has the
+ -- property enabled.
- function Protected_Object_Has_Enabled_Property return Boolean is
- Constits : constant Elist_Id := Part_Of_Constituents (Item_Id);
- Constit_Elmt : Elmt_Id;
- Constit_Id : Entity_Id;
+ -----------------------------------------------------
+ -- Protected_Type_Or_Variable_Has_Enabled_Property --
+ -----------------------------------------------------
+ function Protected_Type_Or_Variable_Has_Enabled_Property return Boolean
+ is
begin
- -- Protected objects always have the properties Async_Readers and
+ -- Protected entities always have the properties Async_Readers and
-- Async_Writers (SPARK RM 7.1.2(16)).
if Property = Name_Async_Readers
-- properties Effective_Reads and Effective_Writes
-- (SPARK RM 7.1.2(16)).
- elsif Present (Constits) then
- Constit_Elmt := First_Elmt (Constits);
- while Present (Constit_Elmt) loop
- Constit_Id := Node (Constit_Elmt);
+ elsif Is_Single_Protected_Object (Item_Id) then
+ declare
+ Constit_Elmt : Elmt_Id;
+ Constit_Id : Entity_Id;
+ Constits : constant Elist_Id
+ := Part_Of_Constituents (Item_Id);
+ begin
+ if Present (Constits) then
+ Constit_Elmt := First_Elmt (Constits);
+ while Present (Constit_Elmt) loop
+ Constit_Id := Node (Constit_Elmt);
+
+ if Has_Enabled_Property (Constit_Id, Property) then
+ return True;
+ end if;
- if Has_Enabled_Property (Constit_Id, Property) then
- return True;
+ Next_Elmt (Constit_Elmt);
+ end loop;
end if;
-
- Next_Elmt (Constit_Elmt);
- end loop;
+ end;
end if;
return False;
- end Protected_Object_Has_Enabled_Property;
+ end Protected_Type_Or_Variable_Has_Enabled_Property;
--------------------------------
-- State_Has_Enabled_Property --
return False;
end State_Has_Enabled_Property;
- -----------------------------------
- -- Variable_Has_Enabled_Property --
- -----------------------------------
+ -------------------------------------------
+ -- Type_Or_Variable_Has_Enabled_Property --
+ -------------------------------------------
- function Variable_Has_Enabled_Property return Boolean is
+ function Type_Or_Variable_Has_Enabled_Property
+ (Item_Id : Entity_Id) return Boolean
+ is
function Is_Enabled (Prag : Node_Id) return Boolean;
-- Determine whether property pragma Prag (if present) denotes an
-- enabled property.
EW : constant Node_Id :=
Get_Pragma (Item_Id, Pragma_Effective_Writes);
- -- Start of processing for Variable_Has_Enabled_Property
+ Is_Derived_Type_With_Volatile_Parent_Type : constant Boolean :=
+ Is_Derived_Type (Item_Id)
+ and then Is_Effectively_Volatile (Etype (Base_Type (Item_Id)));
+
+ -- Start of processing for Type_Or_Variable_Has_Enabled_Property
begin
-- A non-effectively volatile object can never possess external
-- property is enabled when the flag evaluates to True or the flag is
-- missing altogether.
- elsif Property = Name_Async_Readers and then Is_Enabled (AR) then
- return True;
+ elsif Property = Name_Async_Readers and then Present (AR) then
+ return Is_Enabled (AR);
- elsif Property = Name_Async_Writers and then Is_Enabled (AW) then
- return True;
+ elsif Property = Name_Async_Writers and then Present (AW) then
+ return Is_Enabled (AW);
- elsif Property = Name_Effective_Reads and then Is_Enabled (ER) then
- return True;
+ elsif Property = Name_Effective_Reads and then Present (ER) then
+ return Is_Enabled (ER);
- elsif Property = Name_Effective_Writes and then Is_Enabled (EW) then
- return True;
+ elsif Property = Name_Effective_Writes and then Present (EW) then
+ return Is_Enabled (EW);
+
+ -- If other properties are set explicitly, then this one is set
+ -- implicitly to False, except in the case of a derived type
+ -- whose parent type is volatile (in that case, we will inherit
+ -- from the parent type, below).
+
+ elsif (Present (AR)
+ or else Present (AW)
+ or else Present (ER)
+ or else Present (EW))
+ and then not Is_Derived_Type_With_Volatile_Parent_Type
+ then
+ return False;
+
+ -- For a private type, may need to look at the full view
+
+ elsif Is_Private_Type (Item_Id) and then Present (Full_View (Item_Id))
+ then
+ return Type_Or_Variable_Has_Enabled_Property (Full_View (Item_Id));
+
+ -- For a derived type whose parent type is volatile, the
+ -- property may be inherited (but ignore a non-volatile parent).
+
+ elsif Is_Derived_Type_With_Volatile_Parent_Type then
+ return Type_Or_Variable_Has_Enabled_Property
+ (First_Subtype (Etype (Base_Type (Item_Id))));
+
+ -- If not specified explicitly for an object and the type
+ -- is effectively volatile, then take result from the type.
+
+ elsif not Is_Type (Item_Id)
+ and then Is_Effectively_Volatile (Etype (Item_Id))
+ then
+ return Has_Enabled_Property (Etype (Item_Id), Property);
-- The implicit case lacks all property pragmas
elsif No (AR) and then No (AW) and then No (ER) and then No (EW) then
if Is_Protected_Type (Etype (Item_Id)) then
- return Protected_Object_Has_Enabled_Property;
+ return Protected_Type_Or_Variable_Has_Enabled_Property;
else
return True;
end if;
else
return False;
end if;
- end Variable_Has_Enabled_Property;
+ end Type_Or_Variable_Has_Enabled_Property;
-- Start of processing for Has_Enabled_Property
return State_Has_Enabled_Property;
elsif Ekind (Item_Id) = E_Variable then
- return Variable_Has_Enabled_Property;
+ return Type_Or_Variable_Has_Enabled_Property (Item_Id);
+
+ elsif Is_Type (Item_Id) then
+ return Type_Or_Variable_Has_Enabled_Property
+ (Item_Id => First_Subtype (Item_Id));
-- By default, protected objects only have the properties Async_Readers
-- and Async_Writers. If they have Part_Of components, they also inherit
-- (SPARK RM 7.1.2(16)).
elsif Ekind (Item_Id) = E_Protected_Object then
- return Protected_Object_Has_Enabled_Property;
+ return Protected_Type_Or_Variable_Has_Enabled_Property;
-- Otherwise a property is enabled when the related item is effectively
-- volatile.
-- force an error).
function Async_Readers_Enabled (Id : Entity_Id) return Boolean;
- -- Given the entity of an abstract state or a variable, determine whether
- -- Id is subject to external property Async_Readers and if it is, the
- -- related expression evaluates to True.
+ -- Id should be the entity of a state abstraction, a variable, or a type.
+ -- Returns True iff Id is subject to external property Async_Readers.
function Async_Writers_Enabled (Id : Entity_Id) return Boolean;
- -- Given the entity of an abstract state or a variable, determine whether
- -- Id is subject to external property Async_Writers and if it is, the
- -- related expression evaluates to True.
+ -- Id should be the entity of a state abstraction, a variable, or a type.
+ -- Returns True iff Id is subject to external property Async_Writers.
function Available_Full_View_Of_Component (T : Entity_Id) return Boolean;
-- If at the point of declaration an array type has a private or limited
-- 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
-- are looked through.
function Effective_Reads_Enabled (Id : Entity_Id) return Boolean;
- -- Given the entity of an abstract state or a variable, determine whether
- -- Id is subject to external property Effective_Reads and if it is, the
- -- related expression evaluates to True.
+ -- Id should be the entity of a state abstraction, a variable, or a type.
+ -- Returns True iff Id is subject to external property Effective_Reads.
function Effective_Writes_Enabled (Id : Entity_Id) return Boolean;
- -- Given the entity of an abstract state or a variable, determine whether
- -- Id is subject to external property Effective_Writes and if it is, the
- -- related expression evaluates to True.
+ -- Id should be the entity of a state abstraction, a variable, or a type.
+ -- Returns True iff Id is subject to external property Effective_Writes.
function Enclosing_Comp_Unit_Node (N : Node_Id) return Node_Id;
-- Returns the enclosing N_Compilation_Unit node that is the root of a
projects / gcc.git / commitdiff