+2014-01-21 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * aspects.adb Add entries for Async_Readers, Async_Writers,
+ Effective_Reads and Effective_Writes in table Canonical_Aspect.
+ * aspects.ads Add entries for Async_Readers, Async_Writers,
+ Effective_Reads and Effective_Writes in tables Aspect_Id,
+ Aspect_Names, Aspect_Delay and Implementation_Defined_Aspect.
+ * atree.adb (Ekind_In): New version with 8 parameters.
+ (Node34): New routine.
+ (Set_Node34): New routine.
+ * atree.ads (Ekind_In): New version with 8 parameters.
+ (Node34): New routine.
+ (Set_Node34): New routine.
+ * einfo.adb Contract is now Node34.
+ (Contract): Update the assertion and node usage.
+ (Get_Pragma): Include pragmas Async_Readers, Async_Writers,
+ Effective_Reads and Effective_Writes.
+ (Set_Contract): Update the assertion and node usage.
+ (Write_Field24_Name): Remove the output for a contract.
+ (Write_Field34_Name): Add output for a contract.
+ * einfo.ads Contract is now Node34. Update the comment on
+ attribute usage and related node structures.
+ (Get_Pragma): Update the comment on usage.
+ * par-prag.adb (Prag): Pragmas Async_Readers, Async_Writers,
+ Effective_Reads and Effective_Writes do not require special
+ processing by the parser.
+ * sem_ch3.adb (Analyze_Variable_Contract): New routine.
+ (Analyze_Declarations): Analyze the contract of a variable at
+ the end of the declarative region.
+ (Analyze_Object_Declaration): Create a contract for a variable.
+ * sem_ch6.adb (Analyze_Subprogram_Contract): Update the retrieval
+ of classification pragmas.
+ (Process_Formals): Detect an illegal
+ use of a volatile object as a formal in a function.
+ * sem_ch12.adb (Instantiate_Object): Detect an illegal use of
+ a volatile object as an actual in generic instantiation.
+ * sem_prag.adb Add entries for Async_Readers, Async_Writers,
+ Effective_Reads and Effective_Writes in table Sig_Flags.
+ (Analyze_External_State_In_Decl_Part): New routine.
+ (Analyze_Global_Item): Detect an illegal use of a volatile object
+ as a global item of a function.
+ (Analyze_Pragma): Reimplement
+ pragma Abstract_State. Add support for pragmas Async_Readers,
+ Async_Writers, Effective_Reads and Effective_Writes.
+ (Check_External_Properties): New routine.
+ * sem_prag.ads (Analyze_External_State_In_Decl_Part): New routine.
+ (Check_External_Properties): New routine.
+ * sem_res.adb (Resolve_Actuals): Detect an illegal use of a
+ volatile object as an actual in a call.
+ (Resolve_Entity_Name):
+ Add local variables Par, Prev and Usage_OK. Detect illegal
+ contexts of volatile objects.
+ * sem_util.adb (Add_Contract_Item): Add support for
+ pragmas associated with the contract of a variable.
+ (Async_Readers_Enabled): New routine.
+ (Async_Writers_Enabled): New routine.
+ (Effective_Reads_Enabled): New routine.
+ (Effective_Writes_Enabled): New routine.
+ (Has_Enabled_Property):
+ New routine.
+ (Is_Unchecked_Conversion_Instance): New routine.
+ (Is_Volatile_Object): Add support for entities that may denote
+ a volatile object.
+ * sem_util.ads (Add_Contract_Item): Update the
+ comment on usage.
+ (Async_Readers_Enabled): New routine.
+ (Async_Writers_Enabled): New routine.
+ (Effective_Reads_Enabled): New routine.
+ (Effective_Writes_Enabled): New routine.
+ (Is_Unchecked_Conversion_Instance): New routine.
+ * sinfo.ads Update the comment on the structure of N_Contract.
+ * snames.ads-tmpl Add predefined names for Async_Readers,
+ Async_Writers, Effective_Reads and Effective_Writes. Add
+ pragma ids for Async_Readers, Async_Writers, Effective_Reads
+ and Effective_Writes.
+
+2014-01-21 Robert Dewar <dewar@adacore.com>
+
+ * exp_ch4.adb (Eval_Op_Expon): Use CRT_Safe_Compile_Time_Known_Value
+ * sem_eval.adb (Compile_Time_Known_Value): Remove special
+ handling of CRT mode (CRT_Safe_Compile_Time_Known_Value): New
+ function (Eval_Op_Expon): Add CRT_Safe in call to Test_Foldable
+ (Test_Foldable): Add CRT_Safe parameter
+ * sem_eval.ads (Compile_Time_Known_Value): Remove special
+ handling of CRT mode.
+ (CRT_Safe_Compile_Time_Known_Value): New function.
+
2014-01-21 Robert Dewar <dewar@adacore.com>
* sem_prag.adb (Analyze_Pragma, case SPARK_Mode): Fix problem
Aspect_Address => Aspect_Address,
Aspect_Alignment => Aspect_Alignment,
Aspect_All_Calls_Remote => Aspect_All_Calls_Remote,
+ Aspect_Async_Readers => Aspect_Async_Readers,
+ Aspect_Async_Writers => Aspect_Async_Writers,
Aspect_Asynchronous => Aspect_Asynchronous,
Aspect_Atomic => Aspect_Atomic,
Aspect_Atomic_Components => Aspect_Atomic_Components,
Aspect_Discard_Names => Aspect_Discard_Names,
Aspect_Dispatching_Domain => Aspect_Dispatching_Domain,
Aspect_Dynamic_Predicate => Aspect_Predicate,
+ Aspect_Effective_Reads => Aspect_Effective_Reads,
+ Aspect_Effective_Writes => Aspect_Effective_Writes,
Aspect_Elaborate_Body => Aspect_Elaborate_Body,
Aspect_Export => Aspect_Export,
Aspect_External_Name => Aspect_External_Name,
Aspect_Ada_2005, -- GNAT
Aspect_Ada_2012, -- GNAT
+ Aspect_Async_Readers, -- GNAT
+ Aspect_Async_Writers, -- GNAT
Aspect_Asynchronous,
Aspect_Atomic,
Aspect_Atomic_Components,
Aspect_Discard_Names,
+ Aspect_Effective_Reads, -- GNAT
+ Aspect_Effective_Writes, -- GNAT
Aspect_Export,
Aspect_Favor_Top_Level, -- GNAT
Aspect_Independent,
(Aspect_Abstract_State => True,
Aspect_Ada_2005 => True,
Aspect_Ada_2012 => True,
+ Aspect_Async_Readers => True,
+ Aspect_Async_Writers => True,
Aspect_Compiler_Unit => True,
Aspect_Contract_Cases => True,
Aspect_Depends => True,
Aspect_Dimension => True,
Aspect_Dimension_System => True,
+ Aspect_Effective_Reads => True,
+ Aspect_Effective_Writes => True,
Aspect_Favor_Top_Level => True,
Aspect_Global => True,
Aspect_Inline_Always => True,
Aspect_Address => Name_Address,
Aspect_Alignment => Name_Alignment,
Aspect_All_Calls_Remote => Name_All_Calls_Remote,
+ Aspect_Async_Readers => Name_Async_Readers,
+ Aspect_Async_Writers => Name_Async_Writers,
Aspect_Asynchronous => Name_Asynchronous,
Aspect_Atomic => Name_Atomic,
Aspect_Atomic_Components => Name_Atomic_Components,
Aspect_Discard_Names => Name_Discard_Names,
Aspect_Dispatching_Domain => Name_Dispatching_Domain,
Aspect_Dynamic_Predicate => Name_Dynamic_Predicate,
+ Aspect_Effective_Reads => Name_Effective_Reads,
+ Aspect_Effective_Writes => Name_Effective_Writes,
Aspect_Elaborate_Body => Name_Elaborate_Body,
Aspect_External_Name => Name_External_Name,
Aspect_External_Tag => Name_External_Tag,
(No_Aspect => Always_Delay,
Aspect_Address => Always_Delay,
Aspect_All_Calls_Remote => Always_Delay,
+ Aspect_Async_Readers => Always_Delay,
+ Aspect_Async_Writers => Always_Delay,
Aspect_Asynchronous => Always_Delay,
Aspect_Attach_Handler => Always_Delay,
Aspect_Compiler_Unit => Always_Delay,
Aspect_Discard_Names => Always_Delay,
Aspect_Dispatching_Domain => Always_Delay,
Aspect_Dynamic_Predicate => Always_Delay,
+ Aspect_Effective_Reads => Always_Delay,
+ Aspect_Effective_Writes => Always_Delay,
Aspect_Elaborate_Body => Always_Delay,
Aspect_External_Name => Always_Delay,
Aspect_External_Tag => Always_Delay,
T = V7;
end Ekind_In;
+ function Ekind_In
+ (T : Entity_Kind;
+ V1 : Entity_Kind;
+ V2 : Entity_Kind;
+ V3 : Entity_Kind;
+ V4 : Entity_Kind;
+ V5 : Entity_Kind;
+ V6 : Entity_Kind;
+ V7 : Entity_Kind;
+ V8 : Entity_Kind) return Boolean
+ is
+ begin
+ return T = V1 or else
+ T = V2 or else
+ T = V3 or else
+ T = V4 or else
+ T = V5 or else
+ T = V6 or else
+ T = V7 or else
+ T = V8;
+ end Ekind_In;
+
function Ekind_In
(E : Entity_Id;
V1 : Entity_Kind;
return Ekind_In (Ekind (E), V1, V2, V3, V4, V5, V6, V7);
end Ekind_In;
+ function Ekind_In
+ (E : Entity_Id;
+ V1 : Entity_Kind;
+ V2 : Entity_Kind;
+ V3 : Entity_Kind;
+ V4 : Entity_Kind;
+ V5 : Entity_Kind;
+ V6 : Entity_Kind;
+ V7 : Entity_Kind;
+ V8 : Entity_Kind) return Boolean
+ is
+ begin
+ return Ekind_In (Ekind (E), V1, V2, V3, V4, V5, V6, V7, V8);
+ end Ekind_In;
+
------------------------
-- Set_Reporting_Proc --
------------------------
return Node_Id (Nodes.Table (N + 5).Field9);
end Node33;
+ function Node34 (N : Node_Id) return Node_Id is
+ begin
+ pragma Assert (Nkind (N) in N_Entity);
+ return Node_Id (Nodes.Table (N + 5).Field10);
+ end Node34;
+
function List1 (N : Node_Id) return List_Id is
begin
pragma Assert (N <= Nodes.Last);
Nodes.Table (N + 5).Field9 := Union_Id (Val);
end Set_Node33;
+ procedure Set_Node34 (N : Node_Id; Val : Node_Id) is
+ begin
+ pragma Assert (Nkind (N) in N_Entity);
+ Nodes.Table (N + 5).Field10 := Union_Id (Val);
+ end Set_Node34;
+
procedure Set_List1 (N : Node_Id; Val : List_Id) is
begin
pragma Assert (N <= Nodes.Last);
V6 : Entity_Kind;
V7 : Entity_Kind) return Boolean;
+ function Ekind_In
+ (E : Entity_Id;
+ V1 : Entity_Kind;
+ V2 : Entity_Kind;
+ V3 : Entity_Kind;
+ V4 : Entity_Kind;
+ V5 : Entity_Kind;
+ V6 : Entity_Kind;
+ V7 : Entity_Kind;
+ V8 : Entity_Kind) return Boolean;
+
function Ekind_In
(T : Entity_Kind;
V1 : Entity_Kind;
V6 : Entity_Kind;
V7 : Entity_Kind) return Boolean;
+ function Ekind_In
+ (T : Entity_Kind;
+ V1 : Entity_Kind;
+ V2 : Entity_Kind;
+ V3 : Entity_Kind;
+ V4 : Entity_Kind;
+ V5 : Entity_Kind;
+ V6 : Entity_Kind;
+ V7 : Entity_Kind;
+ V8 : Entity_Kind) return Boolean;
+
pragma Inline (Ekind_In);
-- Inline all above functions
function Node33 (N : Node_Id) return Node_Id;
pragma Inline (Node33);
+ function Node34 (N : Node_Id) return Node_Id;
+ pragma Inline (Node34);
+
function List1 (N : Node_Id) return List_Id;
pragma Inline (List1);
procedure Set_Node33 (N : Node_Id; Val : Node_Id);
pragma Inline (Set_Node33);
+ procedure Set_Node34 (N : Node_Id; Val : Node_Id);
+ pragma Inline (Set_Node34);
+
procedure Set_List1 (N : Node_Id; Val : List_Id);
pragma Inline (Set_List1);
-- Stored_Constraint Elist23
-- Related_Expression Node24
- -- Contract Node24
-- Interface_Alias Node25
-- Interfaces Elist25
-- SPARK_Aux_Pragma Node33
- -- (unused) Node34
+ -- Contract Node34
-- (unused) Node35
E_Generic_Package,
E_Package,
E_Package_Body,
- E_Subprogram_Body)
+ E_Subprogram_Body,
+ E_Variable)
or else Is_Generic_Subprogram (Id)
or else Is_Subprogram (Id));
- return Node24 (Id);
+ return Node34 (Id);
end Contract;
function Entry_Parameters_Type (Id : E) return E is
E_Package,
E_Package_Body,
E_Subprogram_Body,
+ E_Variable,
E_Void)
or else Is_Generic_Subprogram (Id)
or else Is_Subprogram (Id));
- Set_Node24 (Id, V);
+ Set_Node34 (Id, V);
end Set_Contract;
procedure Set_Entry_Parameters_Type (Id : E; V : E) is
function Get_Pragma (E : Entity_Id; Id : Pragma_Id) return Node_Id is
Is_CDG : constant Boolean :=
Id = Pragma_Abstract_State or else
+ Id = Pragma_Async_Readers or else
+ Id = Pragma_Async_Writers or else
Id = Pragma_Depends or else
+ Id = Pragma_Effective_Reads or else
+ Id = Pragma_Effective_Writes or else
Id = Pragma_Global or else
Id = Pragma_Initial_Condition or else
Id = Pragma_Initializes or else
Type_Kind =>
Write_Str ("Related_Expression");
- when E_Entry |
- E_Entry_Family |
- E_Generic_Package |
- E_Package |
- E_Package_Body |
- E_Subprogram_Body |
- Generic_Subprogram_Kind |
- Subprogram_Kind =>
- Write_Str ("Contract");
-
when others =>
Write_Str ("Field24???");
end case;
procedure Write_Field34_Name (Id : Entity_Id) is
begin
case Ekind (Id) is
+ when E_Entry |
+ E_Entry_Family |
+ E_Generic_Package |
+ E_Package |
+ E_Package_Body |
+ E_Subprogram_Body |
+ E_Variable |
+ Generic_Subprogram_Kind |
+ Subprogram_Kind =>
+ Write_Str ("Contract");
+
when others =>
Write_Str ("Field34??");
end case;
-- accept statement for a member of the family, and in the prefix of
-- 'COUNT when it applies to a family member.
--- Contract (Node24)
+-- Contract (Node34)
-- Defined in entry, entry family, package, package body, subprogram and
--- subprogram body entities as well as their respective generic forms.
--- Points to the contract of the entity, holding various assertion items
--- and data classifiers.
+-- subprogram body entities as well as their respective generic forms. A
+-- contract is also applicable to a variable. Points to the contract of
+-- the entity, holding various assertion items and data classifiers.
-- Entry_Parameters_Type (Node15)
-- Defined in entries. Points to the access-to-record type that is
-- Accept_Address (Elist21)
-- Scope_Depth_Value (Uint22)
-- Protection_Object (Node23) (protected kind)
- -- Contract (Node24)
-- PPC_Wrapper (Node25)
-- Extra_Formals (Node28)
+ -- Contract (Node34)
-- Default_Expressions_Processed (Flag108)
-- Entry_Accepted (Flag152)
-- Is_AST_Entry (Flag132) (for entry only)
-- Generic_Renamings (Elist23) (for an instance)
-- Inner_Instances (Elist23) (generic case only)
-- Protection_Object (Node23) (for concurrent kind)
- -- Contract (Node24)
-- Interface_Alias (Node25)
-- Overridden_Operation (Node26)
-- Wrapped_Entity (Node27) (non-generic case only)
-- Corresponding_Equality (Node30) (implicit /= only)
-- Thunk_Entity (Node31) (thunk case only)
-- SPARK_Pragma (Node32)
+ -- Contract (Node34)
-- Body_Needed_For_SAL (Flag40)
-- Elaboration_Entity_Required (Flag174)
-- Default_Expressions_Processed (Flag108)
-- Alias (Node18)
-- Extra_Accessibility_Of_Result (Node19)
-- Last_Entity (Node20)
- -- Contract (Node24)
-- Overridden_Operation (Node26)
-- Subprograms_For_Type (Node29)
+ -- Contract (Node34)
-- Has_Invariants (Flag232)
-- Has_Postconditions (Flag240)
-- Is_Machine_Code_Subprogram (Flag137)
-- Generic_Renamings (Elist23) (for an instance)
-- Inner_Instances (Elist23) (generic case only)
-- Limited_View (Node23) (non-generic/instance)
- -- Contract (Node24)
-- Abstract_States (Elist25)
-- Package_Instantiation (Node26)
-- Current_Use_Clause (Node27)
-- Finalizer (Node28) (non-generic case only)
-- SPARK_Aux_Pragma (Node33)
-- SPARK_Pragma (Node32)
+ -- Contract (Node34)
-- Delay_Subprogram_Descriptors (Flag50)
-- Body_Needed_For_SAL (Flag40)
-- Discard_Names (Flag88)
-- Spec_Entity (Node19)
-- Last_Entity (Node20)
-- Scope_Depth_Value (Uint22)
- -- Contract (Node24)
-- Finalizer (Node28) (non-generic case only)
-- SPARK_Aux_Pragma (Node33)
-- SPARK_Pragma (Node32)
+ -- Contract (Node34)
-- Delay_Subprogram_Descriptors (Flag50)
-- Has_Anonymous_Master (Flag253)
-- SPARK_Aux_Pragma_Inherited (Flag266)
-- Generic_Renamings (Elist23) (for an instance)
-- Inner_Instances (Elist23) (generic case only)
-- Protection_Object (Node23) (for concurrent kind)
- -- Contract (Node24)
-- Interface_Alias (Node25)
-- Overridden_Operation (Node26) (never for init proc)
-- Wrapped_Entity (Node27) (non-generic case only)
-- Static_Initialization (Node30) (init_proc only)
-- Thunk_Entity (Node31) (thunk case only)
-- SPARK_Pragma (Node32)
+ -- Contract (Node34)
-- Body_Needed_For_SAL (Flag40)
-- Delay_Cleanups (Flag114)
-- Discard_Names (Flag88)
-- Corresponding_Protected_Entry (Node18)
-- Last_Entity (Node20)
-- Scope_Depth_Value (Uint22)
- -- Contract (Node24)
-- Extra_Formals (Node28)
-- SPARK_Pragma (Node32)
-- SPARK_Pragma_Inherited (Flag265)
+ -- Contract (Node34)
-- Scope_Depth (synth)
-- E_Subprogram_Type
-- Last_Assignment (Node26)
-- Related_Type (Node27)
-- Initialization_Statements (Node28)
+ -- Contract (Node34)
-- Has_Alignment_Clause (Flag46)
-- Has_Atomic_Components (Flag86)
-- Has_Biased_Representation (Flag139)
-- with the given pragma Id. If found, the value returned is the N_Pragma
-- node, otherwise Empty is returned. The following contract pragmas that
-- appear in N_Contract nodes are also handled by this routine:
+ -- Abstract_State
+ -- Async_Readers
+ -- Async_Writers
-- Contract_Cases
-- Depends
+ -- Effective_Reads
+ -- Effective_Writes
-- Global
-- Initial_Condition
-- Initializes
-- Postcondition
-- Refined_Depends
-- Refined_Global
+ -- Refined_State
function Get_Record_Representation_Clause (E : Entity_Id) return Node_Id;
-- Searches the Rep_Item chain for a given entity E, for a record
-- Test for case of known right argument where we can replace the
-- exponentiation by an equivalent expression using multiplication.
- if Compile_Time_Known_Value (Exp) then
+ -- Note: use CRT_Safe version of Compile_Time_Known_Value because in
+ -- configurable run-time mode, we may not have the exponentiation
+ -- routine available, and we don't want the legality of the program
+ -- to depend on how clever the compiler is in knowing values.
+
+ if CRT_Safe_Compile_Time_Known_Value (Exp) then
Expv := Expr_Value (Exp);
-- We only fold small non-negative exponents. You might think we
-- result if the shift causes an overflow before the modular reduction.
if Nkind (Base) = N_Integer_Literal
- and then Intval (Base) = 2
+ and then CRT_Safe_Compile_Time_Known_Value (Base)
+ and then Expr_Value (Base) = Uint_2
and then Is_Integer_Type (Root_Type (Exptyp))
and then Esize (Root_Type (Exptyp)) <= Esize (Standard_Integer)
and then Is_Unsigned_Type (Exptyp)
when Pragma_Abort_Defer |
Pragma_Abstract_State |
+ Pragma_Async_Readers |
+ Pragma_Async_Writers |
Pragma_Assertion_Policy |
Pragma_Assume |
Pragma_Assume_No_Invalid_Values |
Pragma_Disable_Atomic_Synchronization |
Pragma_Discard_Names |
Pragma_Dispatching_Domain |
+ Pragma_Effective_Reads |
+ Pragma_Effective_Writes |
Pragma_Eliminate |
Pragma_Elaborate |
Pragma_Elaborate_All |
("actual must exclude null to match generic formal#", Actual);
end if;
+ -- The following check is only relevant in formal verification mode as
+ -- it is not a standard Ada legality rule. A volatile object cannot be
+ -- used as an actual in a generic instantiation.
+
+ if GNATprove_Mode and then Is_Volatile_Object (Actual) then
+ Error_Msg_N
+ ("volatile object cannot act as actual in generic instantiation",
+ Actual);
+ end if;
+
return List;
end Instantiate_Object;
-- abstract interface types implemented by a record type or a derived
-- record type.
+ procedure Analyze_Variable_Contract (Var_Id : Entity_Id);
+ -- Analyze all delayed aspects chained on the contract of variable Var_Id
+ -- as if they appeared at the end of the declarative region. The aspects in
+ -- consideration are:
+ -- Async_Readers
+ -- Async_Writers
+ -- Effective_Reads
+ -- Effective_Writes
+
procedure Build_Derived_Type
(N : Node_Id;
Parent_Type : Entity_Id;
end if;
end if;
- -- Analyze the contracts of a subprogram declaration or a body now due
- -- to delayed visibility requirements of aspects.
+ -- Analyze the contracts of subprogram declarations, subprogram bodies
+ -- and variables now due to the delayed visibility requirements of their
+ -- aspects.
Decl := First (L);
while Present (Decl) loop
elsif Nkind (Decl) = N_Subprogram_Declaration then
Analyze_Subprogram_Contract (Defining_Entity (Decl));
+
+ elsif Nkind (Decl) = N_Object_Declaration
+ and then Ekind (Defining_Entity (Decl)) = E_Variable
+ then
+ Analyze_Variable_Contract (Defining_Entity (Decl));
end if;
Next (Decl);
if Present (E) then
Set_Has_Initial_Value (Id, True);
end if;
+
+ Set_Contract (Id, Make_Contract (Sloc (Id)));
end if;
-- Initialize alignment and size and capture alignment setting
end if;
end Analyze_Subtype_Indication;
+ -------------------------------
+ -- Analyze_Variable_Contract --
+ -------------------------------
+
+ procedure Analyze_Variable_Contract (Var_Id : Entity_Id) is
+ Items : constant Node_Id := Contract (Var_Id);
+ AR_Val : Boolean := False;
+ AW_Val : Boolean := False;
+ ER_Val : Boolean := False;
+ EW_Val : Boolean := False;
+ Nam : Name_Id;
+ Prag : Node_Id;
+ Seen : Boolean := False;
+
+ begin
+ -- The following check is only relevant in formal verification mode as
+ -- it is not standard Ada legality rule. The declaration of a volatile
+ -- variable must appear at the library level.
+
+ if GNATprove_Mode
+ and then Is_Volatile_Object (Var_Id)
+ and then not Is_Library_Level_Entity (Var_Id)
+ then
+ Error_Msg_N
+ ("volatile variable & must be declared at library level", Var_Id);
+ end if;
+
+ -- Examine the contract
+
+ if Present (Items) then
+
+ -- Analyze classification pragmas
+
+ Prag := Classifications (Items);
+ while Present (Prag) loop
+ Nam := Pragma_Name (Prag);
+
+ if Nam = Name_Async_Readers then
+ Analyze_External_State_In_Decl_Part (Prag, AR_Val);
+ Seen := True;
+
+ elsif Nam = Name_Async_Writers then
+ Analyze_External_State_In_Decl_Part (Prag, AW_Val);
+ Seen := True;
+
+ elsif Nam = Name_Effective_Reads then
+ Analyze_External_State_In_Decl_Part (Prag, ER_Val);
+ Seen := True;
+
+ else pragma Assert (Nam = Name_Effective_Writes);
+ Analyze_External_State_In_Decl_Part (Prag, EW_Val);
+ Seen := True;
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end if;
+
+ -- Once all external properties have been processed, verify their mutual
+ -- interaction.
+
+ if Seen then
+ Check_External_Properties (Var_Id, AR_Val, AW_Val, ER_Val, EW_Val);
+ end if;
+ end Analyze_Variable_Contract;
+
--------------------------
-- Analyze_Variant_Part --
--------------------------
-- Analyze classification pragmas
- Prag := Classifications (Contract (Subp));
+ Prag := Classifications (Items);
while Present (Prag) loop
Nam := Pragma_Name (Prag);
Null_Exclusion_Static_Checks (Param_Spec);
end if;
+ -- The following check is only relevant in formal verification mode
+ -- as it is not a standard Ada legality rule. A function cannot have
+ -- a volatile formal parameter.
+
+ if GNATprove_Mode
+ and then Is_Volatile_Object (Formal)
+ and then Ekind_In (Scope (Formal), E_Function, E_Generic_Function)
+ then
+ Error_Msg_N
+ ("function cannot have a volatile formal parameter", Formal);
+ end if;
+
<<Continue>>
Next (Param_Spec);
end loop;
-- Is_Static_Expression flag from the operands.
procedure Test_Expression_Is_Foldable
- (N : Node_Id;
- Op1 : Node_Id;
- Op2 : Node_Id;
- Stat : out Boolean;
- Fold : out Boolean);
+ (N : Node_Id;
+ Op1 : Node_Id;
+ Op2 : Node_Id;
+ Stat : out Boolean;
+ Fold : out Boolean;
+ CRT_Safe : Boolean := False);
-- Same processing, except applies to an expression N with two operands
- -- Op1 and Op2. The result is static only if both operands are static.
+ -- Op1 and Op2. The result is static only if both operands are static. If
+ -- CRT_Safe is set True, then CRT_Safe_Compile_Time_Known_Value is used
+ -- for the tests that the two operands are known at compile time. See
+ -- spec of this routine for further details.
function Test_In_Range
(N : Node_Id;
-- Compile_Time_Known_Value --
------------------------------
- function Compile_Time_Known_Value
- (Op : Node_Id;
- Ignore_CRT : Boolean := False) return Boolean
- is
+ function Compile_Time_Known_Value (Op : Node_Id) return Boolean is
K : constant Node_Kind := Nkind (Op);
CV_Ent : CV_Entry renames CV_Cache (Nat (Op) mod CV_Cache_Size);
return False;
end if;
- -- If this is not a static expression or a null literal, and we are in
- -- configurable run-time mode, then we consider it not known at compile
- -- time. This avoids anomalies where whether something is allowed with a
- -- given configurable run-time library depends on how good the compiler
- -- is at optimizing and knowing that things are constant when they are
- -- nonstatic. This check is suppressed if Ignore_CRT is True
-
- if (Configurable_Run_Time_Mode and not Ignore_CRT)
- and then K /= N_Null
- and then not Is_Static_Expression (Op)
- then
- -- We make an exception for expressions that evaluate to True/False,
- -- to suppress spurious checks in ZFP mode. So far we have not seen
- -- any negative consequences of this exception.
-
- if Is_Entity_Name (Op)
- and then Ekind (Entity (Op)) = E_Enumeration_Literal
- and then Etype (Entity (Op)) = Standard_Boolean
- then
- null;
- else
- return False;
- end if;
- end if;
-
-- If we have an entity name, then see if it is the name of a constant
-- and if so, test the corresponding constant value, or the name of
-- an enumeration literal, which is always a constant.
end if;
end Compile_Time_Known_Value_Or_Aggr;
+ ---------------------------------------
+ -- CRT_Safe_Compile_Time_Known_Value --
+ ---------------------------------------
+
+ function CRT_Safe_Compile_Time_Known_Value (Op : Node_Id) return Boolean is
+ begin
+ if (Configurable_Run_Time_Mode or No_Run_Time_Mode)
+ and then not Is_OK_Static_Expression (Op)
+ then
+ return False;
+ else
+ return Compile_Time_Known_Value (Op);
+ end if;
+ end CRT_Safe_Compile_Time_Known_Value;
+
-----------------
-- Eval_Actual --
-----------------
return;
end if;
+ -- Otherwise attempt to fold
+
if Is_Universal_Numeric_Type (Etype (Left))
and then
Is_Universal_Numeric_Type (Etype (Right))
begin
-- If not foldable we are done
- Test_Expression_Is_Foldable (N, Left, Right, Stat, Fold);
+ Test_Expression_Is_Foldable
+ (N, Left, Right, Stat, Fold, CRT_Safe => True);
+
+ -- Return if not foldable
if not Fold then
return;
end if;
+ if Configurable_Run_Time_Mode and not Stat then
+ return;
+ end if;
+
-- Fold exponentiation operation
declare
-- Two operand case
procedure Test_Expression_Is_Foldable
- (N : Node_Id;
- Op1 : Node_Id;
- Op2 : Node_Id;
- Stat : out Boolean;
- Fold : out Boolean)
+ (N : Node_Id;
+ Op1 : Node_Id;
+ Op2 : Node_Id;
+ Stat : out Boolean;
+ Fold : out Boolean;
+ CRT_Safe : Boolean := False)
is
Rstat : constant Boolean := Is_Static_Expression (Op1)
and then Is_Static_Expression (Op2);
elsif not Rstat then
Check_Non_Static_Context (Op1);
Check_Non_Static_Context (Op2);
- Fold := Compile_Time_Known_Value (Op1)
- and then Compile_Time_Known_Value (Op2);
+
+ if CRT_Safe then
+ Fold := CRT_Safe_Compile_Time_Known_Value (Op1)
+ and then CRT_Safe_Compile_Time_Known_Value (Op2);
+ else
+ Fold := Compile_Time_Known_Value (Op1)
+ and then Compile_Time_Known_Value (Op2);
+ end if;
+
return;
-- Else result is static and foldable. Both operands are static, and
-- Determine whether two types T1, T2, which have the same base type,
-- are statically matching subtypes (RM 4.9.1(1-2)).
- function Compile_Time_Known_Value
- (Op : Node_Id;
- Ignore_CRT : Boolean := False) return Boolean;
+ function Compile_Time_Known_Value (Op : Node_Id) return Boolean;
-- Returns true if Op is an expression not raising Constraint_Error whose
-- value is known at compile time and for which a call to Expr_Value can
-- be used to determine this value. This is always true if Op is a static
-- expression, but can also be true for expressions which are technically
- -- non-static but which are in fact known at compile time. Some possible
- -- examples of such expressions might be the static lower bound of a
- -- non-static range or the value of a constant object whose initial
- -- value is itself compile time known in the sense of this routine. Note
- -- that this routine is defended against unanalyzed expressions. Such
- -- expressions will not cause a blowup, they may cause pessimistic (i.e.
- -- False) results to be returned. In general we take a pessimistic view.
- -- False does not mean the value could not be known at compile time, but
- -- True means that absolutely definition it is known at compile time and
- -- it is safe to call Expr_Value on the expression Op.
+ -- non-static but which are in fact known at compile time. Some examples of
+ -- such expressions are the static lower bound of a non-static range or the
+ -- value of a constant object whose initial value is itself compile time
+ -- known in the sense of this routine. Note that this routine is defended
+ -- against unanalyzed expressions. Such expressions will not cause a
+ -- blowup, they may cause pessimistic (i.e. False) results to be returned.
+ -- In general we take a pessimistic view. False does not mean the value
+ -- could not be known at compile time, but True means that absolutely
+ -- definition it is known at compile time and it is safe to call
+ -- Expr_Value on the expression Op.
--
-- Note that we don't define precisely the set of expressions that return
-- True. Callers should not make any assumptions regarding the value that
-- efficiency optimization purposes. The code generated can often be more
-- efficient with compile time known values, e.g. range analysis for the
-- purpose of removing checks is more effective if we know precise bounds.
- --
- -- The Ignore_CRT parameter has to do with the special case of configurable
- -- runtime mode. Consider the following example:
+
+ function CRT_Safe_Compile_Time_Known_Value (Op : Node_Id) return Boolean;
+ -- In the case of configurable run-times, there may be an issue calling
+ -- Compile_Time_Known_Value with non-static expressions where the legality
+ -- of the program is not well-defined. Consider this example:
--
-- X := B ** C;
--
-- then what we say is that exponentiation is permitted if the exponent is
-- officially static and has a value in the range 0 .. 4.
--
- -- However, in the normal case, we want efficient code in the case where
- -- a non-static exponent is known at compile time. To take care of this,
- -- the normal default behavior is that in configurable run-time mode most
- -- expressions are considered known at compile time ONLY in the case where
- -- they are officially static. An exception is boolean objects which may
- -- be considered known at compile time even in configurable run-time mode.
- --
- -- That loses optimization opportunities, and it would be better to look
- -- case by case at each use of Compile_Time_Known_Value to see if this
- -- configurable run-time mode special processing is needed. The Ignore_CRT
- -- parameter can be set to True to ignore this special handling in cases
- -- where it is known to be safe to do so.
+ -- In a case like this, we use CRT_Safe_Compile_Time_Known_Value to avoid
+ -- this effect. This routine will return False for a non-static expression
+ -- if we are in configurable run-time mode, even if the expression would
+ -- normally be considered compile-time known.
function Compile_Time_Known_Value_Or_Aggr (Op : Node_Id) return Boolean;
-- Similar to Compile_Time_Known_Value, but also returns True if the value
end if;
end Analyze_Depends_In_Decl_Part;
+ -----------------------------------------
+ -- Analyze_External_State_In_Decl_Part --
+ -----------------------------------------
+
+ procedure Analyze_External_State_In_Decl_Part
+ (N : Node_Id;
+ Expr_Val : out Boolean)
+ is
+ Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N));
+ Obj : constant Node_Id := Get_Pragma_Arg (Arg1);
+ Expr : constant Node_Id := Get_Pragma_Arg (Next (Arg1));
+
+ begin
+ Error_Msg_Name_1 := Pragma_Name (N);
+
+ -- The Async / Effective pragmas must apply to a volatile object other
+ -- than a formal subprogram parameter.
+
+ if Is_Volatile_Object (Obj) then
+ if Is_Entity_Name (Obj)
+ and then Present (Entity (Obj))
+ and then Is_Formal (Entity (Obj))
+ then
+ Error_Msg_N
+ ("external state % cannot apply to a formal parameter", N);
+ end if;
+ else
+ Error_Msg_N ("external state % must apply to a volatile object", N);
+ end if;
+
+ -- Ensure that the expression (if present) is static Boolean. A missing
+ -- argument defaults the value to True.
+
+ Expr_Val := True;
+
+ if Present (Expr) then
+ Analyze_And_Resolve (Expr, Standard_Boolean);
+
+ if Is_Static_Expression (Expr) then
+ Expr_Val := Is_True (Expr_Value (Expr));
+ else
+ Error_Msg_Name_1 := Pragma_Name (N);
+ Error_Msg_N ("expression of % must be static", Expr);
+ end if;
+ end if;
+ end Analyze_External_State_In_Decl_Part;
+
---------------------------------
-- Analyze_Global_In_Decl_Part --
---------------------------------
Check_Mode_Restriction_In_Enclosing_Context (Item, Item_Id);
end if;
+ -- A volatile object cannot appear as a global item of a function
+
+ if Is_Volatile_Object (Item)
+ and then Ekind_In (Spec_Id, E_Function, E_Generic_Function)
+ then
+ Error_Msg_N
+ ("volatile object cannot act as global item of a function",
+ Item);
+ end if;
+
-- The same entity might be referenced through various way. Check
-- the entity of the item rather than the item itself.
-- ABSTRACT_STATE_LIST ::=
-- null
-- | STATE_NAME_WITH_OPTIONS
- -- | (STATE_NAME_WITH_OPTIONS {, STATE_NAME_WITH_OPTIONS})
+ -- | (STATE_NAME_WITH_OPTIONS {, STATE_NAME_WITH_OPTIONS} )
-- STATE_NAME_WITH_OPTIONS ::=
- -- state_NAME
- -- | (state_NAME with OPTION_LIST)
+ -- STATE_NAME
+ -- | (STATE_NAME with OPTION_LIST)
-- OPTION_LIST ::= OPTION {, OPTION}
- -- OPTION ::= SIMPLE_OPTION | NAME_VALUE_OPTION
+ -- OPTION ::=
+ -- SIMPLE_OPTION
+ -- | NAME_VALUE_OPTION
+
+ -- SIMPLE_OPTION ::= identifier
+
+ -- NAME_VALUE_OPTION ::=
+ -- Part_Of => ABSTRACT_STATE
+ -- | External [=> EXTERNAL_PROPERTY_LIST]
- -- SIMPLE_OPTION ::=
- -- External | Non_Volatile | Input_Only | Output_Only
+ -- EXTERNAL_PROPERTY_LIST ::=
+ -- EXTERNAL_PROPERTY
+ -- | (EXTERNAL_PROPERTY {, EXTERNAL_PROPERTY} )
- -- NAME_VALUE_OPTION ::= Part_Of => abstract_state_NAME
+ -- EXTERNAL_PROPERTY ::=
+ -- Async_Readers [=> boolean_EXPRESSION]
+ -- | Async_Writers [=> boolean_EXPRESSION]
+ -- | Effective_Reads [=> boolean_EXPRESSION]
+ -- | Effective_Writes [=> boolean_EXPRESSION]
+
+ -- STATE_NAME ::= defining_identifier
+
+ -- ABSTRACT_STATE ::= name
when Pragma_Abstract_State => Abstract_State : declare
- Pack_Id : Entity_Id;
-- Flags used to verify the consistency of states
Non_Null_Seen : Boolean := False;
Null_Seen : Boolean := False;
+ Pack_Id : Entity_Id;
+ -- The entity of the related package when pragma Abstract_State
+ -- appears.
+
procedure Analyze_Abstract_State (State : Node_Id);
-- Verify the legality of a single state declaration. Create and
-- decorate a state abstraction entity and introduce it into the
----------------------------
procedure Analyze_Abstract_State (State : Node_Id) is
+
+ -- Flags used to verify the consistency of options
+
+ AR_Seen : Boolean := False;
+ AW_Seen : Boolean := False;
+ ER_Seen : Boolean := False;
+ EW_Seen : Boolean := False;
+ External_Seen : Boolean := False;
+ Part_Of_Seen : Boolean := False;
+
+ -- Flags used to store the static value of all external states'
+ -- expressions.
+
+ AR_Val : Boolean := False;
+ AW_Val : Boolean := False;
+ ER_Val : Boolean := False;
+ EW_Val : Boolean := False;
+
+ procedure Analyze_External_Option (Opt : Node_Id);
+ -- Verify the legality of option External
+
+ procedure Analyze_External_Property
+ (Prop : Node_Id;
+ Expr : Node_Id := Empty);
+ -- Verify the legailty of a single external property. Prop
+ -- denotes the external property. Expr is the expression used
+ -- to set the property.
+
+ procedure Analyze_Part_Of_Option (Opt : Node_Id);
+ -- Verify the legality of option Part_Of
+
procedure Check_Duplicate_Option
(Opt : Node_Id;
Status : in out Boolean);
-- seen while processing a state. This routine verifies that
-- Opt is not a duplicate property and sets the flag Status.
+ -----------------------------
+ -- Analyze_External_Option --
+ -----------------------------
+
+ procedure Analyze_External_Option (Opt : Node_Id) is
+ Errors : constant Nat := Serious_Errors_Detected;
+ Prop : Node_Id;
+ Props : Node_Id := Empty;
+
+ begin
+ Check_Duplicate_Option (Opt, External_Seen);
+
+ if Nkind (Opt) = N_Component_Association then
+ Props := Expression (Opt);
+ end if;
+
+ -- External state with properties
+
+ if Present (Props) then
+
+ -- Multiple properties appear as an aggregate
+
+ if Nkind (Props) = N_Aggregate then
+
+ -- Simple property form
+
+ Prop := First (Expressions (Props));
+ while Present (Prop) loop
+ Analyze_External_Property (Prop);
+ Next (Prop);
+ end loop;
+
+ -- Property with expression form
+
+ Prop := First (Component_Associations (Props));
+ while Present (Prop) loop
+ Analyze_External_Property
+ (Prop => First (Choices (Prop)),
+ Expr => Expression (Prop));
+
+ Next (Prop);
+ end loop;
+
+ -- Single property
+
+ else
+ Analyze_External_Property (Props);
+ end if;
+
+ -- An external state defined without any properties defaults
+ -- all properties to True.
+
+ else
+ AR_Val := True;
+ AW_Val := True;
+ ER_Val := True;
+ EW_Val := True;
+ end if;
+
+ -- Once all external properties have been processed, verify
+ -- their mutual interaction. Do not perform the check when
+ -- at least one of the properties is illegal as this will
+ -- produce a bogus error.
+
+ if Errors = Serious_Errors_Detected then
+ Check_External_Properties
+ (State, AR_Val, AW_Val, ER_Val, EW_Val);
+ end if;
+ end Analyze_External_Option;
+
+ -------------------------------
+ -- Analyze_External_Property --
+ -------------------------------
+
+ procedure Analyze_External_Property
+ (Prop : Node_Id;
+ Expr : Node_Id := Empty)
+ is
+ Expr_Val : Boolean;
+
+ begin
+ -- The external property must be one of the predefined four
+ -- reader / writer choices.
+
+ if Nkind (Prop) /= N_Identifier
+ or else not Nam_In (Chars (Prop), Name_Async_Readers,
+ Name_Async_Writers,
+ Name_Effective_Reads,
+ Name_Effective_Writes)
+ then
+ Error_Msg_N ("invalid external state property", Prop);
+ return;
+ end if;
+
+ -- Ensure that the expression of the external state property
+ -- is static Boolean (if applicable).
+
+ if Present (Expr) then
+ Analyze_And_Resolve (Expr, Standard_Boolean);
+
+ if Is_Static_Expression (Expr) then
+ Expr_Val := Is_True (Expr_Value (Expr));
+ else
+ Error_Msg_N
+ ("expression of external state property must be "
+ & "static", Expr);
+ end if;
+
+ -- The lack of expression defaults the property to True
+
+ else
+ Expr_Val := True;
+ end if;
+
+ if Chars (Prop) = Name_Async_Readers then
+ Check_Duplicate_Option (Prop, AR_Seen);
+ AR_Val := Expr_Val;
+
+ elsif Chars (Prop) = Name_Async_Writers then
+ Check_Duplicate_Option (Prop, AW_Seen);
+ AW_Val := Expr_Val;
+
+ elsif Chars (Prop) = Name_Effective_Reads then
+ Check_Duplicate_Option (Prop, ER_Seen);
+ ER_Val := Expr_Val;
+
+ else
+ Check_Duplicate_Option (Prop, EW_Seen);
+ EW_Val := Expr_Val;
+ end if;
+ end Analyze_External_Property;
+
+ ----------------------------
+ -- Analyze_Part_Of_Option --
+ ----------------------------
+
+ procedure Analyze_Part_Of_Option (Opt : Node_Id) is
+ Par_State : constant Node_Id := Expression (Opt);
+
+ begin
+ Check_Duplicate_Option (Opt, Part_Of_Seen);
+
+ Analyze (Par_State);
+
+ -- The expression of option Part_Of must denote an abstract
+ -- state.
+
+ if not Is_Entity_Name (Par_State)
+ or else No (Entity (Par_State))
+ or else Ekind (Entity (Par_State)) /= E_Abstract_State
+ then
+ Error_Msg_N
+ ("option Part_Of must denote an abstract state",
+ Par_State);
+ end if;
+ end Analyze_Part_Of_Option;
+
----------------------------
-- Check_Duplicate_Option --
----------------------------
Errors : constant Nat := Serious_Errors_Detected;
Loc : constant Source_Ptr := Sloc (State);
- Assoc : Node_Id;
- Id : Entity_Id;
Is_Null : Boolean := False;
- Name : Name_Id;
Opt : Node_Id;
- Par_State : Node_Id;
-
- -- Flags used to verify the consistency of options
-
- External_Seen : Boolean := False;
- Input_Seen : Boolean := False;
- Non_Volatile_Seen : Boolean := False;
- Output_Seen : Boolean := False;
- Part_Of_Seen : Boolean := False;
+ Opt_Nam : Node_Id;
+ State_Id : Entity_Id;
+ State_Nam : Name_Id;
-- Start of processing for Analyze_Abstract_State
-- Null states appear as internally generated entities
elsif Nkind (State) = N_Null then
- Name := New_Internal_Name ('S');
+ State_Nam := New_Internal_Name ('S');
Is_Null := True;
Null_Seen := True;
-- Simple state declaration
elsif Nkind (State) = N_Identifier then
- Name := Chars (State);
+ State_Nam := Chars (State);
Non_Null_Seen := True;
-- State declaration with various options. This construct
elsif Nkind (State) = N_Extension_Aggregate then
if Nkind (Ancestor_Part (State)) = N_Identifier then
- Name := Chars (Ancestor_Part (State));
+ State_Nam := Chars (Ancestor_Part (State));
Non_Null_Seen := True;
else
Error_Msg_N
Ancestor_Part (State));
end if;
- -- Process options External, Input_Only, Output_Only and
- -- Volatile. Ensure that none of them appear more than once.
+ -- Catch an attempt to introduce a simple option which is
+ -- currently not allowed. An exception to this is External
+ -- defined without any properties.
Opt := First (Expressions (State));
while Present (Opt) loop
- if Nkind (Opt) = N_Identifier then
- if Chars (Opt) = Name_External then
- Check_Duplicate_Option (Opt, External_Seen);
- elsif Chars (Opt) = Name_Input_Only then
- Check_Duplicate_Option (Opt, Input_Seen);
- elsif Chars (Opt) = Name_Output_Only then
- Check_Duplicate_Option (Opt, Output_Seen);
- elsif Chars (Opt) = Name_Non_Volatile then
- Check_Duplicate_Option (Opt, Non_Volatile_Seen);
-
- -- Ensure that the abstract state component of option
- -- Part_Of has not been omitted.
-
- elsif Chars (Opt) = Name_Part_Of then
- Error_Msg_N
- ("option Part_Of requires an abstract state",
- Opt);
- else
- Error_Msg_N ("invalid state option", Opt);
- end if;
+ if Nkind (Opt) = N_Identifier
+ and then Chars (Opt) = Name_External
+ then
+ Analyze_External_Option (Opt);
else
- Error_Msg_N ("invalid state option", Opt);
+ Error_Msg_N
+ ("simple option not allowed in state declaration",
+ Opt);
end if;
Next (Opt);
end loop;
- -- External may appear on its own or with exactly one option
- -- Input_Only or Output_Only, but not both.
-
- if External_Seen
- and then Input_Seen
- and then Output_Seen
- then
- Error_Msg_N
- ("option External requires exactly one option "
- & "Input_Only or Output_Only", State);
- end if;
+ -- Options External and Part_Of appear as component
+ -- associations.
- -- Either Input_Only or Output_Only require External
+ Opt := First (Component_Associations (State));
+ while Present (Opt) loop
+ Opt_Nam := First (Choices (Opt));
- if (Input_Seen or Output_Seen)
- and then not External_Seen
- then
- Error_Msg_N
- ("options Input_Only and Output_Only require option "
- & "External", State);
- end if;
+ if Nkind (Opt_Nam) = N_Identifier then
+ if Chars (Opt_Nam) = Name_External then
+ Analyze_External_Option (Opt);
- -- Option Part_Of appears as a component association
+ elsif Chars (Opt_Nam) = Name_Part_Of then
+ Analyze_Part_Of_Option (Opt);
- Assoc := First (Component_Associations (State));
- while Present (Assoc) loop
- Opt := First (Choices (Assoc));
- while Present (Opt) loop
- if Nkind (Opt) = N_Identifier
- and then Chars (Opt) = Name_Part_Of
- then
- Check_Duplicate_Option (Opt, Part_Of_Seen);
else
Error_Msg_N ("invalid state option", Opt);
end if;
-
- Next (Opt);
- end loop;
-
- -- Part_Of must denote a parent state. Ensure that the
- -- tree is not malformed by checking the expression of
- -- the component association.
-
- Par_State := Expression (Assoc);
- pragma Assert (Present (Par_State));
-
- Analyze (Par_State);
-
- -- Part_Of specified a legal state, this automatically
- -- makes the state a constituent.
-
- if Is_Entity_Name (Par_State)
- and then Present (Entity (Par_State))
- and then Ekind (Entity (Par_State)) = E_Abstract_State
- then
- null;
else
- Error_Msg_N
- ("option Part_Of must denote an abstract state",
- Par_State);
+ Error_Msg_N ("invalid state option", Opt);
end if;
- Next (Assoc);
+ Next (Opt);
end loop;
-- Any other attempt to declare a state is erroneous
-- The generated state abstraction reuses the same characters
-- from the original state declaration. Decorate the entity.
- Id := Make_Defining_Identifier (Loc, New_External_Name (Name));
- Set_Comes_From_Source (Id, not Is_Null);
- Set_Parent (Id, State);
- Set_Ekind (Id, E_Abstract_State);
- Set_Etype (Id, Standard_Void_Type);
- Set_Refined_State (Id, Empty);
- Set_Refinement_Constituents (Id, New_Elmt_List);
+ State_Id :=
+ Make_Defining_Identifier (Loc, New_External_Name (State_Nam));
+
+ Set_Comes_From_Source (State_Id, not Is_Null);
+ Set_Parent (State_Id, State);
+ Set_Ekind (State_Id, E_Abstract_State);
+ Set_Etype (State_Id, Standard_Void_Type);
+ Set_Refined_State (State_Id, Empty);
+ Set_Refinement_Constituents (State_Id, New_Elmt_List);
-- Every non-null state must be nameable and resolvable the
-- same way a constant is.
if not Is_Null then
Push_Scope (Pack_Id);
- Enter_Name (Id);
+ Enter_Name (State_Id);
Pop_Scope;
end if;
-- Verify whether the state introduces an illegal hidden state
-- within a package subject to a null abstract state.
- Check_No_Hidden_State (Id);
+ Check_No_Hidden_State (State_Id);
-- Associate the state with its related package
Set_Abstract_States (Pack_Id, New_Elmt_List);
end if;
- Append_Elmt (Id, Abstract_States (Pack_Id));
+ Append_Elmt (State_Id, Abstract_States (Pack_Id));
end Analyze_Abstract_State;
-- Local variables
State := First (Expressions (State));
while Present (State) loop
Analyze_Abstract_State (State);
-
Next (State);
end loop;
end if;
end AST_Entry;
+ ------------------------------------------------------------------
+ -- Async_Readers/Async_Writers/Effective_Reads/Effective_Writes --
+ ------------------------------------------------------------------
+
+ -- pragma Asynch_Readers ( identifier [, boolean_EXPRESSION] );
+ -- pragma Asynch_Writers ( identifier [, boolean_EXPRESSION] );
+ -- pragma Effective_Reads ( identifier [, boolean_EXPRESSION] );
+ -- pragma Effective_Writes ( identifier [, boolean_EXPRESSION] );
+
+ when Pragma_Async_Readers |
+ Pragma_Async_Writers |
+ Pragma_Effective_Reads |
+ Pragma_Effective_Writes =>
+ Async_Effective : declare
+ Duplic : Node_Id;
+ Obj_Id : Entity_Id;
+
+ begin
+ GNAT_Pragma;
+ Check_No_Identifiers;
+ Check_At_Least_N_Arguments (1);
+ Check_At_Most_N_Arguments (2);
+ Check_Arg_Is_Local_Name (Arg1);
+
+ Arg1 := Get_Pragma_Arg (Arg1);
+
+ -- Perform minimal verification to ensure that the argument is at
+ -- least a variable. Subsequent finer grained checks will be done
+ -- at the end of the declarative region the contains the pragma.
+
+ if Is_Entity_Name (Arg1) and then Present (Entity (Arg1)) then
+ Obj_Id := Entity (Get_Pragma_Arg (Arg1));
+
+ -- It is not efficient to examine preceding statements in order
+ -- to detect duplicate pragmas as Boolean aspects may appear
+ -- anywhere between the related object declaration and its
+ -- freeze point. As an alternative, inspect the contents of the
+ -- variable contract.
+
+ if Ekind (Obj_Id) = E_Variable then
+ Duplic := Get_Pragma (Obj_Id, Prag_Id);
+
+ if Present (Duplic) then
+ Error_Msg_Name_1 := Pname;
+ Error_Msg_Sloc := Sloc (Duplic);
+ Error_Msg_N ("pragma % duplicates pragma declared #", N);
+
+ -- Chain the pragma on the contract for further processing.
+ -- This also aids in detecting duplicates.
+
+ else
+ Add_Contract_Item (N, Obj_Id);
+ end if;
+
+ -- The minimum legality requirements have been met, do not
+ -- fall through to the error message.
+
+ return;
+ end if;
+ end if;
+
+ -- If we get here, then the pragma applies to a non-object
+ -- construct, issue a generic error.
+
+ Error_Pragma ("pragma % must apply to a volatile object");
+ end Async_Effective;
+
------------------
-- Asynchronous --
------------------
Set_SPARK_Pragma_Inherited (Spec_Id, False);
Set_SPARK_Aux_Pragma (Spec_Id, N);
Set_SPARK_Aux_Pragma_Inherited (Spec_Id, True);
-
return;
-- The pragma applies to a subprogram declaration
return False;
end Appears_In;
+ -------------------------------
+ -- Check_External_Properties --
+ -------------------------------
+
+ procedure Check_External_Properties
+ (Item : Node_Id;
+ AR : Boolean;
+ AW : Boolean;
+ ER : Boolean;
+ EW : Boolean)
+ is
+ begin
+ -- All properties enabled
+
+ if AR and then AW and then ER and then EW then
+ null;
+
+ -- Async_Readers + Effective_Writes
+ -- Async_Readers + Async_Writers + Effective_Writes
+
+ elsif AR and then EW and then not ER then
+ null;
+
+ -- Async_Writers + Effective_Reads
+ -- Async_Readers + Async_Writers + Effective_Reads
+
+ elsif AW and then ER and then not EW then
+ null;
+
+ -- Async_Readers + Async_Writers
+
+ elsif AR and then AW and then not ER and then not EW then
+ null;
+
+ -- Async_Readers
+
+ elsif AR and then not AW and then not ER and then not EW then
+ null;
+
+ -- Async_Writers
+
+ elsif AW and then not AR and then not ER and then not EW then
+ null;
+
+ else
+ Error_Msg_N
+ ("illegal combination of external state properties", Item);
+ end if;
+ end Check_External_Properties;
+
----------------
-- Check_Kind --
----------------
Pragma_Ada_12 => -1,
Pragma_Ada_2012 => -1,
Pragma_All_Calls_Remote => -1,
- Pragma_Allow_Integer_Address => 0,
+ Pragma_Allow_Integer_Address => 0,
Pragma_Annotate => -1,
Pragma_Assert => -1,
Pragma_Assert_And_Cut => -1,
Pragma_Assertion_Policy => 0,
Pragma_Assume => -1,
Pragma_Assume_No_Invalid_Values => 0,
- Pragma_Attribute_Definition => +3,
+ Pragma_Async_Readers => 0,
+ Pragma_Async_Writers => 0,
Pragma_Asynchronous => -1,
Pragma_Atomic => 0,
Pragma_Atomic_Components => 0,
Pragma_Attach_Handler => -1,
+ Pragma_Attribute_Definition => +3,
Pragma_Check => 99,
Pragma_Check_Float_Overflow => 0,
Pragma_Check_Name => 0,
Pragma_Disable_Atomic_Synchronization => -1,
Pragma_Discard_Names => 0,
Pragma_Dispatching_Domain => -1,
+ Pragma_Effective_Reads => 0,
+ Pragma_Effective_Writes => 0,
Pragma_Elaborate => -1,
Pragma_Elaborate_All => -1,
Pragma_Elaborate_Body => -1,
-- Perform full analysis of delayed pragma Depends. This routine is also
-- capable of performing basic analysis of pragma Refined_Depends.
+ procedure Analyze_External_State_In_Decl_Part
+ (N : Node_Id;
+ Expr_Val : out Boolean);
+ -- Perform full analysis of delayed pragmas Async_Readers, Async_Writers,
+ -- Effective_Reads and Effective_Writes. Flag Expr_Val contains the Boolean
+ -- argument of the pragma or a default True if no argument is present.
+
procedure Analyze_Global_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Global. This routine is also
-- capable of performing basic analysis of pragma Refind_Global.
-- whether -gnata was used, if so, then the call has no effect, otherwise
-- Is_Ignored (but not Is_Disabled) is set True.
+ procedure Check_External_Properties
+ (Item : Node_Id;
+ AR : Boolean;
+ AW : Boolean;
+ ER : Boolean;
+ EW : Boolean);
+ -- Flags AR, AW, ER and EW denote the static values of external properties
+ -- Async_Readers, Async_Writers, Effective_Reads and Effective_Writes. Item
+ -- is the related variable or state. Ensure the legality of the permutation
+ -- and if this is not the case, issue an error.
+
function Delay_Config_Pragma_Analyze (N : Node_Id) return Boolean;
-- N is a pragma appearing in a configuration pragma file. Most such
-- pragmas are analyzed when the file is read, before parsing and analyzing
Check_Unset_Reference (A);
end if;
+ -- The following checks are only relevant in formal verification
+ -- mode as they are not standard Ada legality rule.
+
+ if GNATprove_Mode
+ and then Is_Volatile_Object (A)
+ then
+ -- A 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.
+
+ elsif Is_Unchecked_Conversion_Instance (Nam) then
+ null;
+
+ else
+ Error_Msg_N
+ ("volatile object cannot act as actual in a call", A);
+ end if;
+ end if;
+
Next_Actual (A);
-- Case where actual is not present
-- Used to resolve identifiers and expanded names
procedure Resolve_Entity_Name (N : Node_Id; Typ : Entity_Id) is
- E : constant Entity_Id := Entity (N);
+ E : constant Entity_Id := Entity (N);
+ Par : Node_Id;
+ Prev : Node_Id;
+
+ Usage_OK : Boolean := False;
+ -- Flag set when the use of a volatile object agrees with its context
begin
-- If garbage from errors, set to Any_Type and return
Eval_Entity_Name (N);
end if;
+
+ -- The following checks are only relevant in formal verification mode as
+ -- they are not standard Ada legality rule. A volatile object subject to
+ -- enabled properties Async_Writers or Effective_Reads must appear in a
+ -- specific context.
+
+ if GNATprove_Mode
+ and then Ekind (E) = E_Variable
+ and then Is_Volatile_Object (E)
+ and then
+ (Async_Writers_Enabled (E)
+ or else Effective_Reads_Enabled (E))
+ then
+ Par := Parent (N);
+ Prev := N;
+ while Present (Par) loop
+
+ -- The variable can appear on either side of an assignment
+
+ if Nkind (Par) = N_Assignment_Statement then
+ Usage_OK := True;
+ exit;
+
+ -- The variable is part of the initialization expression of an
+ -- object. Ensure that the climb of the parent chain came from the
+ -- expression side and not from the name side.
+
+ elsif Nkind (Par) = N_Object_Declaration
+ and then Present (Expression (Par))
+ and then Prev = Expression (Par)
+ then
+ Usage_OK := True;
+ exit;
+
+ -- The variable appears as an actual parameter in a call to an
+ -- instance of Unchecked_Conversion whose result is renamed.
+
+ elsif Nkind (Par) = N_Function_Call
+ and then Is_Unchecked_Conversion_Instance (Entity (Name (Par)))
+ and then Nkind (Parent (Par)) = N_Object_Renaming_Declaration
+ then
+ Usage_OK := True;
+ exit;
+
+ -- 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.
+
+ elsif Nkind (Par) = N_Procedure_Call_Statement then
+ Usage_OK := True;
+ exit;
+
+ -- Prevent the search from going too far
+
+ elsif Is_Body_Or_Package_Declaration (Par) then
+ exit;
+ end if;
+
+ Prev := Par;
+ Par := Parent (Par);
+ end loop;
+
+ if not Usage_OK then
+ Error_Msg_N ("volatile object cannot appear in this context", N);
+ end if;
+ end if;
end Resolve_Entity_Name;
-------------------
-- components in the selected variant to determine whether all of them
-- have a default.
+ function Has_Enabled_Property
+ (Extern : Node_Id;
+ Prop_Nam : Name_Id) return Boolean;
+ -- Subsidiary to routines Async_xxx_Enabled and Effective_xxx_Enabled.
+ -- Given pragma External, determine whether it contains a property denoted
+ -- by its name Prop_Nam and if it does, whether its expression is True.
+
function Has_Null_Extension (T : Entity_Id) return Boolean;
-- T is a derived tagged type. Check whether the type extension is null.
-- If the parent type is fully initialized, T can be treated as such.
-- The pragma is not a proper contract item
+ else
+ raise Program_Error;
+ end if;
+
+ -- Contract items related to variables. The applicable pragmas are:
+ -- Async_Readers
+ -- Async_Writers
+ -- Effective_Reads
+ -- Effective_Writes
+
+ elsif Ekind (Id) = E_Variable then
+ if Nam_In (Nam, Name_Async_Readers,
+ Name_Async_Writers,
+ Name_Effective_Reads,
+ Name_Effective_Writes)
+ then
+ Set_Next_Pragma (Prag, Classifications (Items));
+ Set_Classifications (Items, Prag);
+
+ -- The pragma is not a proper contract item
+
else
raise Program_Error;
end if;
end if;
end Apply_Compile_Time_Constraint_Error;
+ ---------------------------
+ -- Async_Readers_Enabled --
+ ---------------------------
+
+ function Async_Readers_Enabled (Id : Entity_Id) return Boolean is
+ begin
+ if Ekind (Id) = E_Abstract_State then
+ return
+ Has_Enabled_Property
+ (Extern => Get_Pragma (Id, Pragma_External),
+ Prop_Nam => Name_Async_Readers);
+
+ else pragma Assert (Ekind (Id) = E_Variable);
+ return Present (Get_Pragma (Id, Pragma_Async_Readers));
+ end if;
+ end Async_Readers_Enabled;
+
+ ---------------------------
+ -- Async_Writers_Enabled --
+ ---------------------------
+
+ function Async_Writers_Enabled (Id : Entity_Id) return Boolean is
+ begin
+ if Ekind (Id) = E_Abstract_State then
+ return
+ Has_Enabled_Property
+ (Extern => Get_Pragma (Id, Pragma_External),
+ Prop_Nam => Name_Async_Writers);
+
+ else pragma Assert (Ekind (Id) = E_Variable);
+ return Present (Get_Pragma (Id, Pragma_Async_Writers));
+ end if;
+ end Async_Writers_Enabled;
+
--------------------------------------
-- Available_Full_View_Of_Component --
--------------------------------------
end if;
end Effective_Extra_Accessibility;
+ -----------------------------
+ -- Effective_Reads_Enabled --
+ -----------------------------
+
+ function Effective_Reads_Enabled (Id : Entity_Id) return Boolean is
+ begin
+ if Ekind (Id) = E_Abstract_State then
+ return
+ Has_Enabled_Property
+ (Extern => Get_Pragma (Id, Pragma_External),
+ Prop_Nam => Name_Effective_Reads);
+
+ else pragma Assert (Ekind (Id) = E_Variable);
+ return Present (Get_Pragma (Id, Pragma_Effective_Reads));
+ end if;
+ end Effective_Reads_Enabled;
+
+ ------------------------------
+ -- Effective_Writes_Enabled --
+ ------------------------------
+
+ function Effective_Writes_Enabled (Id : Entity_Id) return Boolean is
+ begin
+ if Ekind (Id) = E_Abstract_State then
+ return
+ Has_Enabled_Property
+ (Extern => Get_Pragma (Id, Pragma_External),
+ Prop_Nam => Name_Effective_Writes);
+
+ else pragma Assert (Ekind (Id) = E_Variable);
+ return Present (Get_Pragma (Id, Pragma_Effective_Writes));
+ end if;
+ end Effective_Writes_Enabled;
+
------------------------------
-- Enclosing_Comp_Unit_Node --
------------------------------
return False;
end Has_Discriminant_Dependent_Constraint;
+ --------------------------
+ -- Has_Enabled_Property --
+ --------------------------
+
+ function Has_Enabled_Property
+ (Extern : Node_Id;
+ Prop_Nam : Name_Id) return Boolean
+ is
+ Prop : Node_Id;
+ Props : Node_Id := Empty;
+
+ begin
+ -- The related abstract state or variable do not have an Extern pragma,
+ -- the property in question cannot be set.
+
+ if No (Extern) then
+ return False;
+
+ elsif Nkind (Extern) = N_Component_Association then
+ Props := Expression (Extern);
+ end if;
+
+ -- External state with properties
+
+ if Present (Props) then
+
+ -- Multiple properties appear as an aggregate
+
+ if Nkind (Props) = N_Aggregate then
+
+ -- Simple property form
+
+ Prop := First (Expressions (Props));
+ while Present (Prop) loop
+ if Chars (Prop) = Prop_Nam then
+ return True;
+ end if;
+
+ Next (Prop);
+ end loop;
+
+ -- Property with expression form
+
+ Prop := First (Component_Associations (Props));
+ while Present (Prop) loop
+ if Chars (Prop) = Prop_Nam then
+ return Is_True (Expr_Value (Expression (Prop)));
+ end if;
+
+ Next (Prop);
+ end loop;
+
+ -- Pragma Extern contains properties, but not the one we want
+
+ return False;
+
+ -- Single property
+
+ else
+ return Chars (Prop) = Prop_Nam;
+ end if;
+
+ -- An external state defined without any properties defaults all
+ -- properties to True;
+
+ else
+ return True;
+ end if;
+ end Has_Enabled_Property;
+
--------------------
-- Has_Infinities --
--------------------
return (U /= 0);
end Is_True;
+ --------------------------------------
+ -- Is_Unchecked_Conversion_Instance --
+ --------------------------------------
+
+ function Is_Unchecked_Conversion_Instance (Id : Entity_Id) return Boolean is
+ Gen_Par : Entity_Id;
+
+ begin
+ -- Look for a function whose generic parent is the predefined intrinsic
+ -- function Unchecked_Conversion.
+
+ if Ekind (Id) = E_Function then
+ Gen_Par := Generic_Parent (Parent (Id));
+
+ return
+ Present (Gen_Par)
+ and then Chars (Gen_Par) = Name_Unchecked_Conversion
+ and then Is_Intrinsic_Subprogram (Gen_Par)
+ and then Is_Predefined_File_Name
+ (Unit_File_Name (Get_Source_Unit (Gen_Par)));
+ end if;
+
+ return False;
+ end Is_Unchecked_Conversion_Instance;
+
-------------------------------
-- Is_Universal_Numeric_Type --
-------------------------------
function Is_Volatile_Object (N : Node_Id) return Boolean is
- function Object_Has_Volatile_Components (N : Node_Id) return Boolean;
- -- Determines if given object has volatile components
-
function Is_Volatile_Prefix (N : Node_Id) return Boolean;
-- If prefix is an implicit dereference, examine designated type
+ function Object_Has_Volatile_Components (N : Node_Id) return Boolean;
+ -- Determines if given object has volatile components
+
------------------------
-- Is_Volatile_Prefix --
------------------------
-- Start of processing for Is_Volatile_Object
begin
- if Is_Volatile (Etype (N))
+ if Nkind (N) = N_Defining_Identifier then
+ return Is_Volatile (N) or else Is_Volatile (Etype (N));
+
+ elsif Nkind (N) = N_Expanded_Name then
+ return Is_Volatile_Object (Entity (N));
+
+ elsif Is_Volatile (Etype (N))
or else (Is_Entity_Name (N) and then Is_Volatile (Entity (N)))
then
return True;
-- Add pragma Prag to the contract of an entry, a package [body] or a
-- subprogram [body] denoted by Id. The following are valid pragmas:
-- Abstract_States
+ -- Async_Readers
+ -- Async_Writers
-- Contract_Cases
-- Depends
+ -- Effective_Reads
+ -- Effective_Writes
-- Global
-- Initial_Condition
-- Initializes
-- not end with a ? (this is used when the caller wants to parameterize
-- whether an error or warning is given.
+ 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.
+
+ 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.
+
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
-- component, several array operations are not avaiable on the type, and
-- Same as Einfo.Extra_Accessibility except thtat object renames
-- 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.
+
+ 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.
+
function Enclosing_Comp_Unit_Node (N : Node_Id) return Node_Id;
-- Returns the enclosing N_Compilation_Unit Node that is the root of a
-- subtree containing N.
-- operand (i.e. is either 0 for False, or 1 for True). This function tests
-- if it is True (i.e. non-zero).
+ function Is_Unchecked_Conversion_Instance (Id : Entity_Id) return Boolean;
+ -- Determine whether an arbitrary entity denotes an instance of function
+ -- Ada.Unchecked_Conversion.
+
function Is_Universal_Numeric_Type (T : Entity_Id) return Boolean;
pragma Inline (Is_Universal_Numeric_Type);
-- True if T is Universal_Integer or Universal_Real
-- establish dependencies between subprogram or package inputs and
-- outputs. Currently the following pragmas appear in this list:
-- Abstract_States
+ -- Async_Readers
+ -- Async_Writers
-- Depends
+ -- Effective_Reads
+ -- Effective_Writes
-- Global
-- Initial_Condition
-- Initializes
Name_Assert : constant Name_Id := N + $; -- Ada 05
Name_Assert_And_Cut : constant Name_Id := N + $; -- GNAT
+ Name_Async_Readers : constant Name_Id := N + $; -- GNAT
+ Name_Async_Writers : constant Name_Id := N + $; -- GNAT
Name_Asynchronous : constant Name_Id := N + $;
Name_Atomic : constant Name_Id := N + $;
Name_Atomic_Components : constant Name_Id := N + $;
Name_Debug : constant Name_Id := N + $; -- GNAT
Name_Depends : constant Name_Id := N + $; -- GNAT
+ Name_Effective_Reads : constant Name_Id := N + $; -- GNAT
+ Name_Effective_Writes : constant Name_Id := N + $; -- GNAT
Name_Elaborate : constant Name_Id := N + $; -- Ada 83
Name_Elaborate_All : constant Name_Id := N + $;
Name_Elaborate_Body : constant Name_Id := N + $;
Pragma_All_Calls_Remote,
Pragma_Assert,
Pragma_Assert_And_Cut,
+ Pragma_Async_Readers,
+ Pragma_Async_Writers,
Pragma_Asynchronous,
Pragma_Atomic,
Pragma_Atomic_Components,
Pragma_CPP_Vtable,
Pragma_Debug,
Pragma_Depends,
+ Pragma_Effective_Reads,
+ Pragma_Effective_Writes,
Pragma_Elaborate,
Pragma_Elaborate_All,
Pragma_Elaborate_Body,
projects / thirdparty / gcc.git / commitdiff
