if Ghost_Config.Ghost_Mode = Check then
if Nkind (N) in N_Entity then
Set_Is_Checked_Ghost_Entity (N);
+ Set_Ghost_Assertion_Level
+ (N, Ghost_Config.Ghost_Mode_Assertion_Level);
end if;
elsif Ghost_Config.Ghost_Mode = Ignore then
if Nkind (N) in N_Entity then
Set_Is_Ignored_Ghost_Entity (N);
+ Set_Ghost_Assertion_Level
+ (N, Ghost_Config.Ghost_Mode_Assertion_Level);
end if;
Set_Is_Ignored_Ghost_Node (N);
while Present (Prag) loop
Prag_Nam := Pragma_Name (Prag);
- if Prag_Nam = Name_Initial_Condition then
+ -- When Assertion_Levels are used then the pacakage can have
+ -- multiple consecutive Initial_Condition pragmas.
+ -- Find the first one here and then iterate over all of them
+ -- later.
+
+ if Prag_Nam = Name_Initial_Condition and then No (Init_Cond) then
Init_Cond := Prag;
elsif Prag_Nam = Name_Initializes then
Analyze_Initializes_In_Decl_Part (Init);
end if;
- if Present (Init_Cond) then
+ while Present (Init_Cond)
+ and then Pragma_Name (Init_Cond) = Name_Initial_Condition
+ loop
Analyze_Initial_Condition_In_Decl_Part (Init_Cond);
- end if;
+ Init_Cond := Next_Pragma (Init_Cond);
+ end loop;
end if;
-- Restore the SPARK_Mode of the enclosing context after all delayed
with Tbuild; use Tbuild;
with Ttypes; use Ttypes;
with Sem_Mech; use Sem_Mech;
+with Sem_Prag; use Sem_Prag;
with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo;
with Sinfo.Nodes; use Sinfo.Nodes;
procedure Make_Dummy_Index (E : Entity_Id);
-- Called to provide a dummy index field value for Any_Array/Any_String
+ function Make_Assertion_Level_Definition
+ (Nam : Name_Id) return Entity_Id;
+ -- Create an Assertion_Level definition with the given name in the'
+ -- Sandard package.
+
procedure Pack_String_Type (String_Type : Entity_Id);
-- Generate proper tree for pragma Pack that applies to given type, and
-- mark type as having the pragma.
Set_First_Index (E, Index);
end Make_Dummy_Index;
+ -------------------------------------
+ -- Make_Assertion_Level_Definition --
+ -------------------------------------
+
+ function Make_Assertion_Level_Definition (Nam : Name_Id) return Entity_Id
+ is
+ Level : constant Entity_Id := Make_Assertion_Level (Stloc, Nam);
+ begin
+ Insert_Assertion_Level (Level);
+ return Level;
+ end Make_Assertion_Level_Definition;
+
----------------------
-- Pack_String_Type --
----------------------
Set_Size_Known_At_Compile_Time (Standard_Duration);
end Build_Duration;
+ Standard_Level_Static := Make_Assertion_Level_Definition (Name_Static);
+ Standard_Level_Runtime := Make_Assertion_Level_Definition (Name_Runtime);
+ Standard_Level_Default :=
+ Make_Assertion_Level_Definition (Name_uDefault_Assertion_Level);
+
-- Build standard exception type. Note that the type name here is
-- actually used in the generated code, so it must be set correctly.
-- The type Standard_Exception_Type must be consistent with the type
P ("-- characteristics of the Standard types for this compiler");
Write_Eol;
+ P ("pragma Assertion_Level (Runtime);");
+ P ("pragma Assertion_Level (Static);");
+ Write_Eol;
+
P ("package Standard is");
P ("pragma Pure (Standard);");
Write_Eol;
-- determine if there actually is an active Suppress or Unsuppress pragma
-- that applies to the entity.
+-- Child_Levels
+-- Assrtion levels that depend on the given level are considered to be
+-- the child levels of that level.
+
-- Class_Postconditions
-- Defined on subprogram entities. Set if the subprogram has class-wide
-- postconditions. Denotes the (and-then) expression built by merging
-- associates generic parameters with the corresponding instances, in
-- those cases where the instance is an entity.
+-- Ghost_Assertion_Level
+-- Assertion level associated with the declaration of the entity. Its
+-- value is either Empty for non-ghost entities. Standard_Level_Default
+-- for Ghost entities without an assertion level or a user defined
+-- assertion level.
+
-- Has_Aliased_Components [implementation base type only]
-- Defined in array type entities. Indicates that the component type
-- of the array is aliased. Should this also be set for records to
-- used when obtaining the formal kind of a formal parameter (the result
-- is one of E_[In/Out/In_Out]_Parameter).
+-- Parent_Levels
+-- Assrtion levels that the given level depends on are considered to be
+-- parent levels of that level.
+
-- Parent_Subtype [base type only]
-- Defined in E_Record_Type. Set only for derived tagged types, in which
-- case it points to the subtype of the parent type. This is the type
-- Number_Dimensions (synth)
-- (plus type attributes)
+ -- E_Assertion_Level
+ -- Child_Levels
+ -- Parent_Levels
+
-- E_Block
-- Renamed_Entity $$$
-- Renamed_Object $$$
procedure Check_Subprogram_Variant;
-- Emit a call to the internally generated procedure with checks for
- -- aspect Subprogram_Variant, if present and enabled.
+ -- aspect Subprogram_Variant, if present and enabled. Multiple calls are
+ -- added when the subprogram was using Assertion_Levels.
function Inherited_From_Formal (S : Entity_Id) return Entity_Id;
-- Within an instance, a type derived from an untagged formal derived
-- Local variables
- Variant_Prag : constant Node_Id :=
+ Variant_Prag : Node_Id :=
Get_Pragma (Current_Scope, Pragma_Subprogram_Variant);
New_Call : Node_Id;
Variant_Proc : Entity_Id;
begin
- if Present (Variant_Prag) and then Is_Checked (Variant_Prag) then
-
+ while Present (Variant_Prag)
+ and then Is_Checked (Variant_Prag)
+ and then Pragma_Name (Variant_Prag) = Name_Subprogram_Variant
+ loop
Pragma_Arg1 :=
Expression (First (Pragma_Argument_Associations (Variant_Prag)));
-- run-time execution.
if Nkind (Pragma_Arg1) = N_Aggregate then
- pragma Assert
- (Chars
- (First
- (Choices
- (First (Component_Associations (Pragma_Arg1))))) =
- Name_Structural);
+ pragma
+ Assert
+ (Chars
+ (First
+ (Choices
+ (First (Component_Associations (Pragma_Arg1)))))
+ = Name_Structural);
return;
end if;
Variant_Proc := Entity (Pragma_Arg1);
New_Call :=
- Make_Procedure_Call_Statement (Loc,
+ Make_Procedure_Call_Statement
+ (Loc,
Name =>
New_Occurrence_Of (Variant_Proc, Loc),
Parameter_Associations =>
Insert_Action (Call_Node, New_Call);
- pragma Assert (Etype (New_Call) /= Any_Type
- or else Serious_Errors_Detected > 0);
- end if;
+ pragma
+ Assert
+ (Etype (New_Call) /= Any_Type
+ or else Serious_Errors_Detected > 0);
+
+ Variant_Prag := Next_Pragma (Variant_Prag);
+ end loop;
end Check_Subprogram_Variant;
---------------------------
is
Cond : Node_Id;
Error : Node_Id;
-
+ Str : String_Id;
begin
-- Generate:
-- Flag and then not Conseq
Store_String_Chars ("failed contract case at ");
Store_String_Chars (Build_Location_String (Sloc (Conseq)));
+ -- Store the string value as the call to RTE can cause a new unit to
+ -- be loaded which causes new strings to be created.
+
+ Str := End_String;
+
Error :=
Make_Procedure_Call_Statement (Loc,
Name =>
New_Occurrence_Of (RTE (RE_Raise_Assert_Failure), Loc),
Parameter_Associations => New_List (
- Make_String_Literal (Loc, End_String)));
+ Make_String_Literal (Loc, Str)));
if No (Checks) then
Checks :=
Call : Node_Id;
Call_List : List_Id;
Call_Loc : Source_Ptr;
+ Check_Prag : Node_Id;
Expr : Node_Id;
Loc : Source_Ptr;
Proc_Body : Node_Id;
-- pragma Check (Initial_Condition, <Expr>);
-- end <Pack_Id>Initial_Condition;
+ Check_Prag :=
+ Make_Pragma
+ (Loc,
+ Chars => Name_Check,
+ Pragma_Argument_Associations =>
+ New_List
+ (Make_Pragma_Argument_Association
+ (Loc,
+ Expression =>
+ Make_Identifier (Loc, Name_Initial_Condition)),
+ Make_Pragma_Argument_Association
+ (Loc, Expression => New_Copy_Tree (Expr))));
+ Copy_Assertion_Policy_Attributes (Check_Prag, IC_Prag);
+
Proc_Body :=
Make_Subprogram_Body (Loc,
Specification =>
Declarations => Empty_List,
Handled_Statement_Sequence =>
Make_Handled_Sequence_Of_Statements (Loc,
- Statements => New_List (
- Make_Pragma (Loc,
- Chars => Name_Check,
- Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression =>
- Make_Identifier (Loc, Name_Initial_Condition)),
- Make_Pragma_Argument_Association (Loc,
- Expression => New_Copy_Tree (Expr)))))));
+ Statements => New_List (Check_Prag)));
Append_To (Body_List, Proc_Body);
Typ => Expr_Typ,
Curr_Val => New_Occurrence_Of (Curr_Id, Loc),
Old_Val => New_Occurrence_Of (Old_Id, Loc)))));
+ Copy_Assertion_Policy_Attributes (Prag, N);
-- Generate:
-- if Curr /= Old then
-- Prev_Decl and is stored in this parameter for a next call to this
-- routine. Is_Last is True when there are no more variants to process.
+ function Variants_Function_Name (Prag : Node_Id) return Name_Id;
+ -- The name of the variants function is either
+ -- * _variants: if no assertion level was associated with the pragma.
+ -- * _variants_<Assertion_Level> otherwise.
+
----------------------
-- Formal_Param_Map --
----------------------
Expr_Typ : constant Entity_Id := Etype (Expr);
Loc : constant Source_Ptr := Sloc (Expr);
- Old_Id : Entity_Id;
- Old_Decl : Node_Id;
- Curr_Id : Entity_Id;
- Curr_Decl : Node_Id;
- Prag : Node_Id;
+ Old_Id : Entity_Id;
+ Old_Decl : Node_Id;
+ Curr_Id : Entity_Id;
+ Curr_Decl : Node_Id;
+ Check_Prag : Node_Id;
begin
-- Create temporaries that store the old values of the associated
-- Generate:
-- pragma Check (Variant, Curr <|> Old);
- Prag :=
+ Check_Prag :=
Make_Pragma (Loc,
Chars => Name_Check,
Pragma_Argument_Associations => New_List (
Typ => Expr_Typ,
Curr_Val => New_Occurrence_Of (Curr_Id, Loc),
Old_Val => New_Occurrence_Of (Old_Id, Loc)))));
+ Copy_Assertion_Policy_Attributes (Check_Prag, Prag);
-- Generate:
-- if Curr /= Old then
-- pragma.
if Is_Last then
- If_Stmt := Prag;
+ If_Stmt := Check_Prag;
else
If_Stmt :=
Make_If_Statement (Loc,
Make_Op_Ne (Loc,
Left_Opnd => New_Occurrence_Of (Curr_Id, Loc),
Right_Opnd => New_Occurrence_Of (Old_Id, Loc)),
- Then_Statements => New_List (Prag));
+ Then_Statements => New_List (Check_Prag));
end if;
-- Generate:
-- end if;
elsif Is_Last then
- Set_Else_Statements (If_Stmt, New_List (Prag));
+ Set_Else_Statements (If_Stmt, New_List (Check_Prag));
-- Generate:
-- elsif Curr /= Old then
Make_Op_Ne (Loc,
Left_Opnd => New_Occurrence_Of (Curr_Id, Loc),
Right_Opnd => New_Occurrence_Of (Old_Id, Loc)),
- Then_Statements => New_List (Prag)));
+ Then_Statements => New_List (Check_Prag)));
end if;
end Process_Variant;
+ ----------------------------
+ -- Variants_Function_Name --
+ ----------------------------
+
+ function Variants_Function_Name (Prag : Node_Id) return Name_Id is
+ begin
+ if Present (Pragma_Ghost_Assertion_Level (Prag))
+ and then Pragma_Ghost_Assertion_Level (Prag)
+ /= Standard_Level_Default
+ then
+ Get_Name_String (Name_uVariants);
+ Add_Str_To_Name_Buffer ("_");
+ Get_Name_String_And_Append
+ (Chars (Pragma_Ghost_Assertion_Level (Prag)));
+ return Name_Enter;
+ else
+ return Name_uVariants;
+ end if;
+ end Variants_Function_Name;
+
-- Local variables
Loc : constant Source_Ptr := Sloc (Prag);
Proc_Bod : Node_Id;
Proc_Decl : Node_Id;
Proc_Id : Entity_Id;
+ Proc_Nam : Name_Id;
Proc_Spec : Node_Id;
Variant : Node_Id;
-- variant expressions captured at the start of subprogram with their
-- values at the recursive call of the subprogram.
- Proc_Id := Make_Defining_Identifier (Loc, Name_uVariants);
+ Proc_Nam := Variants_Function_Name (Prag);
+
+ Proc_Id := Make_Defining_Identifier (Loc, Proc_Nam);
Proc_Spec :=
Make_Procedure_Specification
-------------------
procedure Add_DIC_Check
- (DIC_Prag : Node_Id;
- DIC_Expr : Node_Id;
- Stmts : in out List_Id)
+ (DIC_Prag : Node_Id; DIC_Expr : Node_Id; Stmts : in out List_Id)
is
- Loc : constant Source_Ptr := Sloc (DIC_Prag);
- Nam : constant Name_Id := Original_Aspect_Pragma_Name (DIC_Prag);
+ Loc : constant Source_Ptr := Sloc (DIC_Prag);
+ Nam : constant Name_Id := Original_Aspect_Pragma_Name (DIC_Prag);
+ Prag : Node_Id;
begin
-- The DIC pragma is ignored, nothing left to do
-- Otherwise the DIC expression must be checked at run time.
-- Generate:
-
+ --
-- pragma Check (<Nam>, <DIC_Expr>);
else
- Append_New_To (Stmts,
- Make_Pragma (Loc,
- Pragma_Identifier =>
- Make_Identifier (Loc, Name_Check),
+ Prag :=
+ Make_Pragma
+ (Loc,
+ Pragma_Identifier =>
+ Make_Identifier (Loc, Name_Check),
+ Pragma_Argument_Associations =>
+ New_List
+ (Make_Pragma_Argument_Association
+ (Loc, Expression => Make_Identifier (Loc, Nam)),
+ Make_Pragma_Argument_Association
+ (Loc, Expression => DIC_Expr)));
- Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression => Make_Identifier (Loc, Nam)),
+ Copy_Assertion_Policy_Attributes (Prag, DIC_Prag);
- Make_Pragma_Argument_Association (Loc,
- Expression => DIC_Expr))));
+ Append_New_To (Stmts, Prag);
end if;
-- Add the pragma to the list of processed pragmas
DIC_Typ : Entity_Id;
Dummy_1 : Entity_Id;
Dummy_2 : Entity_Id;
+ Prag : Node_Id;
Proc_Body : Node_Id;
Proc_Body_Id : Entity_Id;
Proc_Decl : Node_Id;
if Partial_DIC then
pragma Assert (Present (Priv_Typ));
- if Has_Own_DIC (Work_Typ) then -- If we're testing this then maybe
- Add_Own_DIC -- we shouldn't be calling Find_DIC_Typ above???
- (DIC_Prag => DIC_Prag,
- DIC_Typ => DIC_Typ, -- Should this just be Work_Typ???
- Obj_Id => Obj_Id,
- Stmts => Stmts);
+ if Has_Own_DIC (Work_Typ) then
+ -- If we're testing this then maybe
+
+ Prag := DIC_Prag;
+ while Present (Prag)
+ and then Nkind (Prag) = N_Pragma
+ and then Pragma_Name (Prag) = Name_Default_Initial_Condition
+ and then (Prag = DIC_Prag
+ or else From_Same_Pragma (Prag, DIC_Prag))
+ loop
+ Add_Own_DIC -- we shouldn't be calling Find_DIC_Typ above???
+ (DIC_Prag => Prag,
+ DIC_Typ => DIC_Typ, -- Should this just be Work_Typ???
+ Obj_Id => Obj_Id,
+ Stmts => Stmts);
+ Next_Rep_Item (Prag);
+ end loop;
end if;
-- Otherwise, the "full" DIC procedure verifies the DICs inherited from
Ploc : constant Source_Ptr := Sloc (Prag);
Str_Arg : constant Node_Id := Next (Next (First (Args)));
- Assoc : List_Id;
- Str : String_Id;
+ Assoc : List_Id;
+ Check_Prag : Node_Id;
+ Str : String_Id;
begin
-- The invariant is ignored, nothing left to do
-- Generate:
-- pragma Check (<Nam>, <Expr>, <Str>);
- Append_New_To (Checks,
+ Check_Prag :=
Make_Pragma (Ploc,
- Chars => Name_Check,
- Pragma_Argument_Associations => Assoc));
+ Chars => Name_Check,
+ Pragma_Argument_Associations => Assoc);
+
+ Copy_Assertion_Policy_Attributes (Check_Prag, Prag);
+
+ Append_New_To (Checks, Check_Prag);
end if;
-- Output an info message when inheriting an invariant and the
Ancestor_Part,
Atomic_Sync_Required,
Array_Aggregate,
+ Aspect_Ghost_Assertion_Level,
Aspect_On_Partial_View,
Aspect_Rep_Item,
Aspect_Specifications,
Null_Statement,
Object_Definition,
Of_Present,
+ Original_Aspect,
Original_Discriminant,
Original_Entity,
+ Original_Pragma,
Others_Discrete_Choices,
Out_Present,
Parameter_Associations,
Parent_With,
Position,
Pragma_Argument_Associations,
+ Pragma_Ghost_Assertion_Level,
Pragma_Identifier,
Pragmas_After,
Pragmas_Before,
Can_Never_Be_Null,
Can_Use_Internal_Rep,
Checks_May_Be_Suppressed,
+ Child_Levels,
Class_Postconditions,
Class_Preconditions,
Class_Preconditions_Subprogram,
Full_View,
Generic_Homonym,
Generic_Renamings,
+ Ghost_Assertion_Level,
Has_Aliased_Components,
Has_Alignment_Clause,
Has_All_Calls_Remote,
Overridden_Operation,
Package_Instantiation,
Packed_Array_Impl_Type,
+ Parent_Levels,
Parent_Subtype,
Part_Of_Constituents,
Part_Of_References,
Sm (First_Rep_Item, Node_Id),
Sm (Freeze_Node, Node_Id),
Sm (From_Limited_With, Flag),
+ Sm (Ghost_Assertion_Level, Node_Id),
Sm (Has_Aliased_Components, Flag, Impl_Base_Type_Only),
Sm (Has_Alignment_Clause, Flag),
Sm (Has_All_Calls_Remote, Flag),
Sm (SPARK_Pragma, Node_Id),
Sm (SPARK_Pragma_Inherited, Flag)));
+ Cc (E_Assertion_Level, Entity_Kind,
+ -- An assertion level. Used to associate a level indicator to an
+ -- assertion like construct. Constructs assigned with a certain level
+ -- can be disabled through pragma Assertion_Policy. Levels can form a
+ -- hierarchy. A declaration of a level can include a list of levels
+ -- this level depends on known as the Parent_Levels. An opposite list
+ -- is also kept to store all the levels that depend on it known as the
+ -- Child_Levels.
+ (Sm (Child_Levels, Elist_Id),
+ Sm (Parent_Levels, Elist_Id)));
+
-- Union types. These don't fit into the normal parent/child hierarchy
-- above.
(Sy (Identifier, Node_Id, Default_Empty),
Sy (Expression, Node_Id, Default_Empty),
Sy (Class_Present, Flag),
+ Sm (Aspect_Ghost_Assertion_Level, Node_Id),
Sm (Aspect_On_Partial_View, Flag),
Sm (Aspect_Rep_Item, Node_Id),
Sm (Aspect_Subprograms, Elist_Id),
Sm (Is_Delayed_Aspect, Flag),
Sm (Is_Disabled, Flag),
Sm (Is_Ignored, Flag),
- Sm (Next_Rep_Item, Node_Id)));
+ Sm (Next_Rep_Item, Node_Id),
+ Sm (Original_Aspect, Node_Id)));
Cc (N_Call_Marker, Node_Kind,
(Sm (Is_Declaration_Level_Node, Flag),
Sm (Is_Ignored_Ghost_Pragma, Flag),
Sm (Next_Pragma, Node_Id),
Sm (Next_Rep_Item, Node_Id),
+ Sm (Original_Pragma, Node_Id),
+ Sm (Pragma_Ghost_Assertion_Level, Node_Id),
Sm (Uneval_Old_Accept, Flag),
Sm (Uneval_Old_Warn, Flag)));
-- Concrete entity types:
E_Void,
+ E_Assertion_Level,
E_Component,
E_Constant,
E_Discriminant,
with Sem_Disp; use Sem_Disp;
with Sem_Eval; use Sem_Eval;
with Sem_Prag; use Sem_Prag;
-with Sem_Res; use Sem_Res;
with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo;
with Sinfo.Nodes; use Sinfo.Nodes;
with Sinfo.Utils; use Sinfo.Utils;
with Snames; use Snames;
+with Stand; use Stand;
with Table;
package body Ghost is
Table_Increment => Alloc.Ignored_Ghost_Nodes_Increment,
Table_Name => "Ignored_Ghost_Nodes");
+ ---------------------
+ -- Local variables --
+ ---------------------
+
+ Assertion_Level_Error_Msg : constant String :=
+ "incompatible assertion levels in effect";
+
+ Ghost_Policy_Error_Msg : constant String :=
+ "incompatible ghost policies in effect";
+
-----------------------
-- Local subprograms --
-----------------------
- procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type);
- pragma Inline (Install_Ghost_Mode);
- -- Install Ghost mode Mode as the Ghost mode in effect
+ function Assertion_Level_To_Name (Level : Entity_Id) return Name_Id;
+ -- Returns No_Name if there is no Level or the name of the Level.
+
+ procedure Check_Valid_Ghost_Declaration (N : Node_Id);
+ -- Check that the declaration for a Ghost node N has a valid
+ -- Assertion_Policy and a valid Assertion_Level.
+
+ function Get_Ghost_Aspect (N : Node_Id) return Node_Id;
+ -- Returns the Ghost aspect for a given node if it has one.
- procedure Install_Ghost_Region (Mode : Name_Id; N : Node_Id);
+ function Get_Ghost_Pragma (N : Node_Id) return Node_Id;
+ -- Return the Ghost pragma following this node.
+
+ function Get_Ghost_Assertion_Level (N : Node_Id) return Entity_Id;
+ -- Returns the Assertion_Level entity if the node has a Ghost aspect and
+ -- the Ghost aspect is using an Assertion_Level.
+
+ function Ghost_Policy_In_Effect (Id : Entity_Id) return Name_Id;
+ -- Returns the first Assertion Policy in place for either Ghost or the
+ -- Assertion_Level associated with Ghost aspect on the the declaration node
+ -- Decl.
+
+ procedure Install_Ghost_Region
+ (Mode : Name_Id;
+ N : Node_Id;
+ Level : Entity_Id);
pragma Inline (Install_Ghost_Region);
-- Install a Ghost region comprised of mode Mode and ignored region start
- -- node N.
+ -- node N and Level as the Assertion_Level that was associated with it.
function Is_Subject_To_Ghost (N : Node_Id) return Boolean;
-- Determine whether declaration or body N is subject to aspect or pragma
-- been analyzed yet, but the context needs to establish the "ghostness"
-- of N.
+ procedure Mark_And_Set_Ghost_Region (N : Node_Id; Id : Entity_Id);
+ -- Install a new ghost region for N based on the active policy applied for
+ -- Id. Additionally if the policy is ignored mark and set the node as an
+ -- ignored ghost region.
+
procedure Mark_Ghost_Declaration_Or_Body
- (N : Node_Id;
- Mode : Name_Id);
+ (N : Node_Id;
+ Mode : Name_Id;
+ Level : Entity_Id);
-- Mark the defining entity of declaration or body N as Ghost depending on
-- mode Mode. Mark all formals parameters when N denotes a subprogram or a
- -- body.
+ -- body. Additionally set level as the Ghost_Assertion_Level for all of
+ -- them.
procedure Record_Ignored_Ghost_Node (N : Node_Or_Entity_Id);
-- Save ignored Ghost node or entity N in table Ignored_Ghost_Nodes for
-- later elimination.
+ ------------------------------
+ -- Assertion_Level_From_Arg --
+ ------------------------------
+
+ function Assertion_Level_From_Arg (Arg : Node_Id) return Entity_Id is
+ Expr : constant Node_Id := Get_Pragma_Arg (Arg);
+ Level : Entity_Id;
+
+ begin
+ -- Aspect Ghost without an expression uses Standard_Level_Default
+
+ if No (Expr) then
+ return Standard_Level_Default;
+ end if;
+
+ -- Check if the expression matches a static boolean expression first
+
+ Preanalyze_And_Resolve_Without_Errors (Expr);
+ if Is_OK_Static_Expression (Expr) then
+ if Is_True (Expr_Value (Expr)) then
+ return Standard_Level_Default;
+ else
+ -- Ghost => False is considered to be non-ghost
+
+ return Empty;
+ end if;
+ end if;
+
+ -- Alternatively the argument could be an Assertion_Level
+
+ if Nkind (Expr) = N_Identifier
+ and then Present (Get_Assertion_Level (Chars (Expr)))
+ then
+ Level := Get_Assertion_Level (Chars (Expr));
+ if Present (Level) then
+ return Level;
+ end if;
+ end if;
+
+ -- We are dealing with a malformed ghost argument.
+ -- An error will be emitted when the pragma is analyzed.
+
+ return Empty;
+ end Assertion_Level_From_Arg;
+
+ -----------------------------
+ -- Assertion_Level_To_Name --
+ -----------------------------
+
+ function Assertion_Level_To_Name (Level : Entity_Id) return Name_Id is
+ begin
+ if No (Level) then
+ return No_Name;
+ end if;
+
+ return Chars (Level);
+ end Assertion_Level_To_Name;
+
----------------------------
-- Check_Ghost_Completion --
----------------------------
(Prev_Id : Entity_Id;
Compl_Id : Entity_Id)
is
- Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
+ Policy : Name_Id;
begin
-- Nothing to do if one of the views is missing
if No (Prev_Id) or else No (Compl_Id) then
- null;
+ return;
+ end if;
+
+ Policy := Ghost_Policy_In_Effect (Prev_Id);
-- The Ghost policy in effect at the point of declaration and at the
-- point of completion must match (SPARK RM 6.9(16)).
- elsif Is_Checked_Ghost_Entity (Prev_Id)
+ if Is_Checked_Ghost_Entity (Prev_Id)
and then Policy = Name_Ignore
then
Error_Msg_Sloc := Sloc (Compl_Id);
- Error_Msg_N ("incompatible ghost policies in effect", Prev_Id);
+ Error_Msg_N (Ghost_Policy_Error_Msg, Prev_Id);
Error_Msg_N ("\& declared with ghost policy `Check`", Prev_Id);
Error_Msg_N ("\& completed # with ghost policy `Ignore`", Prev_Id);
then
Error_Msg_Sloc := Sloc (Compl_Id);
- Error_Msg_N ("incompatible ghost policies in effect", Prev_Id);
+ Error_Msg_N (Ghost_Policy_Error_Msg, Prev_Id);
Error_Msg_N ("\& declared with ghost policy `Ignore`", Prev_Id);
Error_Msg_N ("\& completed # with ghost policy `Check`", Prev_Id);
end if;
--
-- * Contain a reference to a Ghost entity
- function Is_OK_Statement (Stmt : Node_Id) return Boolean;
+ function Is_OK_Statement
+ (Stmt : Node_Id; Id : Entity_Id; Call_Arg : Node_Id) return Boolean;
-- Determine whether node Stmt is a suitable context for a reference
-- to a Ghost entity. To qualify as such, Stmt must either
--
function Is_OK_Pragma (Prag : Node_Id; Id : Entity_Id) return Boolean
is
- procedure Check_Policies (Prag_Nam : Name_Id);
+ procedure Check_Policies;
-- Verify that the Ghost policy in effect at the point of the
- -- declaration of Ghost entity Id (if present) is the same as the
- -- assertion policy for pragma name Prag_Nam. Emit an error if
- -- this is not the case.
+ -- declaration of Ghost entity Id (if present) is the same as
+ -- the assertion policy for the pragma. Emit an error if this
+ -- is not the case.
--------------------
-- Check_Policies --
--------------------
- procedure Check_Policies (Prag_Nam : Name_Id) is
- AP : constant Name_Id := Check_Kind (Prag_Nam);
-
+ procedure Check_Policies is
begin
-- If the Ghost policy in effect at the point of the
-- declaration of Ghost entity Id is Ignore, then the assertion
if Present (Id)
and then not Is_Checked_Ghost_Entity (Id)
- and then AP /= Name_Ignore
+ and then not Is_Ignored (Prag)
then
- Error_Msg_N
- ("incompatible ghost policies in effect",
- Ghost_Ref);
+ Error_Msg_N (Ghost_Policy_Error_Msg, Ghost_Ref);
Error_Msg_NE
("\ghost entity & has policy `Ignore`",
Ghost_Ref, Ghost_Id);
-
- Error_Msg_Name_1 := AP;
Error_Msg_N
- ("\assertion expression has policy %", Ghost_Ref);
+ ("\assertion expression has policy `Check`",
+ Ghost_Ref);
end if;
end Check_Policies;
-- Start of processing for Is_OK_Pragma
begin
- if Nkind (Prag) = N_Pragma then
- Prag_Id := Get_Pragma_Id (Prag);
- Prag_Nam := Original_Aspect_Pragma_Name (Prag);
+ if Nkind (Prag) /= N_Pragma then
+ return False;
+ end if;
- -- A pragma that applies to a Ghost construct or specifies an
- -- aspect of a Ghost entity is a Ghost pragma (SPARK RM 6.9(3))
+ Prag_Id := Get_Pragma_Id (Prag);
+ Prag_Nam := Original_Aspect_Pragma_Name (Prag);
- if Is_Ghost_Pragma (Prag) then
- return True;
+ -- A pragma may not be analyzed, so that its Ghost status is
+ -- not determined yet, but it is guaranteed to be Ghost when
+ -- referencing a Ghost entity.
- -- A pragma may not be analyzed, so that its Ghost status is
- -- not determined yet, but it is guaranteed to be Ghost when
- -- referencing a Ghost entity.
+ if Prag_Nam
+ in Name_Annotate
+ | Name_Compile_Time_Error
+ | Name_Compile_Time_Warning
+ | Name_Unreferenced
+ then
+ return True;
- elsif Prag_Nam in Name_Annotate
- | Name_Compile_Time_Error
- | Name_Compile_Time_Warning
- | Name_Unreferenced
- then
- return True;
+ -- An assertion expression pragma is Ghost when it contains a
+ -- reference to a Ghost entity (SPARK RM 6.9(10)), except for
+ -- predicate pragmas (SPARK RM 6.9(11)).
- -- An assertion expression pragma is Ghost when it contains a
- -- reference to a Ghost entity (SPARK RM 6.9(10)), except for
- -- predicate pragmas (SPARK RM 6.9(11)).
+ elsif Is_Valid_Assertion_Kind (Prag_Nam)
+ and then Assertion_Expression_Pragma (Prag_Id)
+ and then Prag_Id /= Pragma_Predicate
+ then
+ -- Ensure that the assertion policy and the Ghost policy are
+ -- compatible (SPARK RM 6.9(20)).
- elsif Assertion_Expression_Pragma (Prag_Id)
- and then Prag_Id /= Pragma_Predicate
- then
- -- Ensure that the assertion policy and the Ghost policy are
- -- compatible (SPARK RM 6.9(20)).
+ Check_Policies;
+ return True;
- Check_Policies (Prag_Nam);
- return True;
+ -- A pragma that applies to a Ghost construct or specifies an
+ -- aspect of a Ghost entity is a Ghost pragma (SPARK RM 6.9(3))
- -- Several pragmas that may apply to a non-Ghost entity are
- -- treated as Ghost when they contain a reference to a Ghost
- -- entity (SPARK RM 6.9(11)).
+ elsif Is_Ghost_Pragma (Prag) then
+ return True;
- elsif Prag_Nam in Name_Global
- | Name_Depends
- | Name_Initializes
- | Name_Refined_Global
- | Name_Refined_Depends
- | Name_Refined_State
- then
- return True;
- end if;
+ -- Several pragmas that may apply to a non-Ghost entity are
+ -- treated as Ghost when they contain a reference to a Ghost
+ -- entity (SPARK RM 6.9(11)).
+
+ elsif Prag_Nam
+ in Name_Global
+ | Name_Depends
+ | Name_Initializes
+ | Name_Refined_Global
+ | Name_Refined_Depends
+ | Name_Refined_State
+ then
+ return True;
end if;
return False;
-- Is_OK_Statement --
---------------------
- function Is_OK_Statement (Stmt : Node_Id) return Boolean is
+ function Is_OK_Statement
+ (Stmt : Node_Id; Id : Entity_Id; Call_Arg : Node_Id) return Boolean
+ is
+ procedure Check_Assignment_Policies (Assignee : Entity_Id);
+ -- Check that:
+ -- * An ignored entity is not used to modify a checked ghost
+ -- entity in an assignment.
+ -- * A checked ghost assignment is not used in an ignored ghost
+ -- region.
+ -- * The level of the ghost region depends on the level of the
+ -- ghost assignment.
+
+ procedure Check_Procedure_Call_Policies (Callee : Entity_Id);
+ -- Check that
+ -- * the a checked call argument is not modified by an ignored
+ -- procedure call.
+ -- * the level of the modified call argument depends on the level
+ -- of the call.
+
+ function Is_Modified_By_Call
+ (Call : Node_Id; Call_Arg : Node_Id; Callee : Entity_Id)
+ return Boolean;
+ -- Check that Call_Arg was used in the call and that the formal
+ -- for that argument was either out or in-out.
+
+ -------------------------------
+ -- Check_Assignment_Policies --
+ -------------------------------
+
+ procedure Check_Assignment_Policies (Assignee : Entity_Id) is
+ A_Policy : constant Name_Id :=
+ Ghost_Policy_In_Effect (Assignee);
+ A_Level : constant Entity_Id :=
+ Ghost_Assertion_Level (Assignee);
+ Id_Policy : constant Name_Id := Ghost_Policy_In_Effect (Id);
+ Region_Policy : constant Ghost_Mode_Type :=
+ Ghost_Config.Ghost_Mode;
+ Region_Level : constant Entity_Id :=
+ Ghost_Config.Ghost_Mode_Assertion_Level;
+ begin
+ if A_Policy = Name_Check and then Id_Policy = Name_Ignore then
+ Error_Msg_Sloc := Sloc (Ghost_Ref);
+
+ Error_Msg_N (Ghost_Policy_Error_Msg, Ghost_Ref);
+ Error_Msg_NE ("\& has ghost policy `Ignore`", Ghost_Ref, Id);
+ Error_Msg_NE
+ ("\& used # to modify an entity with `Check`",
+ Ghost_Ref,
+ Id);
+ end if;
+
+ if A_Policy = Name_Check and then Region_Policy = Ignore then
+ Error_Msg_N (Ghost_Policy_Error_Msg, Stmt);
+ Error_Msg_NE ("\& has ghost policy `Check`", Stmt, Assignee);
+ Error_Msg_NE
+ ("\& is modified in a region with `Ignore`",
+ Stmt,
+ Assignee);
+ end if;
+
+ if Present (Region_Level)
+ and then not Is_Assertion_Level_Dependent
+ (Region_Level, A_Level)
+ then
+ Error_Msg_Sloc := Sloc (Stmt);
+
+ Error_Msg_N (Assertion_Level_Error_Msg, Stmt);
+ Error_Msg_Name_1 := Chars (A_Level);
+ Error_Msg_NE ("\& has assertion level %", Stmt, Assignee);
+ Error_Msg_Name_1 := Chars (Region_Level);
+ Error_Msg_NE
+ ("\& is modified within a region with %", Stmt, Id);
+ Error_Msg_Name_1 := Chars (Region_Level);
+ Error_Msg_NE
+ ("\assertion level of & should depend on %",
+ Stmt,
+ Assignee);
+ end if;
+ end Check_Assignment_Policies;
+
+ -----------------------------------
+ -- Check_Procedure_Call_Policies --
+ -----------------------------------
+
+ procedure Check_Procedure_Call_Policies (Callee : Entity_Id) is
+ Id_Level : constant Entity_Id := Ghost_Assertion_Level (Id);
+ Id_Policy : constant Name_Id := Ghost_Policy_In_Effect (Id);
+
+ Call_Level : Entity_Id;
+ Call_Policy : Name_Id;
+ begin
+ if No (Callee) then
+ return;
+ end if;
+
+ -- Checks apply only if we are processing a call argument that
+ -- is modified by the call.
+
+ if No (Call_Arg)
+ or else not Is_Modified_By_Call (Stmt, Call_Arg, Callee)
+ then
+ return;
+ end if;
+
+ Call_Policy := Ghost_Policy_In_Effect (Callee);
+ Call_Level := Ghost_Assertion_Level (Callee);
+
+ if Id_Policy = Name_Check
+ and then Call_Policy = Name_Ignore
+ then
+ Error_Msg_Sloc := Sloc (Ghost_Ref);
+ Error_Msg_N (Ghost_Policy_Error_Msg, Ghost_Ref);
+ Error_Msg_NE ("\& has ghost policy `Check`", Ghost_Ref, Id);
+ Error_Msg_NE
+ ("\& is modified # by a procedure with `Ignore`",
+ Ghost_Ref,
+ Id);
+ end if;
+
+ if not Is_Assertion_Level_Dependent (Id_Level, Call_Level) then
+ Error_Msg_Sloc := Sloc (Ghost_Ref);
+
+ Error_Msg_N (Assertion_Level_Error_Msg, Ghost_Ref);
+ Error_Msg_Name_1 := Chars (Id_Level);
+ Error_Msg_NE ("\& has assertion level %", Ghost_Ref, Id);
+ Error_Msg_Name_1 := Chars (Call_Level);
+ Error_Msg_NE
+ ("\& is modified # by a procedure with %", Ghost_Ref, Id);
+ Error_Msg_Name_1 := Chars (Call_Level);
+ Error_Msg_NE
+ ("\assertion level of & should depend on %",
+ Ghost_Ref,
+ Id);
+ end if;
+ end Check_Procedure_Call_Policies;
+
+ -------------------------
+ -- Is_Modified_By_Call --
+ -------------------------
+
+ function Is_Modified_By_Call
+ (Call : Node_Id; Call_Arg : Node_Id; Callee : Entity_Id)
+ return Boolean
+ is
+ Form : Node_Id;
+ Act : Node_Id;
+ begin
+ Act := First_Actual (Call);
+ Form := First_Formal (Callee);
+
+ while Present (Form) and then Present (Act) loop
+ if Act = Call_Arg then
+ return
+ Ekind (Form) in E_Out_Parameter | E_In_Out_Parameter;
+ end if;
+
+ Next_Formal (Form);
+ Next_Actual (Act);
+ end loop;
+
+ return False;
+ end Is_Modified_By_Call;
+
+ -- Start of processing for Is_OK_Statement
+
begin
-- An assignment statement is Ghost when the target is a Ghost
-- entity.
if Nkind (Stmt) = N_Assignment_Statement then
- return Is_Ghost_Assignment (Stmt);
+ if Is_Ghost_Assignment (Stmt) then
+ Check_Assignment_Policies
+ (Get_Enclosing_Ghost_Entity (Name (Stmt)));
+
+ return True;
+ end if;
-- A procedure call is Ghost when it calls a Ghost procedure
elsif Nkind (Stmt) = N_Procedure_Call_Statement then
- return Is_Ghost_Procedure_Call (Stmt);
+ if Is_Ghost_Procedure_Call (Stmt) then
+ Check_Procedure_Call_Policies (Get_Subprogram_Entity (Stmt));
+ return True;
+ end if;
-- Special cases
-- Local variables
- Par : Node_Id;
+ Par : Node_Id;
+ Prev : Node_Id;
-- Start of processing for Is_OK_Ghost_Context
begin
- -- The context is Ghost when it appears within a Ghost package or
- -- subprogram.
-
- if Ghost_Config.Ghost_Mode > None then
- return True;
-
-- Routine Expand_Record_Extension creates a parent subtype without
-- inserting it into the tree. There is no good way of recognizing
-- this special case as there is no parent. Try to approximate the
-- context.
- elsif No (Parent (Context)) and then Is_Tagged_Type (Ghost_Id) then
+ if No (Parent (Context)) and then Is_Tagged_Type (Ghost_Id) then
return True;
-- Otherwise climb the parent chain looking for a suitable Ghost
else
Par := Context;
+ Prev := Empty;
while Present (Par) loop
- if Is_Ignored_Ghost_Node (Par) then
- return True;
-
-- It is not possible to check correct use of Ghost entities
-- in generic instantiations until after the generic has been
-- resolved. Postpone that verification to after resolution.
- elsif Nkind (Par) = N_Generic_Association then
+ if Nkind (Par) = N_Generic_Association then
return True;
-- A reference to a Ghost entity can appear within an aspect
elsif Is_OK_Pragma (Par, Ghost_Id) then
return True;
- elsif Is_OK_Statement (Par) then
+ elsif Is_OK_Statement (Par, Ghost_Id, Prev) then
return True;
-- Prevent the search from going too far
exit;
end if;
+ Prev := Par;
Par := Parent (Par);
end loop;
------------------------
procedure Check_Ghost_Policy (Id : Entity_Id; Ref : Node_Id) is
- Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
-
+ Ghost_Region : constant Node_Id := Ghost_Config.Current_Region;
+ Region_Policy : constant Ghost_Mode_Type := Ghost_Config.Ghost_Mode;
begin
+ -- Ghost entities can be referenced inside a renaming declaration if
+ -- used within a renaming declaration.
+
+ if No (Ghost_Region)
+ or else Nkind (Ghost_Region)
+ in N_Object_Renaming_Declaration
+ | N_Subprogram_Renaming_Declaration
+ then
+ return;
+ end if;
+
-- The Ghost policy in effect a the point of declaration and at the
-- point of use must match (SPARK RM 6.9(15)).
if Is_Checked_Ghost_Entity (Id)
- and then Policy = Name_Ignore
+ and then Region_Policy = Ignore
and then Known_To_Be_Assigned (Ref)
then
- Error_Msg_Sloc := Sloc (Ref);
-
- Error_Msg_N ("incompatible ghost policies in effect", Ref);
+ Error_Msg_N (Ghost_Policy_Error_Msg, Ref);
Error_Msg_NE ("\& declared with ghost policy `Check`", Ref, Id);
+ Error_Msg_Sloc := Sloc (Ref);
Error_Msg_NE ("\& used # with ghost policy `Ignore`", Ref, Id);
+ end if;
- elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then
- Error_Msg_Sloc := Sloc (Ref);
+ if No (Ghost_Region)
+ or else (Nkind (Ghost_Region) = N_Pragma
+ and then Get_Pragma_Id (Ghost_Region)
+ in Pragma_Global
+ | Pragma_Depends
+ | Pragma_Refined_Global
+ | Pragma_Refined_Depends
+ | Pragma_Initializes
+ | Pragma_Refined_State)
+ then
+ return;
+ end if;
- Error_Msg_N ("incompatible ghost policies in effect", Ref);
+ if Is_Ignored_Ghost_Entity (Id) and then Region_Policy = Check
+ then
+ Error_Msg_N (Ghost_Policy_Error_Msg, Ref);
Error_Msg_NE ("\& declared with ghost policy `Ignore`", Ref, Id);
+ Error_Msg_Sloc := Sloc (Ref);
Error_Msg_NE ("\& used # with ghost policy `Check`", Ref, Id);
end if;
end Check_Ghost_Policy;
return;
end if;
- -- Once it has been established that the reference to the Ghost entity
- -- is within a suitable context, ensure that the policy at the point of
- -- declaration and at the point of use match.
-
- if Is_OK_Ghost_Context (Ghost_Ref) then
- if Present (Ghost_Id) then
- Check_Ghost_Policy (Ghost_Id, Ghost_Ref);
- end if;
-
- -- Otherwise the Ghost entity appears in a non-Ghost context and affects
+ -- If the Ghost entity appears in a non-Ghost context and affects
-- its behavior or value (SPARK RM 6.9(10,11)).
- else
+ if not Is_OK_Ghost_Context (Ghost_Ref) then
Error_Msg_N ("ghost entity cannot appear in this context", Ghost_Ref);
-- When the Ghost entity appears in a pragma Predicate, explain the
& "or use a type invariant on a private type", Ghost_Ref);
end if;
end if;
+
+ -- Once it has been established that the reference to the Ghost entity
+ -- is within a suitable context, ensure that the policy at the point of
+ -- declaration and at the point of use match.
+
+ if Present (Ghost_Id) then
+ Check_Ghost_Policy (Ghost_Id, Ghost_Ref);
+ end if;
end Check_Ghost_Context;
------------------------------------------------
end if;
end Check_Ghost_Context_In_Generic_Association;
+ -----------------------------------
+ -- Check_Valid_Ghost_Declaration --
+ -----------------------------------
+
+ procedure Check_Valid_Ghost_Declaration (N : Node_Id) is
+ procedure Check_Valid_Assertion_Level (Id : Entity_Id; Ref : Node_Id);
+ -- Check that the the assertion level of the declared entity is
+ -- compatible with assertion level of the ghost region.
+
+ procedure Check_Valid_Ghost_Policy (Id : Entity_Id; Ref : Node_Id);
+ -- Check that the declared identifier does not have a Checked assertion
+ -- policy while being declared inside an ignored ghost region.
+
+ ---------------------------------
+ -- Check_Valid_Assertion_Level --
+ ---------------------------------
+
+ procedure Check_Valid_Assertion_Level (Id : Entity_Id; Ref : Node_Id) is
+ Id_Level : constant Entity_Id := Ghost_Assertion_Level (Id);
+ Region_Level : constant Entity_Id :=
+ Ghost_Config.Ghost_Mode_Assertion_Level;
+ begin
+ -- This check is not applied for generic isntantiations
+
+ if Is_Generic_Instance (Id) then
+ return;
+ end if;
+
+ if not Is_Assertion_Level_Dependent (Id_Level, Region_Level) then
+ Error_Msg_Sloc := Sloc (Ref);
+
+ Error_Msg_N (Assertion_Level_Error_Msg, Ref);
+ Error_Msg_Name_1 := Chars (Id_Level);
+ Error_Msg_NE ("\& has assertion level %", Ref, Id);
+ Error_Msg_Name_1 := Chars (Region_Level);
+ Error_Msg_NE ("\& is declared within a region with %", Ref, Id);
+ Error_Msg_Name_1 := Chars (Region_Level);
+ Error_Msg_NE ("\assertion level of & should depend on %", Ref, Id);
+ end if;
+ end Check_Valid_Assertion_Level;
+
+ ------------------------------
+ -- Check_Valid_Ghost_Policy --
+ ------------------------------
+
+ procedure Check_Valid_Ghost_Policy (Id : Entity_Id; Ref : Node_Id) is
+ Policy : constant Name_Id := Ghost_Policy_In_Effect (Id);
+ begin
+ if Ghost_Config.Ghost_Mode = Ignore and then Policy = Name_Check
+ then
+ Error_Msg_Sloc := Sloc (Ref);
+
+ Error_Msg_N (Ghost_Policy_Error_Msg, Ref);
+ Error_Msg_NE ("\& has ghost policy `Check`", Ref, Id);
+ Error_Msg_NE
+ ("\& is declared # within ghost policy `Ignore`", Ref, Id);
+ end if;
+ end Check_Valid_Ghost_Policy;
+
+ -- Local variables
+
+ Id : constant Entity_Id := Defining_Entity (N);
+
+ -- Start of processing for Check_Valid_Ghost_Declaration
+ begin
+ if not Is_Ghost_Entity (Id) or else Ghost_Config.Ghost_Mode = None
+ then
+ return;
+ end if;
+
+ Check_Valid_Ghost_Policy (Id, N);
+ Check_Valid_Assertion_Level (Id, N);
+ end Check_Valid_Ghost_Declaration;
+
---------------------------------------------
-- Check_Ghost_Formal_Procedure_Or_Package --
---------------------------------------------
Over_Subp : Entity_Id;
begin
- if Present (Subp) and then Present (Overridden_Subp) then
- Over_Subp := Ultimate_Alias (Overridden_Subp);
- Deriv_Typ := Find_Dispatching_Type (Subp);
-
- -- A Ghost primitive of a non-Ghost type extension cannot override an
- -- inherited non-Ghost primitive (SPARK RM 6.9(8)).
-
- if Is_Ghost_Entity (Subp)
- and then Present (Deriv_Typ)
- and then not Is_Ghost_Entity (Deriv_Typ)
- and then not Is_Ghost_Entity (Over_Subp)
- and then not Is_Abstract_Subprogram (Over_Subp)
- then
- Error_Msg_N ("incompatible overriding in effect", Subp);
+ if No (Subp) or else No (Overridden_Subp) then
+ return;
+ end if;
- Error_Msg_Sloc := Sloc (Over_Subp);
- Error_Msg_N ("\& declared # as non-ghost subprogram", Subp);
+ Over_Subp := Ultimate_Alias (Overridden_Subp);
+ Deriv_Typ := Find_Dispatching_Type (Subp);
- Error_Msg_Sloc := Sloc (Subp);
- Error_Msg_N ("\overridden # with ghost subprogram", Subp);
- end if;
+ -- A Ghost primitive of a non-Ghost type extension cannot override an
+ -- inherited non-Ghost primitive (SPARK RM 6.9(8)).
- -- A non-Ghost primitive of a type extension cannot override an
- -- inherited Ghost primitive (SPARK RM 6.9(8)).
+ if Is_Ghost_Entity (Subp)
+ and then Present (Deriv_Typ)
+ and then not Is_Ghost_Entity (Deriv_Typ)
+ and then not Is_Ghost_Entity (Over_Subp)
+ and then not Is_Abstract_Subprogram (Over_Subp)
+ then
+ Error_Msg_N ("incompatible overriding in effect", Subp);
- if Is_Ghost_Entity (Over_Subp)
- and then not Is_Ghost_Entity (Subp)
- and then not Is_Abstract_Subprogram (Subp)
- then
- Error_Msg_N ("incompatible overriding in effect", Subp);
+ Error_Msg_Sloc := Sloc (Over_Subp);
+ Error_Msg_N ("\& declared # as non-ghost subprogram", Subp);
- Error_Msg_Sloc := Sloc (Over_Subp);
- Error_Msg_N ("\& declared # as ghost subprogram", Subp);
+ Error_Msg_Sloc := Sloc (Subp);
+ Error_Msg_N ("\overridden # with ghost subprogram", Subp);
+ end if;
- Error_Msg_Sloc := Sloc (Subp);
- Error_Msg_N ("\overridden # with non-ghost subprogram", Subp);
- end if;
+ -- A non-Ghost primitive of a type extension cannot override an
+ -- inherited Ghost primitive (SPARK RM 6.9(8)).
- if Present (Deriv_Typ)
- and then not Is_Ignored_Ghost_Entity (Deriv_Typ)
- then
- -- When a tagged type is either non-Ghost or checked Ghost and
- -- one of its primitives overrides an inherited operation, the
- -- overridden operation of the ancestor type must be ignored Ghost
- -- if the primitive is ignored Ghost (SPARK RM 6.9(19)).
+ if Is_Ghost_Entity (Over_Subp)
+ and then not Is_Ghost_Entity (Subp)
+ and then not Is_Abstract_Subprogram (Subp)
+ then
+ Error_Msg_N ("incompatible overriding in effect", Subp);
- if Is_Ignored_Ghost_Entity (Subp) then
+ Error_Msg_Sloc := Sloc (Over_Subp);
+ Error_Msg_N ("\& declared # as ghost subprogram", Subp);
- -- Both the parent subprogram and overriding subprogram are
- -- ignored Ghost.
+ Error_Msg_Sloc := Sloc (Subp);
+ Error_Msg_N ("\overridden # with non-ghost subprogram", Subp);
+ end if;
- if Is_Ignored_Ghost_Entity (Over_Subp) then
- null;
+ if Present (Deriv_Typ)
+ and then not Is_Ignored_Ghost_Entity (Deriv_Typ)
+ then
+ -- When a tagged type is either non-Ghost or checked Ghost and
+ -- one of its primitives overrides an inherited operation, the
+ -- overridden operation of the ancestor type must be ignored Ghost
+ -- if the primitive is ignored Ghost (SPARK RM 6.9(19)).
- -- The parent subprogram carries policy Check
+ if Is_Ignored_Ghost_Entity (Subp) then
- elsif Is_Checked_Ghost_Entity (Over_Subp) then
- Error_Msg_N
- ("incompatible ghost policies in effect", Subp);
+ -- Both the parent subprogram and overriding subprogram are
+ -- ignored Ghost.
- Error_Msg_Sloc := Sloc (Over_Subp);
- Error_Msg_N
- ("\& declared # with ghost policy `Check`", Subp);
+ if Is_Ignored_Ghost_Entity (Over_Subp) then
+ null;
- Error_Msg_Sloc := Sloc (Subp);
- Error_Msg_N
- ("\overridden # with ghost policy `Ignore`", Subp);
+ -- The parent subprogram carries policy Check
- -- The parent subprogram is non-Ghost
+ elsif Is_Checked_Ghost_Entity (Over_Subp) then
+ Error_Msg_N (Ghost_Policy_Error_Msg, Subp);
- else
- Error_Msg_N
- ("incompatible ghost policies in effect", Subp);
+ Error_Msg_Sloc := Sloc (Over_Subp);
+ Error_Msg_N
+ ("\& declared # with ghost policy `Check`", Subp);
- Error_Msg_Sloc := Sloc (Over_Subp);
- Error_Msg_N ("\& declared # as non-ghost subprogram", Subp);
+ Error_Msg_Sloc := Sloc (Subp);
+ Error_Msg_N
+ ("\overridden # with ghost policy `Ignore`", Subp);
- Error_Msg_Sloc := Sloc (Subp);
- Error_Msg_N
- ("\overridden # with ghost policy `Ignore`", Subp);
- end if;
+ -- The parent subprogram is non-Ghost
- -- When a tagged type is either non-Ghost or checked Ghost and
- -- one of its primitives overrides an inherited operation, the
- -- the primitive of the tagged type must be ignored Ghost if the
- -- overridden operation is ignored Ghost (SPARK RM 6.9(19)).
+ else
+ Error_Msg_N (Ghost_Policy_Error_Msg, Subp);
- elsif Is_Ignored_Ghost_Entity (Over_Subp) then
+ Error_Msg_Sloc := Sloc (Over_Subp);
+ Error_Msg_N ("\& declared # as non-ghost subprogram", Subp);
- -- Both the parent subprogram and the overriding subprogram are
- -- ignored Ghost.
+ Error_Msg_Sloc := Sloc (Subp);
+ Error_Msg_N
+ ("\overridden # with ghost policy `Ignore`", Subp);
+ end if;
- if Is_Ignored_Ghost_Entity (Subp) then
- null;
+ -- When a tagged type is either non-Ghost or checked Ghost and
+ -- one of its primitives overrides an inherited operation, the
+ -- the primitive of the tagged type must be ignored Ghost if the
+ -- overridden operation is ignored Ghost (SPARK RM 6.9(19)).
- -- The overriding subprogram carries policy Check
+ elsif Is_Ignored_Ghost_Entity (Over_Subp) then
- elsif Is_Checked_Ghost_Entity (Subp) then
- Error_Msg_N
- ("incompatible ghost policies in effect", Subp);
+ -- Both the parent subprogram and the overriding subprogram are
+ -- ignored Ghost.
- Error_Msg_Sloc := Sloc (Over_Subp);
- Error_Msg_N
- ("\& declared # with ghost policy `Ignore`", Subp);
+ if Is_Ignored_Ghost_Entity (Subp) then
+ null;
- Error_Msg_Sloc := Sloc (Subp);
- Error_Msg_N
- ("\overridden # with Ghost policy `Check`", Subp);
+ -- The overriding subprogram carries policy Check
- -- The overriding subprogram is non-Ghost
+ elsif Is_Checked_Ghost_Entity (Subp) then
+ Error_Msg_N (Ghost_Policy_Error_Msg, Subp);
- else
- Error_Msg_N
- ("incompatible ghost policies in effect", Subp);
+ Error_Msg_Sloc := Sloc (Over_Subp);
+ Error_Msg_N
+ ("\& declared # with ghost policy `Ignore`", Subp);
- Error_Msg_Sloc := Sloc (Over_Subp);
- Error_Msg_N
- ("\& declared # with ghost policy `Ignore`", Subp);
+ Error_Msg_Sloc := Sloc (Subp);
+ Error_Msg_N
+ ("\overridden # with Ghost policy `Check`", Subp);
- Error_Msg_Sloc := Sloc (Subp);
- Error_Msg_N
- ("\overridden # with non-ghost subprogram", Subp);
- end if;
+ -- The overriding subprogram is non-Ghost
+
+ else
+ Error_Msg_N (Ghost_Policy_Error_Msg, Subp);
+
+ Error_Msg_Sloc := Sloc (Over_Subp);
+ Error_Msg_N
+ ("\& declared # with ghost policy `Ignore`", Subp);
+
+ Error_Msg_Sloc := Sloc (Subp);
+ Error_Msg_N
+ ("\overridden # with non-ghost subprogram", Subp);
end if;
end if;
end if;
---------------------------
procedure Check_Ghost_Primitive (Prim : Entity_Id; Typ : Entity_Id) is
+ Prim_Level : Entity_Id;
+ Typ_Level : Entity_Id;
begin
- -- The Ghost policy in effect at the point of declaration of a primitive
- -- operation and a tagged type must match (SPARK RM 6.9(18)).
+ if not Is_Tagged_Type (Typ) then
+ return;
+ end if;
- if Is_Tagged_Type (Typ) then
- if Is_Checked_Ghost_Entity (Prim)
- and then Is_Ignored_Ghost_Entity (Typ)
- then
- Error_Msg_N ("incompatible ghost policies in effect", Prim);
+ -- The Ghost policy in effect at the point of declaration of a primitive
+ -- operation and a tagged type must match (SPARK RM 6.9(20)).
- Error_Msg_Sloc := Sloc (Typ);
- Error_Msg_NE
- ("\tagged type & declared # with ghost policy `Ignore`",
- Prim, Typ);
+ if Is_Checked_Ghost_Entity (Prim)
+ and then Is_Ignored_Ghost_Entity (Typ)
+ then
+ Error_Msg_N (Ghost_Policy_Error_Msg, Prim);
- Error_Msg_Sloc := Sloc (Prim);
- Error_Msg_N
- ("\primitive subprogram & declared # with ghost policy `Check`",
- Prim);
+ Error_Msg_Sloc := Sloc (Typ);
+ Error_Msg_NE
+ ("\tagged type & declared # with ghost policy `Ignore`",
+ Prim, Typ);
- elsif Is_Ignored_Ghost_Entity (Prim)
- and then Is_Checked_Ghost_Entity (Typ)
- then
- Error_Msg_N ("incompatible ghost policies in effect", Prim);
+ Error_Msg_Sloc := Sloc (Prim);
+ Error_Msg_N
+ ("\primitive subprogram & declared # with ghost policy `Check`",
+ Prim);
+ end if;
- Error_Msg_Sloc := Sloc (Typ);
- Error_Msg_NE
- ("\tagged type & declared # with ghost policy `Check`",
- Prim, Typ);
+ Prim_Level := Ghost_Assertion_Level (Prim);
+ Typ_Level := Ghost_Assertion_Level (Typ);
+
+ if not Is_Assertion_Level_Dependent (Prim_Level, Typ_Level) then
+ Error_Msg_N (Assertion_Level_Error_Msg, Prim);
+ Error_Msg_Name_1 := Chars (Typ_Level);
+ Error_Msg_Sloc := Sloc (Typ);
+ Error_Msg_NE ("\tagged type & declared # with %", Prim, Typ);
+ Error_Msg_Name_1 := Chars (Prim_Level);
+ Error_Msg_Sloc := Sloc (Prim);
+ Error_Msg_NE
+ ("\primitive subprogram & declared # with %", Prim, Prim);
+ Error_Msg_Name_1 := Chars (Typ_Level);
+ Error_Msg_NE
+ ("\assertion level of & should depend on %", Prim, Prim);
- Error_Msg_Sloc := Sloc (Prim);
- Error_Msg_N
- ("\primitive subprogram & declared # with ghost policy `Ignore`",
- Prim);
- end if;
end if;
end Check_Ghost_Primitive;
Constit : Node_Id;
Constit_Id : Entity_Id)
is
+ State_Level : Entity_Id;
+ Constit_Level : Entity_Id;
begin
- if Is_Ghost_Entity (State_Id) then
- if Is_Ghost_Entity (Constit_Id) then
+ -- Only check ghost states
- -- The Ghost policy in effect at the point of abstract state
- -- declaration and constituent must match (SPARK RM 6.9(17)).
+ if not Is_Ghost_Entity (State_Id) then
+ return;
+ end if;
- if Is_Checked_Ghost_Entity (State_Id)
- and then Is_Ignored_Ghost_Entity (Constit_Id)
- then
- Error_Msg_Sloc := Sloc (Constit);
- SPARK_Msg_N ("incompatible ghost policies in effect", State);
-
- SPARK_Msg_NE
- ("\abstract state & declared with ghost policy `Check`",
- State, State_Id);
- SPARK_Msg_NE
- ("\constituent & declared # with ghost policy `Ignore`",
- State, Constit_Id);
-
- elsif Is_Ignored_Ghost_Entity (State_Id)
- and then Is_Checked_Ghost_Entity (Constit_Id)
- then
- Error_Msg_Sloc := Sloc (Constit);
- SPARK_Msg_N ("incompatible ghost policies in effect", State);
-
- SPARK_Msg_NE
- ("\abstract state & declared with ghost policy `Ignore`",
- State, State_Id);
- SPARK_Msg_NE
- ("\constituent & declared # with ghost policy `Check`",
- State, Constit_Id);
- end if;
+ -- A constituent of a Ghost abstract state must be a Ghost entity
+ -- (SPARK RM 7.2.2(12)).
+
+ if not Is_Ghost_Entity (Constit_Id) then
+ SPARK_Msg_NE
+ ("constituent of ghost state & must be ghost",
+ Constit, State_Id);
+ end if;
- -- A constituent of a Ghost abstract state must be a Ghost entity
- -- (SPARK RM 7.2.2(12)).
+ -- The Ghost policy in effect at the point of an ignored abstract state
+ -- cannot be check (SPARK RM 6.9(19)).
+
+ if Is_Ignored_Ghost_Entity (State_Id)
+ and then Is_Checked_Ghost_Entity (Constit_Id)
+ then
+ SPARK_Msg_N (Ghost_Policy_Error_Msg, State);
+ Error_Msg_Sloc := Sloc (State_Id);
+ SPARK_Msg_NE
+ ("\abstract state & declared # with ghost policy `Ignore`",
+ State, State_Id);
+ Error_Msg_Sloc := Sloc (Constit_Id);
+ SPARK_Msg_NE
+ ("\constituent & declared # with ghost policy `Check`",
+ State, Constit_Id);
+ end if;
+
+ State_Level := Ghost_Assertion_Level (State_Id);
+ Constit_Level := Ghost_Assertion_Level (Constit_Id);
+
+ if not Is_Assertion_Level_Dependent (Constit_Level, State_Level) then
+ SPARK_Msg_N (Assertion_Level_Error_Msg, State);
+ Error_Msg_Name_1 := Chars (State_Level);
+ Error_Msg_Sloc := Sloc (State_Id);
+ SPARK_Msg_NE ("\abstract state & declared # with %", State, State_Id);
+ Error_Msg_Name_1 := Chars (Constit_Level);
+ Error_Msg_Sloc := Sloc (Constit_Id);
+ SPARK_Msg_NE ("\constituent & declared # with %", State, Constit_Id);
+ Error_Msg_Name_1 := Chars (State_Level);
+ SPARK_Msg_NE
+ ("\assertion level of & should depend on %", State, Constit_Id);
- else
- SPARK_Msg_NE
- ("constituent of ghost state & must be ghost",
- Constit, State_Id);
- end if;
end if;
end Check_Ghost_Refinement;
end if;
end Check_Ghost_Type;
+ ----------------------
+ -- Get_Ghost_Aspect --
+ ----------------------
+
+ function Get_Ghost_Aspect (N : Node_Id) return Node_Id is
+ Asp : Node_Id;
+ begin
+ if not Permits_Aspect_Specifications (N) then
+ return Empty;
+ end if;
+
+ Asp := First (Aspect_Specifications (N));
+ while Present (Asp) loop
+ if Chars (Identifier (Asp)) = Name_Ghost then
+ return Asp;
+ end if;
+
+ Next (Asp);
+ end loop;
+
+ return Empty;
+ end Get_Ghost_Aspect;
+
+ ----------------------
+ -- Get_Ghost_Pragma --
+ ----------------------
+
+ function Get_Ghost_Pragma (N : Node_Id) return Node_Id is
+ Decl : Node_Id := Empty;
+ begin
+ -- When the context is a [generic] package declaration, pragma Ghost
+ -- resides in the visible declarations.
+
+ if Nkind (N) in N_Generic_Package_Declaration | N_Package_Declaration
+ then
+ Decl := First (Visible_Declarations (Specification (N)));
+
+ -- When the context is a package or a subprogram body, pragma Ghost
+ -- resides in the declarative part.
+
+ elsif Nkind (N) in N_Package_Body | N_Subprogram_Body then
+ Decl := First (Declarations (N));
+
+ -- Otherwise pragma Ghost appears in the declarations following N
+
+ elsif Is_List_Member (N) then
+ Decl := Next (N);
+ end if;
+
+ while Present (Decl) loop
+ if Nkind (Decl) = N_Pragma
+ and then Pragma_Name (Decl) = Name_Ghost
+ then
+ return Decl;
+
+ -- A source construct ends the region where pragma Ghost may appear,
+ -- stop the traversal. Check the original node as source constructs
+ -- may be rewritten into something else by expansion.
+
+ elsif Comes_From_Source (Original_Node (Decl)) then
+ exit;
+ end if;
+
+ Next (Decl);
+ end loop;
+
+ return Empty;
+ end Get_Ghost_Pragma;
+
+ -------------------------------
+ -- Get_Ghost_Assertion_Level --
+ -------------------------------
+
+ function Get_Ghost_Assertion_Level (N : Node_Id) return Entity_Id is
+ Ghost_Asp : constant Node_Id := Get_Ghost_Aspect (N);
+ Ghost_Prag : Node_Id;
+
+ begin
+ if Present (Ghost_Asp) then
+ return Assertion_Level_From_Arg (Expression (Ghost_Asp));
+ end if;
+
+ Ghost_Prag := Get_Ghost_Pragma (N);
+ if Present (Ghost_Prag) then
+ return
+ Assertion_Level_From_Arg
+ (First (Pragma_Argument_Associations (Ghost_Prag)));
+ end if;
+
+ return Empty;
+ end Get_Ghost_Assertion_Level;
+
+ ----------------------------
+ -- Ghost_Policy_In_Effect --
+ ----------------------------
+
+ function Ghost_Policy_In_Effect (Id : Entity_Id) return Name_Id is
+ Level : constant Entity_Id := Ghost_Assertion_Level (Id);
+ Level_Nam : constant Name_Id :=
+ (if No (Level) then No_Name else Chars (Level));
+ begin
+ return Policy_In_Effect (Name_Ghost, Level_Nam);
+ end Ghost_Policy_In_Effect;
+
--------------------------------
-- Implements_Ghost_Interface --
--------------------------------
Set_Ignored_Ghost_Recording_Proc (Record_Ignored_Ghost_Node'Access);
end Initialize;
- ------------------------
- -- Install_Ghost_Mode --
- ------------------------
-
- procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type) is
- begin
- Install_Ghost_Region (Mode, Empty);
- end Install_Ghost_Mode;
-
--------------------------
-- Install_Ghost_Region --
--------------------------
- procedure Install_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id) is
+ procedure Install_Ghost_Region
+ (Mode : Ghost_Mode_Type;
+ N : Node_Id;
+ Level : Entity_Id)
+ is
begin
-- The context is already within an ignored Ghost region. Maintain the
-- start of the outermost ignored Ghost region.
Ghost_Config.Ignored_Ghost_Region := Empty;
end if;
+ Ghost_Config.Current_Region := N;
Ghost_Config.Ghost_Mode := Mode;
+ Ghost_Config.Ghost_Mode_Assertion_Level := Level;
end Install_Ghost_Region;
- procedure Install_Ghost_Region (Mode : Name_Id; N : Node_Id) is
+ procedure Install_Ghost_Region
+ (Mode : Name_Id;
+ N : Node_Id;
+ Level : Entity_Id) is
begin
- Install_Ghost_Region (Name_To_Ghost_Mode (Mode), N);
+ Install_Ghost_Region (Name_To_Ghost_Mode (Mode), N, Level);
end Install_Ghost_Region;
+ -------------------------
+ -- Is_Compatible_Level --
+ -------------------------
+
+ function Is_Assertion_Level_Dependent
+ (Self : Entity_Id; Other : Entity_Id) return Boolean
+ is
+ begin
+ return
+ Self = Standard_Level_Default
+ or else Other = Standard_Level_Default
+ or else Is_Same_Or_Depends_On_Level (Self, Other)
+ or else Is_Same_Or_Depends_On_Level (Self, Standard_Level_Static);
+ end Is_Assertion_Level_Dependent;
+
-------------------------
-- Is_Ghost_Assignment --
-------------------------
-----------------------
function Enables_Ghostness (Arg : Node_Id) return Boolean is
- Expr : Node_Id;
+ Expr : constant Node_Id := Get_Pragma_Arg (Arg);
begin
- Expr := Arg;
+ -- Aspect Ghost without an expression enables ghostness
- if Nkind (Expr) = N_Pragma_Argument_Association then
- Expr := Get_Pragma_Arg (Expr);
+ if No (Expr) then
+ return True;
end if;
- -- Determine whether the expression of the aspect or pragma is static
- -- and denotes True.
+ -- Check if the expression matches a static boolean expression first
- if Present (Expr) then
- Preanalyze_And_Resolve (Expr);
-
- return
- Is_OK_Static_Expression (Expr)
- and then Is_True (Expr_Value (Expr));
+ Preanalyze_And_Resolve_Without_Errors (Expr);
+ if Is_OK_Static_Expression (Expr) then
+ return Is_True (Expr_Value (Expr));
+ end if;
- -- Otherwise Ghost defaults to True
+ -- Alternatively the argument could be an Assertion_Level
- else
+ if Nkind (Expr) = N_Identifier
+ and then Present (Get_Assertion_Level (Chars (Expr)))
+ then
return True;
end if;
+
+ return False;
end Enables_Ghostness;
-- Local variables
Id : constant Entity_Id := Defining_Entity (N);
Asp : Node_Id;
- Decl : Node_Id;
+ Prag : Node_Id;
Prev_Id : Entity_Id;
-- Start of processing for Is_Subject_To_Ghost
-- Examine the aspect specifications (if any) looking for aspect Ghost
- if Permits_Aspect_Specifications (N) then
- Asp := First (Aspect_Specifications (N));
- while Present (Asp) loop
- if Chars (Identifier (Asp)) = Name_Ghost then
- return Enables_Ghostness (Expression (Asp));
- end if;
+ Asp := Get_Ghost_Aspect (N);
- Next (Asp);
- end loop;
+ if Present (Asp) then
+ return Enables_Ghostness (Expression (Asp));
end if;
- Decl := Empty;
-
- -- When the context is a [generic] package declaration, pragma Ghost
- -- resides in the visible declarations.
-
- if Nkind (N) in N_Generic_Package_Declaration | N_Package_Declaration
- then
- Decl := First (Visible_Declarations (Specification (N)));
-
- -- When the context is a package or a subprogram body, pragma Ghost
- -- resides in the declarative part.
-
- elsif Nkind (N) in N_Package_Body | N_Subprogram_Body then
- Decl := First (Declarations (N));
+ -- Examine the following pragmas for an applicable Ghost pragma
- -- Otherwise pragma Ghost appears in the declarations following N
+ Prag := Get_Ghost_Pragma (N);
- elsif Is_List_Member (N) then
- Decl := Next (N);
+ if Present (Prag) then
+ return
+ Enables_Ghostness (First (Pragma_Argument_Associations (Prag)));
end if;
- while Present (Decl) loop
- if Nkind (Decl) = N_Pragma
- and then Pragma_Name (Decl) = Name_Ghost
- then
- return
- Enables_Ghostness (First (Pragma_Argument_Associations (Decl)));
-
- -- A source construct ends the region where pragma Ghost may appear,
- -- stop the traversal. Check the original node as source constructs
- -- may be rewritten into something else by expansion.
-
- elsif Comes_From_Source (Original_Node (Decl)) then
- exit;
- end if;
-
- Next (Decl);
- end loop;
-
return False;
end Is_Subject_To_Ghost;
-- where P is a package, X is a record, and Comp is an array, we need
-- to check the ghost flags of X.
- Orig_Lhs : constant Node_Id := Name (N);
+ Orig_Lhs : constant Node_Id := Name (N);
+ Id : Entity_Id;
+ Lhs : Node_Id;
+
begin
-- Ghost assignments are irrelevant when the expander is inactive, and
-- processing them in that mode can lead to spurious errors.
- if Expander_Active then
- -- Cases where full analysis is needed, involving array indexing
- -- which would otherwise be missing array-bounds checks:
-
- if not Analyzed (Orig_Lhs)
- and then
- ((Nkind (Orig_Lhs) = N_Indexed_Component
- and then Nkind (Prefix (Orig_Lhs)) = N_Selected_Component
- and then Nkind (Prefix (Prefix (Orig_Lhs))) =
- N_Indexed_Component)
- or else
- (Nkind (Orig_Lhs) = N_Selected_Component
- and then Nkind (Prefix (Orig_Lhs)) = N_Indexed_Component
- and then Nkind (Prefix (Prefix (Orig_Lhs))) =
- N_Selected_Component
- and then Nkind (Parent (N)) /= N_Loop_Statement))
- then
- Analyze (Orig_Lhs);
- end if;
-
- -- Make sure Lhs is at least preanalyzed, so we can tell whether
- -- it denotes a ghost variable. In some cases we need to do a full
- -- analysis, or else the back end gets confused. Note that in the
- -- preanalysis case, we are preanalyzing a copy of the left-hand
- -- side name, temporarily attached to the tree.
-
- declare
- Lhs : constant Node_Id :=
- (if Analyzed (Orig_Lhs) then Orig_Lhs
- else New_Copy_Tree (Orig_Lhs));
- begin
- if not Analyzed (Lhs) then
- Set_Name (N, Lhs);
- Set_Parent (Lhs, N);
- Preanalyze_Without_Errors (Lhs);
- Set_Name (N, Orig_Lhs);
- end if;
-
- declare
- Id : constant Entity_Id := Get_Enclosing_Ghost_Entity (Lhs);
- begin
- if Present (Id) then
- -- Left-hand side denotes a Checked ghost entity, so install
- -- the region.
+ if not Expander_Active then
+ return;
+ end if;
- if Is_Checked_Ghost_Entity (Id) then
- Install_Ghost_Region (Check, N);
+ -- Cases where full analysis is needed, involving array indexing
+ -- which would otherwise be missing array-bounds checks:
- -- Left-hand side denotes an Ignored ghost entity, so
- -- install the region, and mark the assignment statement as
- -- an ignored ghost assignment, so it will be removed later.
+ if not Analyzed (Orig_Lhs)
+ and then
+ ((Nkind (Orig_Lhs) = N_Indexed_Component
+ and then Nkind (Prefix (Orig_Lhs)) = N_Selected_Component
+ and then Nkind (Prefix (Prefix (Orig_Lhs))) =
+ N_Indexed_Component)
+ or else
+ (Nkind (Orig_Lhs) = N_Selected_Component
+ and then Nkind (Prefix (Orig_Lhs)) = N_Indexed_Component
+ and then Nkind (Prefix (Prefix (Orig_Lhs))) =
+ N_Selected_Component
+ and then Nkind (Parent (N)) /= N_Loop_Statement))
+ then
+ Analyze (Orig_Lhs);
+ end if;
- elsif Is_Ignored_Ghost_Entity (Id) then
- Install_Ghost_Region (Ignore, N);
- Set_Is_Ignored_Ghost_Node (N);
- Record_Ignored_Ghost_Node (N);
- end if;
- end if;
- end;
- end;
+ -- Make sure Lhs is at least preanalyzed, so we can tell whether
+ -- it denotes a ghost variable. In some cases we need to do a full
+ -- analysis, or else the back end gets confused. Note that in the
+ -- preanalysis case, we are preanalyzing a copy of the left-hand
+ -- side name, temporarily attached to the tree.
+
+ Lhs :=
+ (if Analyzed (Orig_Lhs) then Orig_Lhs else New_Copy_Tree (Orig_Lhs));
+ if not Analyzed (Lhs) then
+ Set_Name (N, Lhs);
+ Set_Parent (Lhs, N);
+ Preanalyze_Without_Errors (Lhs);
+ Set_Name (N, Orig_Lhs);
end if;
+
+ Id := Get_Enclosing_Ghost_Entity (Lhs);
+ Mark_And_Set_Ghost_Region (N, Id);
end Mark_And_Set_Ghost_Assignment;
-----------------------------
Spec_Id : Entity_Id)
is
Body_Id : constant Entity_Id := Defining_Entity (N);
+ Level : Entity_Id := Empty;
Policy : Name_Id := No_Name;
begin
-- A body becomes Ghost when it is subject to aspect or pragma Ghost
if Is_Subject_To_Ghost (N) then
- Policy := Policy_In_Effect (Name_Ghost);
+ if Present (Spec_Id) then
+ Policy := Ghost_Policy_In_Effect (Spec_Id);
+ Level := Ghost_Assertion_Level (Spec_Id);
+ else
+ Policy := Ghost_Policy_In_Effect (Body_Id);
+ Level := Ghost_Assertion_Level (Body_Id);
+ end if;
-- A body declared within a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
elsif Ghost_Config.Ghost_Mode = Check then
Policy := Name_Check;
+ Level := Ghost_Config.Ghost_Mode_Assertion_Level;
elsif Ghost_Config.Ghost_Mode = Ignore then
Policy := Name_Ignore;
+ Level := Ghost_Config.Ghost_Mode_Assertion_Level;
-- Inherit the "ghostness" of the previous declaration when the body
-- acts as a completion.
elsif Is_Ignored_Ghost_Entity (Spec_Id) then
Policy := Name_Ignore;
end if;
+
+ Level := Ghost_Assertion_Level (Spec_Id);
end if;
-- The Ghost policy in effect at the point of declaration and at the
(Prev_Id => Spec_Id,
Compl_Id => Body_Id);
+ if Present (Level) then
+ Set_Ghost_Assertion_Level (Body_Id, Level);
+ end if;
+
-- Mark the body as its formals as Ghost
- Mark_Ghost_Declaration_Or_Body (N, Policy);
+ Mark_Ghost_Declaration_Or_Body (N, Policy, Level);
-- Install the appropriate Ghost region
- Install_Ghost_Region (Policy, N);
+ Install_Ghost_Region (Policy, N, Level);
end Mark_And_Set_Ghost_Body;
-----------------------------------
Prev_Id : Entity_Id)
is
Compl_Id : constant Entity_Id := Defining_Entity (N);
+ Level : Entity_Id := Empty;
Policy : Name_Id := No_Name;
begin
if Ghost_Config.Ghost_Mode = Check then
Policy := Name_Check;
+ Level := Ghost_Config.Ghost_Mode_Assertion_Level;
elsif Ghost_Config.Ghost_Mode = Ignore then
Policy := Name_Ignore;
+ Level := Ghost_Config.Ghost_Mode_Assertion_Level;
-- The completion becomes Ghost when its initial declaration is also
-- Ghost.
elsif Is_Checked_Ghost_Entity (Prev_Id) then
Policy := Name_Check;
+ Level := Ghost_Assertion_Level (Prev_Id);
elsif Is_Ignored_Ghost_Entity (Prev_Id) then
Policy := Name_Ignore;
+ Level := Ghost_Assertion_Level (Prev_Id);
end if;
-- The Ghost policy in effect at the point of declaration and at the
-- Mark the completion as Ghost
- Mark_Ghost_Declaration_Or_Body (N, Policy);
+ Mark_Ghost_Declaration_Or_Body (N, Policy, Level);
-- Install the appropriate Ghost region
- Install_Ghost_Region (Policy, N);
+ Install_Ghost_Region (Policy, N, Level);
end Mark_And_Set_Ghost_Completion;
------------------------------------
------------------------------------
procedure Mark_And_Set_Ghost_Declaration (N : Node_Id) is
+ Level : Entity_Id := Empty;
Par_Id : Entity_Id;
Policy : Name_Id := No_Name;
+ Id : Entity_Id;
begin
-- A declaration becomes Ghost when it is subject to aspect or pragma
-- Ghost.
if Is_Subject_To_Ghost (N) then
- Policy := Policy_In_Effect (Name_Ghost);
+ Id := Defining_Entity (N);
+
+ if Is_Ghost_Entity (Id) then
+ if Is_Checked_Ghost_Entity (Id) then
+ Policy := Name_Check;
+
+ elsif Is_Ignored_Ghost_Entity (Id) then
+ Policy := Name_Ignore;
+ end if;
+
+ Level := Ghost_Assertion_Level (Id);
+
+ else
+ -- We need to mark the declaration before the analysis so we
+ -- cannot rely on the Id already having the correct ghost markers.
+ -- Analyze if the node is associated with a ghost aspect here and
+ -- check for the applicable policy.
+
+ Level := Get_Ghost_Assertion_Level (N);
+ Policy :=
+ Policy_In_Effect (Name_Ghost, Assertion_Level_To_Name (Level));
+ end if;
-- A declaration elaborated in a Ghost region is automatically Ghost
-- (SPARK RM 6.9(2)).
elsif Ghost_Config.Ghost_Mode = Check then
Policy := Name_Check;
+ Level := Ghost_Config.Ghost_Mode_Assertion_Level;
elsif Ghost_Config.Ghost_Mode = Ignore then
Policy := Name_Ignore;
+ Level := Ghost_Config.Ghost_Mode_Assertion_Level;
-- A child package or subprogram declaration becomes Ghost when its
-- parent is Ghost (SPARK RM 6.9(2)).
elsif Is_Ignored_Ghost_Entity (Par_Id) then
Policy := Name_Ignore;
end if;
+
+ Level := Ghost_Assertion_Level (Par_Id);
end if;
-- Mark the declaration and its formals as Ghost
- Mark_Ghost_Declaration_Or_Body (N, Policy);
+ Mark_Ghost_Declaration_Or_Body (N, Policy, Level);
+
+ Check_Valid_Ghost_Declaration (N);
-- Install the appropriate Ghost region
- Install_Ghost_Region (Policy, N);
+ Install_Ghost_Region (Policy, N, Level);
end Mark_And_Set_Ghost_Declaration;
--------------------------------------
-- Local variables
+ Level : Entity_Id := Empty;
Policy : Name_Id := No_Name;
begin
-- An instantiation becomes Ghost when it is subject to pragma Ghost
if Is_Subject_To_Ghost (N) then
- Policy := Policy_In_Effect (Name_Ghost);
+ Policy := Ghost_Policy_In_Effect (Gen_Id);
-- An instantiation declaration within a Ghost region is automatically
-- Ghost (SPARK RM 6.9(2)).
elsif Ghost_Config.Ghost_Mode = Check then
Policy := Name_Check;
+ Level := Ghost_Config.Ghost_Mode_Assertion_Level;
elsif Ghost_Config.Ghost_Mode = Ignore then
Policy := Name_Ignore;
+ Level := Ghost_Config.Ghost_Mode_Assertion_Level;
-- Inherit the "ghostness" of the generic unit, but the current Ghost
-- policy is the relevant one for the instantiation.
elsif Is_Checked_Ghost_Entity (Gen_Id)
or else Is_Ignored_Ghost_Entity (Gen_Id)
then
- Policy := Policy_In_Effect (Name_Ghost);
+ Policy := Ghost_Policy_In_Effect (Gen_Id);
if Policy = No_Name then
Policy := Name_Ignore;
end if;
+
+ Level := Ghost_Assertion_Level (Gen_Id);
end if;
-- Mark the instantiation as Ghost
- Mark_Ghost_Declaration_Or_Body (N, Policy);
+ Mark_Ghost_Declaration_Or_Body (N, Policy, Level);
-- Install the appropriate Ghost region
- Install_Ghost_Region (Policy, N);
+ Install_Ghost_Region (Policy, N, Level);
-- Check Ghost actuals. Given that this routine is unconditionally
-- invoked with subprogram and package instantiations, this check
procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id) is
Id : Entity_Id;
-
begin
-- A procedure call becomes Ghost when the procedure being invoked is
-- Ghost. Install the Ghost mode of the procedure.
Id := Get_Enclosing_Ghost_Entity (Name (N));
- if Present (Id) then
- if Is_Checked_Ghost_Entity (Id) then
- Install_Ghost_Region (Check, N);
+ Mark_And_Set_Ghost_Region (N, Id);
+ end Mark_And_Set_Ghost_Procedure_Call;
- elsif Is_Ignored_Ghost_Entity (Id) then
- Install_Ghost_Region (Ignore, N);
+ -------------------------------
+ -- Mark_And_Set_Ghost_Region --
+ -------------------------------
- Set_Is_Ignored_Ghost_Node (N);
- Record_Ignored_Ghost_Node (N);
- end if;
+ procedure Mark_And_Set_Ghost_Region (N : Node_Id; Id : Entity_Id) is
+ Id_Policy : Name_Id;
+ begin
+ -- Nothing to do if we are not dealing with a ghost entity
+
+ if No (Id) or else not Is_Ghost_Entity (Id) then
+ return;
end if;
- end Mark_And_Set_Ghost_Procedure_Call;
+
+ Id_Policy := Ghost_Policy_In_Effect (Id);
+
+ if Id_Policy = Name_Check then
+ Install_Ghost_Region (Check, N, Ghost_Assertion_Level (Id));
+
+ elsif Id_Policy = Name_Ignore then
+ Install_Ghost_Region (Ignore, N, Ghost_Assertion_Level (Id));
+ Set_Is_Ignored_Ghost_Node (N);
+ Record_Ignored_Ghost_Node (N);
+ end if;
+ end Mark_And_Set_Ghost_Region;
-----------------------
-- Mark_Ghost_Clause --
------------------------------------
procedure Mark_Ghost_Declaration_Or_Body
- (N : Node_Id;
- Mode : Name_Id)
+ (N : Node_Id;
+ Mode : Name_Id;
+ Level : Entity_Id)
is
Id : constant Entity_Id := Defining_Entity (N);
Param_Id : Entity_Id;
begin
- -- Mark the related node and its entity
+ Set_Ghost_Assertion_Level (Id, Level);
if Mode = Name_Check then
Mark_Formals := True;
while Present (Param) loop
Param_Id := Defining_Entity (Param);
+ Set_Ghost_Assertion_Level (Param_Id, Level);
+
if Mode = Name_Check then
Set_Is_Checked_Ghost_Entity (Param_Id);
Id : Entity_Id)
is
Policy : Name_Id := No_Name;
-
+ Level : constant Entity_Id := Ghost_Assertion_Level (Id);
begin
-- A renaming becomes Ghost when it renames a Ghost entity
Policy := Name_Ignore;
end if;
- Mark_Ghost_Declaration_Or_Body (N, Policy);
+ Mark_Ghost_Declaration_Or_Body (N, Policy, Level);
end Mark_Ghost_Renaming;
------------------------
--------------------------------
procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is
+ Level : constant Entity_Id := Ghost_Assertion_Level (Id);
begin
if Is_Checked_Ghost_Entity (Id) then
- Install_Ghost_Mode (Check);
+ Install_Ghost_Region (Check, N, Level);
elsif Is_Ignored_Ghost_Entity (Id) then
- Install_Ghost_Mode (Ignore);
+ Install_Ghost_Region (Ignore, N, Level);
else
- Install_Ghost_Mode (None);
+ Install_Ghost_Region (None, N, Level);
end if;
end Set_Ghost_Mode_From_Entity;
-- Local variables
- Id : Entity_Id;
+ Id : Entity_Id;
+ Level : Entity_Id;
-- Start of processing for Set_Ghost_Mode
-- property is encoded in the pragma itself.
elsif Nkind (N) = N_Pragma then
+ Level := Pragma_Ghost_Assertion_Level (N);
if Is_Checked_Ghost_Pragma (N) then
- Install_Ghost_Mode (Check);
+ Install_Ghost_Region (Check, N, Level);
elsif Is_Ignored_Ghost_Pragma (N) then
- Install_Ghost_Mode (Ignore);
+ Install_Ghost_Region (Ignore, N, Level);
else
- Install_Ghost_Mode (None);
+ Install_Ghost_Region (None, N, Level);
end if;
-- The Ghost mode of a procedure call depends on the Ghost mode of the
-------------------------
procedure Set_Is_Ghost_Entity (Id : Entity_Id) is
- Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
+ Policy : constant Name_Id := Ghost_Policy_In_Effect (Id);
begin
if Policy = Name_Check then
Set_Is_Checked_Ghost_Entity (Id);
package Ghost is
+ function Assertion_Level_From_Arg (Arg : Node_Id) return Entity_Id;
+ -- Returns the assertion level for the given pragma or aspect based on
+ -- the argument Arg. Which is either
+ --
+ -- * Standard_Level_Default if there was no argument or the argument
+ -- evaluated to True.
+ -- * Assertion_Level if the argument was referencing a user defined
+ -- Assertion_Level.
+ -- * Empty othrwise since we are not dealing with a ghost entity.
+
procedure Check_Ghost_Completion
(Prev_Id : Entity_Id;
Compl_Id : Entity_Id);
Constit : Node_Id;
Constit_Id : Entity_Id);
-- Verify that the Ghost policy of constituent Constit_Id is compatible
- -- with the Ghost policy of abstract state State_I.
+ -- with the Ghost policy of abstract state State_Id.
+ --
+ -- Additionally verify that the Ghost_Assertion_Levels are compatible.
procedure Check_Ghost_Type (Typ : Entity_Id);
-- Verify that Ghost type Typ is neither concurrent, nor effectively
procedure Initialize;
-- Initialize internal tables
- procedure Install_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id);
+ procedure Install_Ghost_Region
+ (Mode : Ghost_Mode_Type;
+ N : Node_Id;
+ Level : Entity_Id);
pragma Inline (Install_Ghost_Region);
-- Install a Ghost region described by mode Mode and ignored region start
-- node N.
+ function Is_Assertion_Level_Dependent
+ (Self : Entity_Id; Other : Entity_Id) return Boolean;
+ -- Check that assertion level Self is assertion-level-dependent with Other.
+ --
+ -- According to SPARK RM 6.9(5) this means that
+ -- * Either Self or Other has the default assertion level.
+ -- * Self either is or depends on Other
+ -- * Self either is or depends on Static
+
function Is_Ghost_Assignment (N : Node_Id) return Boolean;
-- Determine whether arbitrary node N denotes an assignment statement whose
-- target is a Ghost entity.
E_Anonymous_Access_Type => ' ',
E_Array_Subtype => 'A',
E_Array_Type => 'A',
+ E_Assertion_Level => 'z',
E_Block => 'q',
E_Class_Wide_Subtype => 'C',
E_Class_Wide_Type => 'C',
-- w protected object protected type
-- x abstract procedure exception
-- y abstract function entry or entry family
- -- z generic formal parameter (unused)
+ -- z generic formal parameter assertion level
---------------------------------------------------
-- Handling of Imported and Exported Subprograms --
-- reflect the starting node of the outermost ignored Ghost region. If a
-- nested ignored Ghost region is entered, the value must remain
-- unchanged.
+
+ Ghost_Mode_Assertion_Level : Entity_Id := Empty;
+ -- The Assertion_Level that is applied to the current ghost region.
+ -- It is either:
+ -- * Empty - when there is no ghost region
+ -- * Assertion_Level - if the ghost aspect/pragama had an
+ -- Assertion_Levle associated with it.
+ -- * Standard_Default_Level - if the ghost aspect/pragama did not have
+ -- an Assertion_Level associated to it.
+
+ Current_Region : Node_Id := Empty;
+ -- Latest ghost region
end record;
Ghost_Config : Ghost_Config_Type;
| Pragma_Annotate
| Pragma_Assert
| Pragma_Assert_And_Cut
+ | Pragma_Assertion_Level
| Pragma_Assertion_Policy
| Pragma_Assume
| Pragma_Assume_No_Invalid_Values
-- Provide a clean environment for the unit
Ignore_SPARK_Mode_Pragmas_In_Instance := False;
- Install_Ghost_Region (None, Empty);
+ Install_Ghost_Region (None, Empty, Empty);
Install_SPARK_Mode (None, Empty);
-- Otherwise we need to load the unit, First build unit name from the
-- Set up a clean environment before analyzing
- Install_Ghost_Region (None, Empty);
+ Install_Ghost_Region (None, Empty, Empty);
Ignore_SPARK_Mode_Pragmas_In_Instance := False;
Outer_Generic_Scope := Empty;
-- expression is allowed. Includes checking that the expression
-- does not raise Constraint_Error.
+ procedure Convert_Aspect_With_Assertion_Levels (Aspect : Node_Id);
+ -- If an Aspect is using an association with an Assertion_Level
+ -- analyze the aspect with the level and convert it into an aspect
+ -- without the Assertion_Level. In the case the aspect has
+ -- associations with Assertion_Levels then multiple aspects are
+ -- created and each one will point to the original aspect that
+ -- they were created from in the Original_Aspect field.
+
function Directly_Specified
(Id : Entity_Id; A : Aspect_Id) return Boolean;
-- Returns True if the given aspect is directly (as opposed to
end case;
end Check_Expr_Is_OK_Static_Expression;
+ ------------------------------------------
+ -- Convert_Aspect_With_Assertion_Levels --
+ ------------------------------------------
+
+ procedure Convert_Aspect_With_Assertion_Levels (Aspect : Node_Id)
+ is
+ Assoc : Node_Id;
+ Assocs : List_Id;
+ Choice : Node_Id;
+ Level : Entity_Id;
+ Sub_Expr : Node_Id;
+ New_Aspect : Node_Id;
+ begin
+ Assocs := Component_Associations (Expression (Aspect));
+ Assoc := First (Assocs);
+
+ if Present (Expressions (Expression (Aspect))) then
+ Error_Msg_N
+ ("wrong syntax for argument of %", Expression (Aspect));
+ Error_Msg_N
+ ("\aspect with Assertion_Level can only contain "
+ & "contain Assertion_Level associations",
+ Expression (Aspect));
+ end if;
+
+ while Present (Assoc) loop
+ if List_Length (Choices (Assoc)) > 1 then
+ Error_Msg_Name_1 := Nam;
+ Error_Msg_N ("wrong syntax for argument of %", Assoc);
+ Error_Msg_N
+ ("\only one Assertion_Level can be associated "
+ & "with an expression",
+ Assoc);
+ end if;
+
+ Choice := First (Choices (Assoc));
+
+ if Nkind (Choice) /= N_Identifier then
+ Error_Msg_N ("wrong syntax for argument of %", Assoc);
+ Error_Msg_N
+ ("\association must denote an Assertion_Level", Assoc);
+ end if;
+
+ Level := Get_Assertion_Level (Chars (Choice));
+
+ Sub_Expr := Expression (Assoc);
+ New_Aspect :=
+ Make_Aspect_Specification
+ (Sloc => Sloc (Assoc),
+ Identifier => New_Copy_Tree (Id),
+ Expression => Sub_Expr);
+
+ Check_Applicable_Policy (New_Aspect, Level);
+
+ Set_Aspect_Ghost_Assertion_Level (New_Aspect, Level);
+
+ Insert_After (Aspect, New_Aspect);
+
+ -- Store the Original_Aspect for the detection of
+ -- duplicates.
+
+ Set_Original_Aspect (New_Aspect, Aspect);
+
+ Next (Assoc);
+ end loop;
+ end Convert_Aspect_With_Assertion_Levels;
+
------------------------
-- Directly_Specified --
------------------------
-- Set additional semantic fields
- if Is_Ignored (Aspect) then
- Set_Is_Ignored (Aitem);
- elsif Is_Checked (Aspect) then
- Set_Is_Checked (Aitem);
- end if;
+ Set_Is_Checked (Aitem, Is_Checked (Aspect));
+ Set_Is_Ignored (Aitem, Is_Ignored (Aspect));
+ Set_Pragma_Ghost_Assertion_Level
+ (Aitem, Aspect_Ghost_Assertion_Level (Aspect));
Set_Corresponding_Aspect (Aitem, Aspect);
Set_From_Aspect_Specification (Aitem);
-- as such for later reference in the tree. This also sets the
-- Is_Ignored and Is_Checked flags appropriately.
- Check_Applicable_Policy (Aspect);
+ if Is_Valid_Assertion_Kind (Nam) then
+ if Is_Checked (Aspect) or else Is_Ignored (Aspect) then
+ null;
+
+ -- If the Aspect has at least one Assertion_Level argument
+ -- then split the original Aspect into multiple aspects each
+ -- with an associated Assertion_Level.
+
+ elsif Has_Assertion_Level_Argument (Aspect) then
+ Convert_Aspect_With_Assertion_Levels (Aspect);
+ goto Continue;
+ else
+ Check_Applicable_Policy (Aspect);
+ end if;
+
+ end if;
if Is_Disabled (Aspect) then
goto Continue;
if No_Duplicates_Allowed (A_Id) then
Anod := First (L);
while Anod /= Aspect loop
- if Comes_From_Source (Aspect)
- and then Same_Aspect (A_Id, Get_Aspect_Id (Anod))
+
+ if (Comes_From_Source (Aspect)
+ or else (Original_Aspect (Aspect) /= Anod
+ and then not From_Same_Aspect (Aspect, Anod)))
+ and then Same_Aspect (A_Id, Get_Aspect_Id (Anod))
then
Error_Msg_Name_1 := Nam;
Error_Msg_Sloc := Sloc (Anod);
if Class_Present (Anod) = Class_Present (Aspect) then
if not Class_Present (Anod) then
Error_Msg_NE
- ("aspect% for & previously given#",
- Id, E);
+ ("aspect% for & previously given#", Id, E);
else
Error_Msg_NE
("aspect `%''Class` for & previously given#",
- Id, E);
+ Id,
+ E);
end if;
end if;
end if;
package body Sem_Prag is
+ ----------------------------------
+ -- Handling of Assertion Levels --
+ ----------------------------------
+
+ -- Assertion levels are special entities declared using pragma
+ -- Assertion_Level. Assertion levels can be used in most Assertion_Kind
+ -- pragmas to associate a given level with a given list of existing
+ -- arguments. E.g.
+ --
+ -- pragma Assert (Level1 => (Expr1, "Msg1"),
+ -- Level2 => (Expr2, "Msg2"));
+ --
+ -- Assertion levels can also be used in pragma Assertion_Policy and
+ -- Check_Policy as a valid policy name. E.g.
+ --
+ -- pragma Assertion_Policy (Level1 => Check);
+
+ --------------------------------
+ -- Declaring Assertion Levels --
+ --------------------------------
+
+ -- Assertion levels are declared using configuration level pragma
+ -- Assertion_Level. We create a new E_Assertion_Level entity for each
+ -- pragma and add each unique level to the Assertion_Levels table.
+ --
+ -- A pragma can be declared with dependencies. e.g.
+ --
+ -- pragma Assertion_Level (L1);
+ -- pragma Assertion_Level (L2, Depends => L1);
+ -- pragma Assertion_Level (L3, Depends => L2);
+ --
+ -- Levels that a level depends are called parent levels. Levels that depend
+ -- on a given level are called child levels. These dependencies are stored
+ -- in an E_Assertion_Level entity as attributes Parent_Levels and
+ -- Child_Levels.
+ --
+ -- When a pragma with the same level name is declared, we check that the
+ -- assertion level is declared with the same dependencies as the existing
+ -- level. Otherwise an error is raised.
+
+ package Assertion_Levels is new Table.Table (
+ Table_Component_Type => Entity_Id,
+ Table_Index_Type => Nat,
+ Table_Low_Bound => 1,
+ Table_Initial => 30,
+ Table_Increment => 200,
+ Table_Name => "Assertion_Levels");
+
+ -------------------------------------------
+ -- Applying Policies to Assertion Levels --
+ -------------------------------------------
+
+ -- When a policy is applied to an assertion level, all assertions
+ -- associated with that level are subjected to the same policy. Depending
+ -- on the policy value, the same policy is applied to its dependencies.
+ --
+ -- Consider the following assertion levels:
+ --
+ -- pragma Assertion_Level (L1);
+ -- pragma Assertion_Level (L2, Depends => L1);
+ -- pragma Assertion_Level (L3, Depends => L2);
+ --
+ -- When policy Check (or On) is applied to an assertion level, it is also
+ -- applied to all of its transitive parent levels. For example
+ --
+ -- pragma Assertion_Policy (L3 => Check);
+ --
+ -- applies policy Check to L2 and L1.
+ --
+ -- When policy Ignore (or Off) is applied to an assertion level, it is also
+ -- applied to all of its transitive child levels. For example
+ --
+ -- pragma Assertion_Policy (L1 => Ignore);
+ --
+ -- applies the policy Ignore for L2 and L3.
+ --
+ -- Note that assertion levels are not allowed to have the same name as any
+ -- other Assertion_Kind defined in the RM in order to avoid unintentional
+ -- name overloading.
+
+ --------------------------------------------------
+ -- Handling of Assertions with Assertion Levels --
+ --------------------------------------------------
+
+ -- Each Assertion pragma (see Is_Valid_Assertion) supports a new syntax
+ -- where the existing arguments can be associated with an assertion level.
+ --
+ -- Each association is converted into a new pragma with the same name but
+ -- without the level argument, and the old pragma is rewritten as N_Null.
+ -- An applicable policy for those pragmas is calculated by looking at the
+ -- first active Check_Policy that either matches the pragma name or the
+ -- name of the Assertion_Level. The following policy-based attributes are
+ -- set for the given pramga:
+ --
+ -- * Is_Checked - Based on the policy
+ -- * Is_Ignored - Based on the policy
+ -- * Is_Disabled - Based on the policy
+ -- * Pragma_Ghost_Assertion_Level - level associated with the assertion.
+ -- * Original_Pragma - reference to the original pragma that had the
+ -- Assertion_Levels.
+ --
+ -- For example, the following pragma:
+ --
+ -- pragma Assert (L1 => (Expr1, "Msg1"),
+ -- L2 => (Expr2, "Msg2"));
+ --
+ -- is rewritten as:
+ --
+ -- null; -- The original pragma
+ -- pragma Assert (Expr1, "Msg1");
+ -- pragma Assert (Expr2, "Msg2");
+ --
+ -- Each of the new pragmas is analyzed according to its existing semantic
+ -- rules.
+
----------------------------------------------
-- Common Handling of Import-Export Pragmas --
----------------------------------------------
-- Query whether a particular item appears in a mixed list of nodes and
-- entities. It is assumed that all nodes in the list have entities.
+ procedure Apply_Check_Policy (N : Node_Id; Policy : Name_Id);
+ -- Set the Is_Checked, Is_Ignored, Is_Disabled attributes on node N
+ -- based on the Policy. e.g.
+ --
+ -- * When Name_Ignore (or Name_Off) is used the node is marked as ignored.
+ -- * When Name_Check (or Name_On) is used the node is marked as checked.
+ -- * When Name_Disable is used the node is marked as disabled.
+
procedure Check_Postcondition_Use_In_Inlined_Subprogram
(Prag : Node_Id;
Spec_Id : Entity_Id);
-- set, the routine reports duplicate pragmas. The routine returns Empty
-- when reaching the start of the node chain.
+ function Get_Applicable_Policy
+ (Nam : Name_Id; Level : Entity_Id) return Name_Id;
+ -- Return the name of the Check_Policy applied to the name or the level
+ -- associated with the node.
+
function Get_Base_Subprogram (Def_Id : Entity_Id) return Entity_Id;
-- If Def_Id refers to a renamed subprogram, then the base subprogram (the
-- original one, following the renaming chain) is returned. Otherwise the
-- Determine whether dependency clause Clause is surrounded by extra
-- parentheses. If this is the case, issue an error message.
+ procedure Mark_Is_Checked (N : Node_Id);
+ -- Sets Is_Checked and unsets Is_Ignored
+
+ procedure Mark_Is_Disabled (N : Node_Id);
+ -- Sets Is_Disabled and Is_Ignored and unsets Is_Checked
+
+ procedure Mark_Is_Ignored (N : Node_Id);
+ -- Sets Is_Ignored and unsets Is_Checked
+
procedure Record_Possible_Body_Reference
(State_Id : Entity_Id;
Ref : Node_Id);
(Arg : Node_Id;
N1, N2 : Name_Id);
procedure Check_Arg_Is_One_Of
- (Arg : Node_Id;
- N1, N2, N3 : Name_Id);
- procedure Check_Arg_Is_One_Of
- (Arg : Node_Id;
- N1, N2, N3, N4 : Name_Id);
- procedure Check_Arg_Is_One_Of
- (Arg : Node_Id;
- N1, N2, N3, N4, N5 : Name_Id);
+ (Arg : Node_Id;
+ Names : Name_List);
-- Check the specified argument Arg to make sure that it is an
- -- identifier whose name matches either N1 or N2 (or N3, N4, N5 if
+ -- identifier whose name matches either N1 or N2 (or a list of names is
-- present). If not then give error and raise Pragma_Exit.
procedure Check_Arg_Is_Queuing_Policy (Arg : Node_Id);
-- presence of at least one component. UU_Typ is the related Unchecked_
-- Union type.
+ function Create_Pragma_Without_Assertion_Level
+ (Expr : Node_Id) return Node_Id;
+ -- Creates a new pragma from an Assertion_Level association argument
+ -- with the same name as the orignal pragma.
+
procedure Ensure_Aggregate_Form (Arg : Node_Id);
-- Subsidiary routine to the processing of pragmas Abstract_State,
-- Contract_Cases, Depends, Exceptional_Cases, Global, Initializes,
-- a class-wide precondition only if one of its ancestors has an
-- explicit class-wide precondition.
+ function Assertion_Level_Pragma_Comes_From_Source
+ (N : Node_Id) return Boolean
+ is (Present (Original_Pragma (N))
+ and then Present (Original_Node (Original_Pragma (N)))
+ and then Comes_From_Source (Original_Node (Original_Pragma (N))));
+ -- Determine whether a pragma was originally from source and used an
+ -- assertion level.
+ --
+ -- When the pragma was using an Assertion_Level it was replaced by
+ -- a new pragma where the Original_Pragma points to the original
+ -- pragma node which was removed from the tree and replaced by a
+ -- null node.
+
-----------------------------
-- Inherits_Class_Wide_Pre --
-----------------------------
-- rewriting the pragma identifier. This allows the retrieval of the
-- original pragma name by routine Original_Aspect_Pragma_Name.
- if Comes_From_Source (N) then
+ if Comes_From_Source (N)
+ or else Assertion_Level_Pragma_Comes_From_Source (N)
+ then
if Pname in Name_Pre | Name_Pre_Class then
Is_Pre_Post := True;
Set_Class_Present (N, Pname = Name_Pre_Class);
end Check_Arg_Is_One_Of;
procedure Check_Arg_Is_One_Of
- (Arg : Node_Id;
- N1, N2, N3 : Name_Id)
+ (Arg : Node_Id;
+ Names : Name_List)
is
Argx : constant Node_Id := Get_Pragma_Arg (Arg);
-
begin
Check_Arg_Is_Identifier (Argx);
- if Chars (Argx) not in N1 | N2 | N3 then
- Error_Pragma_Arg ("invalid argument for pragma%", Argx);
- end if;
- end Check_Arg_Is_One_Of;
-
- procedure Check_Arg_Is_One_Of
- (Arg : Node_Id;
- N1, N2, N3, N4 : Name_Id)
- is
- Argx : constant Node_Id := Get_Pragma_Arg (Arg);
-
- begin
- Check_Arg_Is_Identifier (Argx);
-
- if Chars (Argx) not in N1 | N2 | N3 | N4 then
- Error_Pragma_Arg ("invalid argument for pragma%", Argx);
+ if (for some Name of Names => Chars (Argx) = Name) then
+ return;
end if;
- end Check_Arg_Is_One_Of;
-
- procedure Check_Arg_Is_One_Of
- (Arg : Node_Id;
- N1, N2, N3, N4, N5 : Name_Id)
- is
- Argx : constant Node_Id := Get_Pragma_Arg (Arg);
- begin
- Check_Arg_Is_Identifier (Argx);
-
- if Chars (Argx) not in N1 | N2 | N3 | N4 | N5 then
- Error_Pragma_Arg ("invalid argument for pragma%", Argx);
- end if;
+ Error_Pragma_Arg ("invalid argument for pragma%", Argx);
end Check_Arg_Is_One_Of;
---------------------------------
end loop;
end Check_Variant;
+ -------------------------------------------
+ -- Create_Pragma_Without_Assertion_Level --
+ -------------------------------------------
+
+ function Create_Pragma_Without_Assertion_Level
+ (Expr : Node_Id) return Node_Id
+ is
+ function Aggregate_To_Associations (N : Node_Id) return List_Id;
+ -- Converts an Aggregate into a list of
+ -- Pragma_Argument_Associations.
+
+ procedure Validate_Assertion_Level_Aggregate (N : Node_Id);
+ -- Handle invalid syntax scenarios for an Aggregate containing
+ -- Assertion_Levels.
+
+ -------------------------------
+ -- Aggregate_To_Associations --
+ -------------------------------
+
+ function Aggregate_To_Associations (N : Node_Id) return List_Id is
+ Args : constant List_Id := New_List;
+ Comp_Assn : Node_Id;
+ Comp_Expr : Node_Id;
+ Comp_Expr_Repl : Node_Id;
+ Choice : Node_Id;
+ begin
+ pragma Assert (Nkind (N) = N_Aggregate);
+ Validate_Assertion_Level_Aggregate (N);
+
+ Comp_Expr := First (Expressions (N));
+ while Present (Comp_Expr) loop
+ -- Remove the expression from the list so that it can be
+ -- inserted into the new Pragma_Argument_Association.
+
+ Comp_Expr_Repl := Comp_Expr;
+ Next (Comp_Expr);
+ Remove (Comp_Expr_Repl);
+ Append_To
+ (Args,
+ Make_Pragma_Argument_Association
+ (Sloc (Comp_Expr_Repl),
+ Expression => Comp_Expr_Repl));
+ end loop;
+
+ Comp_Assn := First (Component_Associations (N));
+ while Present (Comp_Assn) loop
+ Choice := First (Choices (Comp_Assn));
+ Append_To
+ (Args,
+ Make_Pragma_Argument_Association
+ (Sloc (Comp_Assn),
+ Chars => Chars (Choice),
+ Expression => Expression (Comp_Assn)));
+ Next (Comp_Assn);
+ end loop;
+ return Args;
+ end Aggregate_To_Associations;
+
+ ----------------------------------------
+ -- Validate_Assertion_Level_Aggregate --
+ ----------------------------------------
+
+ procedure Validate_Assertion_Level_Aggregate (N : Node_Id) is
+ Comp_Assn : Node_Id;
+ Choice : Node_Id;
+ begin
+ Comp_Assn := First (Component_Associations (N));
+ while Present (Comp_Assn) loop
+ if List_Length (Choices (Comp_Assn)) /= 1 then
+ Error_Pragma_Arg
+ ("only one Assertion_Level can be associated "
+ & "with an expression",
+ Comp_Assn);
+ end if;
+
+ Choice := First (Choices (Comp_Assn));
+
+ if Nkind (Choice) /= N_Identifier then
+ Error_Pragma_Arg
+ ("\association must denote an Assertion_Level", Comp_Assn);
+ end if;
+ Next (Comp_Assn);
+ end loop;
+ end Validate_Assertion_Level_Aggregate;
+
+ -- Local variables
+
+ Args : List_Id;
+
+ -- Start of proessing for Create_Pragma_Without_Assertion_Level
+
+ begin
+ if Nkind (Expr) in N_Aggregate then
+ Validate_Assertion_Level_Aggregate (Expr);
+ Args := Aggregate_To_Associations (Expr);
+ else
+ Args :=
+ New_List
+ (Make_Pragma_Argument_Association (Sloc (Expr),
+ Expression => Expr));
+ end if;
+
+ return
+ Make_Pragma (Sloc (N),
+ Chars => Pname,
+ Pragma_Argument_Associations => Args);
+ end Create_Pragma_Without_Assertion_Level;
+
---------------------------
-- Ensure_Aggregate_Form --
---------------------------
end Set_Ravenscar_Profile;
+ -- Local variables
+
+ Assoc : Node_Id;
+ Last_Prag : Node_Id;
+ Level : Entity_Id;
+ Sub_Prag : Node_Id;
+
-- Start of processing for Analyze_Pragma
begin
elsif Is_Rewrite_Substitution (N)
and then Nkind (Original_Node (N)) = N_Pragma
then
- Set_Is_Ignored (N, Is_Ignored (Original_Node (N)));
- Set_Is_Checked (N, Is_Checked (Original_Node (N)));
+ Set_Pragma_Ghost_Assertion_Level (N, Original_Node (N));
-- Skip querying the applicable policy at this point for dynamic
-- predicate checks since they rely on the policy applicable in
-- Otherwise query the applicable policy at this point
- else
- Check_Applicable_Policy (N);
+ elsif Is_Valid_Assertion_Kind (Pname) then
+ -- If the pragma is using Assertion_Level associations, analyze the
+ -- applicable policies for that pragma and then convert it into a
+ -- pragma without assertion levels. Analyze the new pragma with
+ -- policy-related attributes (Is_Checked/Is_Ignored/Is_Disabled)
+ -- already set.
+
+ if Has_Assertion_Level_Argument (N) then
+ Assoc := First (Pragma_Argument_Associations (N));
+ Last_Prag := N;
+ while Present (Assoc) loop
+ Level := Get_Assertion_Level (Chars (Assoc));
+ Sub_Prag :=
+ Create_Pragma_Without_Assertion_Level (Expression (Assoc));
+
+ -- Set policy based attributes based on the pragma name and the
+ -- assertion level.
+
+ Check_Applicable_Policy (Sub_Prag, Level);
- -- If pragma is disabled, rewrite as NULL and skip analysis
+ -- Store the Level on the pragma node for easier access
+
+ Set_Pragma_Ghost_Assertion_Level (Sub_Prag, Level);
+
+ -- Store the Original_Pragma for the detection of
+ -- duplicates.
+
+ Set_Original_Pragma (Sub_Prag, N);
+
+ -- Insert the created pragmas in the same order after the
+ -- original pragma and analyze them later.
+
+ Insert_After (Last_Prag, Sub_Prag);
+ Last_Prag := Sub_Prag;
+
+ Next (Assoc);
+ end loop;
+
+ -- Remove the original pragma and continue processing all
+ -- of the new sub-pragmas.
- if Is_Disabled (N) then
Rewrite (N, Make_Null_Statement (Loc));
Analyze (N);
raise Pragma_Exit;
+
+ -- Otherwise apply the policy based attributes based on the pragma
+ -- name.
+
+ else
+ Check_Applicable_Policy (N, Empty);
end if;
end if;
+ -- If the pragma is disabled, rewrite it as NULL and skip its analysis
+
+ if Is_Disabled (N) then
+ Rewrite (N, Make_Null_Statement (Loc));
+ Analyze (N);
+ raise Pragma_Exit;
+ end if;
+
-- Mark assertion pragmas as Ghost depending on their enclosing context
if Assertion_Expression_Pragma (Prag_Id) then
if Present (State_Id) then
Set_Is_Ghost_Entity (State_Id);
+
+ -- Amend the Assertion_Level coming from the
+ -- package.
+
+ Set_Ghost_Assertion_Level
+ (State_Id, Standard_Level_Default);
end if;
-- Synchronous
elsif Chars (Opt_Nam) = Name_Part_Of then
Analyze_Part_Of_Option (Opt);
+ elsif Chars (Opt_Nam) = Name_Ghost then
+ Check_Duplicate_Option (Opt, Ghost_Seen);
+ Check_Ghost_Synchronous;
+
+ if Present (State_Id) then
+ Set_Is_Ghost_Entity (State_Id);
+
+ -- Amend the Assertion_Level coming from the
+ -- package.
+
+ if Nkind (Expression (Opt)) /= N_Identifier then
+ Error_Pragma_Arg
+ ("level name must be an identifier", N);
+ end if;
+ Set_Ghost_Assertion_Level
+ (State_Id,
+ Get_Assertion_Level
+ (Chars (Expression (Opt))));
+ end if;
else
SPARK_Msg_N ("invalid state option", Opt);
end if;
-- Local variables
- Expr : Node_Id;
- New_Args : List_Id;
+ Args : Args_List (1 .. 2);
+ Arg_Check : Node_Id renames Args (1);
+ Arg_Message : Node_Id renames Args (2);
+ Check_Prag : Node_Id;
+ New_Args : List_Id;
+ Names : constant Name_List (1 .. 2) :=
+ (Name_Check, Name_Message);
-- Start of processing for Assert
Check_At_Least_N_Arguments (1);
Check_At_Most_N_Arguments (2);
- Check_Arg_Order ((Name_Check, Name_Message));
- Check_Optional_Identifier (Arg1, Name_Check);
- Expr := Get_Pragma_Arg (Arg1);
+ Gather_Associations (Names, Args);
+ Check_Arg_Order (Names);
-- Special processing for Loop_Invariant, Loop_Variant or for
-- other cases where a Loop_Entry attribute is present. If the
-- assertion pragma contains attribute Loop_Entry, ensure that
-- the related pragma is within a loop.
- if Prag_Id = Pragma_Loop_Invariant
+ if Prag_Id = Pragma_Loop_Invariant
or else Prag_Id = Pragma_Loop_Variant
- or else Contains_Loop_Entry (Expr)
+ or else Contains_Loop_Entry (Arg_Check)
then
Check_Loop_Pragma_Placement;
-- Perform preanalysis to deal with embedded Loop_Entry
-- attributes.
- Preanalyze_And_Resolve_Assert_Expression (Expr, Any_Boolean);
+ Preanalyze_And_Resolve_Assert_Expression
+ (Arg_Check, Any_Boolean);
end if;
-- Implement Assert[_And_Cut]/Assume/Loop_Invariant by generating
New_Args := New_List (
Make_Pragma_Argument_Association (Loc,
Expression => Make_Identifier (Loc, Pname)),
- Make_Pragma_Argument_Association (Sloc (Expr),
- Expression => Expr));
+ Make_Pragma_Argument_Association (Sloc (Arg_Check),
+ Expression => Arg_Check));
- if Arg_Count > 1 then
- Check_Optional_Identifier (Arg2, Name_Message);
+ if Present (Arg_Message) then
-- Provide semantic annotations for optional argument, for
-- ASIS use, before rewriting.
-- Is this still needed???
- Preanalyze_And_Resolve (Expression (Arg2), Standard_String);
+ Preanalyze_And_Resolve (Arg_Message, Standard_String);
Append_To (New_Args, New_Copy_Tree (Arg2));
end if;
-- Rewrite as Check pragma
- Rewrite (N,
- Make_Pragma (Loc,
- Chars => Name_Check,
- Pragma_Argument_Associations => New_Args));
+ Check_Prag :=
+ Make_Pragma
+ (Loc,
+ Chars => Name_Check,
+ Pragma_Argument_Associations => New_Args);
+ Copy_Assertion_Policy_Attributes (Check_Prag, N);
+ Rewrite (N, Check_Prag);
Analyze (N);
end Assert;
+ ---------------------
+ -- Assertion_Level --
+ ---------------------
+
+ -- pragma Assertion_Level (LEVEL_IDENTIFIER
+ -- [, depends => DEPENDENCY_DESCRIPTOR]);
+ --
+ -- DEPENDENCY_DESCRIPTOR ::= LEVEL_IDENTIFIER | LEVEL_IDENTIFIER_LIST
+ --
+ -- LEVEL_IDENTIFIER_LIST ::= '[' LEVEL_IDENTIFIER
+ -- {, LEVEL_IDENTIFIER} ']'
+
+ when Pragma_Assertion_Level => Assertion_Level : declare
+ procedure Add_Dependencies
+ (Level : Entity_Id; Parent_Level : Entity_Id);
+ -- Adds the following dependencies:
+ -- * Adds Parent_Level to the Parent_Levels of Level
+ -- * Adds Level to the Child_Levels of Parent_Level
+
+ procedure Check_Known_Level_Name
+ (Level : Entity_Id; Ref : Node_Id);
+ -- Raise an error if the level has not be declared before
+
+ procedure Check_Valid_Level_Name (Nam : Name_Id);
+ -- Raise an error if the name matches a valid assertion kind.
+ --
+ -- This is to avoid the ambigiouty in Assertion_Policy if either
+ -- the level or the assertion kind is affected by the policy.
+
+ procedure Check_Valid_Level_Node (N : Node_Id);
+ -- Raise an error if the node is not a simple identifier
+
+ ----------------------
+ -- Add_Dependencies --
+ ----------------------
+
+ procedure Add_Dependencies
+ (Level : Entity_Id; Parent_Level : Entity_Id)
+ is
+ Parent_Level_List : Elist_Id;
+ Child_Levels_List : Elist_Id;
+ begin
+ if No (Parent_Levels (Level)) then
+ Set_Parent_Levels (Level, New_Elmt_List);
+ end if;
+ Parent_Level_List := Parent_Levels (Level);
+ Append_Elmt (Parent_Level, Parent_Level_List);
+
+ if No (Child_Levels (Parent_Level)) then
+ Set_Child_Levels (Parent_Level, New_Elmt_List);
+ end if;
+ Child_Levels_List := Child_Levels (Parent_Level);
+ Append_Elmt (Level, Child_Levels_List);
+ end Add_Dependencies;
+
+ ----------------------------
+ -- Check_Known_Level_Name --
+ ----------------------------
+
+ procedure Check_Known_Level_Name
+ (Level : Entity_Id; Ref : Node_Id) is
+ begin
+ if No (Level) then
+ Error_Msg_Name_1 := Chars (Ref);
+ Error_Msg_N ("unknown assertion level &", Ref);
+ raise Pragma_Exit;
+ end if;
+ end Check_Known_Level_Name;
+
+ ----------------------------
+ -- Check_Valid_Level_Name --
+ ----------------------------
+
+ procedure Check_Valid_Level_Name (Nam : Name_Id) is
+ begin
+ if Is_Valid_Assertion_Kind (Nam) then
+ Error_Pragma_Arg
+ ("level name cannot match an assertion kind", Arg1);
+ end if;
+ end Check_Valid_Level_Name;
+
+ ----------------------------
+ -- Check_Valid_Level_Node --
+ ----------------------------
+
+ procedure Check_Valid_Level_Node (N : Node_Id) is
+ begin
+ if Nkind (N) /= N_Identifier then
+ Error_Pragma_Arg ("level name must be an identifier", N);
+ end if;
+ end Check_Valid_Level_Node;
+
+ -- Local variables
+
+ Dep : Node_Id;
+ Dep_Id : Entity_Id;
+ Dep_Arg : Node_Id;
+ Level_Arg : Node_Id;
+ Level_Id : Entity_Id;
+ Level_Nam : Name_Id;
+
+ -- Start of processing for Pragma_Assertion_Level
+
+ begin
+ GNAT_Pragma;
+ Check_Valid_Configuration_Pragma;
+ Check_At_Least_N_Arguments (1);
+ Check_At_Most_N_Arguments (2);
+
+ Check_No_Identifier (Arg1);
+
+ Level_Arg := Expression (Arg1);
+ Check_Valid_Level_Node (Level_Arg);
+
+ Level_Nam := Chars (Level_Arg);
+ Check_Valid_Level_Name (Level_Nam);
+
+ Level_Id := Make_Assertion_Level (Loc, Level_Nam);
+
+ Set_Parent (Level_Id, Level_Arg);
+ Set_Entity (Level_Arg, Level_Id);
+
+ if Arg_Count = 2 then
+ Check_Identifier (Arg2, Name_Depends);
+
+ Dep_Arg := Expression (Arg2);
+
+ if Nkind (Dep_Arg) = N_Identifier then
+ Dep_Id := Get_Assertion_Level (Chars (Dep_Arg));
+ Check_Known_Level_Name (Dep_Id, Dep_Arg);
+ Add_Dependencies (Level_Id, Dep_Id);
+ elsif Nkind (Dep_Arg) = N_Aggregate then
+ Dep := First (Expressions (Dep_Arg));
+ while Present (Dep) loop
+ Check_Valid_Level_Node (Dep);
+ Dep_Id := Get_Assertion_Level (Chars (Dep));
+ Check_Known_Level_Name (Dep_Id, Dep);
+ Add_Dependencies (Level_Id, Dep_Id);
+
+ Next (Dep);
+ end loop;
+ else
+ Error_Pragma_Arg
+ ("depends argument must be either "
+ & "an identifier or "
+ & "an aggregate of identifiers", Dep_Arg);
+ end if;
+ end if;
+
+ -- Register the new Assertion_Level
+
+ Insert_Assertion_Level (Level_Id);
+ end Assertion_Level;
+
----------------------
-- Assertion_Policy --
----------------------
-- ASSERTION_KIND => POLICY_IDENTIFIER
-- {, ASSERTION_KIND => POLICY_IDENTIFIER});
- -- ASSERTION_KIND ::= RM_ASSERTION_KIND | ID_ASSERTION_KIND
+ -- ASSERTION_KIND ::= RM_ASSERTION_KIND |
+ -- ID_ASSERTION_KIND |
+ -- LEVEL_IDENTIFIER
-- RM_ASSERTION_KIND ::= Assert |
-- Static_Predicate |
-- Local variables
+ Policy_Names : constant Name_List :=
+ (Name_Check, Name_Disable, Name_Ignore, Name_Suppressible);
+
Arg : Node_Id;
+ Id : Node_Id;
Kind : Name_Id;
+ Level : Entity_Id;
LocP : Source_Ptr;
Policy : Node_Id;
and then (Nkind (Arg1) /= N_Pragma_Argument_Association
or else Chars (Arg1) = No_Name)
then
- Check_Arg_Is_One_Of (Arg1,
- Name_Check, Name_Disable, Name_Ignore, Name_Suppressible);
+ Check_Arg_Is_One_Of (Arg1, Policy_Names);
Resolve_Suppressible (Arg1);
-- Check Kind and Policy have allowed forms
Kind := Chars (Arg);
+ Id := Make_Identifier (LocP, Kind);
Policy := Get_Pragma_Arg (Arg);
if not Is_Valid_Assertion_Kind (Kind) then
- Error_Pragma_Arg
- ("invalid assertion kind for pragma%", Arg);
+ Set_Entity (Id, Get_Assertion_Level (Kind));
+ Level := Entity (Id);
+ if No (Level)
+ or else Ekind (Level) /= E_Assertion_Level
+ then
+ Error_Pragma_Arg
+ ("invalid assertion kind for pragma%",
+ Arg);
+ end if;
end if;
- Check_Arg_Is_One_Of (Arg,
- Name_Check, Name_Disable, Name_Ignore, Name_Suppressible);
+ Check_Arg_Is_One_Of (Arg, Policy_Names);
Resolve_Suppressible (Arg);
Chars => Name_Check_Policy,
Pragma_Argument_Associations => New_List (
Make_Pragma_Argument_Association (LocP,
- Expression => Make_Identifier (LocP, Kind)),
+ Expression => Id),
Make_Pragma_Argument_Association (LocP,
Expression => Policy))));
pragma Assert (Has_Dynamic_Predicate_Aspect (Typ));
if not Predicates_Ignored (Typ) then
- Set_Is_Checked (N, True);
- Set_Is_Ignored (N, False);
+ Mark_Is_Checked (N);
else
- Set_Is_Checked (N, False);
- Set_Is_Ignored (N, True);
+ Mark_Is_Ignored (N);
end if;
end Handle_Dynamic_Predicate_Check;
Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config;
-- Save the Ghost-related attributes to restore on exit
+ Names : constant Name_List (1 .. 3) :=
+ (Name_Name, Name_Check, Name_Message);
+
+ Args : Args_List (1 .. 3);
+ Arg_Name : Node_Id renames Args (1);
+ Arg_Check : Node_Id renames Args (2);
+ Arg_Message : Node_Id renames Args (3);
+
Cname : Name_Id;
Eloc : Source_Ptr;
- Expr : Node_Id;
- Str : Node_Id;
- pragma Warnings (Off, Str);
-- Start of processing for Pragma_Check
GNAT_Pragma;
Check_At_Least_N_Arguments (2);
Check_At_Most_N_Arguments (3);
- Check_Optional_Identifier (Arg1, Name_Name);
- Check_Optional_Identifier (Arg2, Name_Check);
- if Arg_Count = 3 then
- Check_Optional_Identifier (Arg3, Name_Message);
- Str := Get_Pragma_Arg (Arg3);
- end if;
+ Gather_Associations (Names, Args);
- Rewrite_Assertion_Kind (Get_Pragma_Arg (Arg1));
- Check_Arg_Is_Identifier (Arg1);
- Cname := Chars (Get_Pragma_Arg (Arg1));
+ Rewrite_Assertion_Kind (Arg_Name);
+ Check_Arg_Is_Identifier (Arg_Name);
+ Cname := Chars (Arg_Name);
-- Check forbidden name Assertions or Statement_Assertions
when Name_Assertions =>
Error_Pragma_Arg
("""Assertions"" is not allowed as a check kind for "
- & "pragma%", Arg1);
+ & "pragma%", Arg_Name);
when Name_Statement_Assertions =>
Error_Pragma_Arg
("""Statement_Assertions"" is not allowed as a check kind "
- & "for pragma%", Arg1);
+ & "for pragma%", Arg_Name);
when others =>
null;
elsif Is_Rewrite_Substitution (N)
and then Nkind (Original_Node (N)) = N_Pragma
then
- Set_Is_Ignored (N, Is_Ignored (Original_Node (N)));
- Set_Is_Checked (N, Is_Checked (Original_Node (N)));
+ Copy_Assertion_Policy_Attributes (N, Original_Node (N));
-- Internally added dynamic predicate checks require checking the
-- applicable policy at the point of the type declaration of their
-- Otherwise query the applicable policy at this point
else
- case Check_Kind (Cname) is
- when Name_Ignore =>
- Set_Is_Ignored (N, True);
- Set_Is_Checked (N, False);
+ Apply_Check_Policy (N, Get_Applicable_Policy (Cname, Empty));
- when Name_Check =>
- Set_Is_Ignored (N, False);
- Set_Is_Checked (N, True);
+ -- For disable, rewrite pragma as null statement and skip
+ -- rest of the analysis of the pragma.
- -- For disable, rewrite pragma as null statement and skip
- -- rest of the analysis of the pragma.
-
- when Name_Disable =>
- Rewrite (N, Make_Null_Statement (Loc));
- Analyze (N);
- raise Pragma_Exit;
-
- -- No other possibilities
-
- when others =>
- raise Program_Error;
- end case;
+ if Is_Disabled (N) then
+ Rewrite (N, Make_Null_Statement (Loc));
+ Analyze (N);
+ raise Pragma_Exit;
+ end if;
end if;
- -- If check kind was not Disable, then continue pragma analysis
-
- Expr := Get_Pragma_Arg (Arg2);
-
-- Mark the pragma (or, if rewritten from an aspect, the original
-- aspect) as enabled. Nothing to do for an internally generated
-- check for a dynamic predicate.
-- expression is only evaluated if the check fails and
-- Assertion_Error is to be raised.
- if Arg_Count = 3 then
- Preanalyze_And_Resolve (Str, Standard_String);
+ if Present (Arg_Message) then
+ Preanalyze_And_Resolve (Arg_Message, Standard_String);
end if;
-- Now you might think we could just do the same with the Boolean
-- warning when we delete the if statement.
if Expander_Active and Is_Ignored_In_Codegen (N) then
- Eloc := Sloc (Expr);
+ Eloc := Sloc (Arg_Check);
Rewrite (N,
Make_If_Statement (Eloc,
Condition =>
Make_And_Then (Eloc,
Left_Opnd => Make_Identifier (Eloc, Name_False),
- Right_Opnd => Expr),
+ Right_Opnd => Arg_Check),
Then_Statements => New_List (
Make_Null_Statement (Eloc))));
else
In_Assertion_Expr := In_Assertion_Expr + 1;
- Analyze_And_Resolve (Expr, Any_Boolean);
+ Analyze_And_Resolve (Arg_Check, Any_Boolean);
In_Assertion_Expr := In_Assertion_Expr - 1;
end if;
-- new form syntax.
when Pragma_Check_Policy => Check_Policy : declare
- Kind : Node_Id;
+ procedure Get_All_Child_Levels
+ (Level : Entity_Id;
+ Deps : in out Elist_Id);
+ -- Add all of the transitive children of the given Level to the
+ -- Deps list.
+
+ procedure Get_All_Parent_Levels
+ (Level : Entity_Id;
+ Deps : in out Elist_Id);
+ -- Add all of the transitive parents of the given Level to the
+ -- Deps list.
+
+ --------------------------
+ -- Get_All_Child_Levels --
+ --------------------------
+
+ procedure Get_All_Child_Levels
+ (Level : Entity_Id;
+ Deps : in out Elist_Id)
+ is
+ It : Elmt_Id;
+ Child_Lvl : Entity_Id;
+ begin
+ if No (Child_Levels (Level)) then
+ return;
+ end if;
+
+ It := First_Elmt (Child_Levels (Level));
+ while Present (It) loop
+ Child_Lvl := Node (It);
+ if not Contains (Deps, Child_Lvl) then
+ Append_New_Elmt (Child_Lvl, Deps);
+ Get_All_Child_Levels (Child_Lvl, Deps);
+ end if;
+
+ Next_Elmt (It);
+ end loop;
+ end Get_All_Child_Levels;
+
+ ---------------------------
+ -- Get_All_Parent_Levels --
+ ---------------------------
+
+ procedure Get_All_Parent_Levels
+ (Level : Entity_Id;
+ Deps : in out Elist_Id)
+ is
+ It : Elmt_Id;
+ D : Entity_Id;
+ begin
+ if No (Parent_Levels (Level)) then
+ return;
+ end if;
+
+ It := First_Elmt (Parent_Levels (Level));
+ while Present (It) loop
+ D := Node (It);
+
+ if not Contains (Deps, D) then
+ Append_New_Elmt (D, Deps);
+ Get_All_Parent_Levels (D, Deps);
+ end if;
+
+ Next_Elmt (It);
+ end loop;
+ end Get_All_Parent_Levels;
+
+ -- Local variables
+
+ Policy_Names : constant Name_List :=
+ (Name_On, Name_Off, Name_Check, Name_Disable, Name_Ignore);
+
+ Affected_Levels : Elist_Id := New_Elmt_List;
+ Depends_On_Static : Boolean := False;
+
+ Kind : Node_Id;
+ Level : Entity_Id;
+ L : Entity_Id;
+ L_It : Elmt_Id;
+ L_Id : Node_Id;
+ New_P : Node_Id;
+ Policy_Nam : Name_Id;
+
+ -- Start of processing for Pragma Check_Policy
begin
GNAT_Pragma;
-- Check policy
Check_Optional_Identifier (Arg2, Name_Policy);
- Check_Arg_Is_One_Of
- (Arg2,
- Name_On, Name_Off, Name_Check, Name_Disable, Name_Ignore);
+ Check_Arg_Is_One_Of (Arg2, Policy_Names);
+
+ Policy_Nam := Chars (Get_Pragma_Arg (Arg2));
-- And chain pragma on the Check_Policy_List for search
Set_Next_Pragma (N, Opt.Check_Policy_List);
Opt.Check_Policy_List := N;
+ -- For Assertion_Levels create new policies for all of the
+ -- level dependencies.
+
+ if Present (Entity (Kind))
+ and then Ekind (Entity (Kind)) = E_Assertion_Level
+ then
+ Level := Entity (Kind);
+
+ Depends_On_Static :=
+ Depends_On_Level (Level, Standard_Level_Static);
+
+ if Policy_Nam in Name_On | Name_Check then
+ if Level = Standard_Level_Static then
+ Error_Pragma_Arg
+ ("policy for `Static` cannot be changed to `Check`",
+ Arg1);
+ elsif Depends_On_Static then
+ Error_Pragma_Arg
+ ("Policy for a level that depends on `Static` "
+ & "cannot be changed to `Check`",
+ Arg1);
+ end if;
+ end if;
+
+ if Policy_Nam in Name_Off | Name_Ignore
+ and then Level = Standard_Level_Runtime
+ then
+ Error_Pragma_Arg
+ ("policy for `Runtime` cannot be changed to `Ignore`",
+ Arg1);
+ end if;
+
+ -- For Assertion_Levels create new policyies for all of the
+ -- level dependencies.
+
+ if Policy_Nam in Name_On | Name_Check then
+
+ -- Activating a level activates all levels that it
+ -- depends on (Parent_Levels).
+
+ Get_All_Parent_Levels (Level, Affected_Levels);
+ elsif Policy_Nam in Name_Off | Name_Ignore then
+
+ -- Deactivating a level deactivates all levels that
+ -- depend on it (Child_Levels)
+
+ Get_All_Child_Levels (Level, Affected_Levels);
+ end if;
+
+ L_It := First_Elmt (Affected_Levels);
+ while Present (L_It) loop
+ L := Node (L_It);
+ L_Id := Make_Identifier (Sloc (Arg1), Chars (L));
+ Set_Entity (L_Id, L);
+ New_P :=
+ Make_Pragma (Sloc (N),
+ Chars => Name_Check_Policy,
+ Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Sloc (Arg1),
+ Expression => L_Id),
+ Make_Pragma_Argument_Association (Sloc (Arg2),
+ Expression =>
+ New_Copy_Tree (Get_Pragma_Arg (Arg2)))));
+
+ -- We have collected the unique list of all transitive
+ -- Parent_Levels or Child_Levels. Avoid calculating
+ -- them again.
+
+ Set_Analyzed (New_P);
+
+ Set_Next_Pragma (New_P, Opt.Check_Policy_List);
+ Opt.Check_Policy_List := New_P;
+
+ Next_Elmt (L_It);
+ end loop;
+ end if;
+
-- For the new syntax, what we do is to convert each argument to
-- an old syntax equivalent. We do that because we want to chain
-- old style Check_Policy pragmas for the search (we don't want
Arg : Node_Id;
Argx : Node_Id;
LocP : Source_Ptr;
- New_P : Node_Id;
-
begin
Arg := Arg1;
while Present (Arg) loop
Check_No_Identifiers;
Check_At_Most_N_Arguments (2); -- Accounts for implicit type arg
+ -- The value "null" cannot be associated with an assertion level
+ -- as it has no runtime semantics.
+
+ if Present (Pragma_Ghost_Assertion_Level (N))
+ and then Pragma_Ghost_Assertion_Level (N)
+ /= Standard_Level_Default
+ and then Present (Arg1)
+ and then Nkind (Get_Pragma_Arg (Arg1)) = N_Null
+ then
+ Error_Pragma_Arg
+ ("null argument cannot be used together "
+ & "with assertion levels",
+ Arg1);
+ end if;
+
Typ := Empty;
Stmt := Prev (N);
while Present (Stmt) loop
-- Skip prior pragmas, but check for duplicates
if Nkind (Stmt) = N_Pragma then
- if Pragma_Name (Stmt) = Pname then
+ if Pragma_Name (Stmt) = Pname
+ and then not From_Same_Pragma (N, Stmt)
+ then
Duplication_Error
(Prag => N,
Prev => Stmt);
GNAT_Pragma;
Check_Arg_Count (1);
Check_No_Identifiers;
- Check_Arg_Is_One_Of (Arg1, Name_On, Name_Off, Name_All_Extensions);
+ Check_Arg_Is_One_Of
+ (Arg1, (Name_On, Name_Off, Name_All_Extensions));
if Chars (Get_Pragma_Arg (Arg1)) = Name_On then
Ada_Version := Ada_With_Core_Extensions;
if Arg_Count = 2 then
Check_Arg_Is_One_Of
- (Arg2, Name_As_Is, Name_Uppercase, Name_Lowercase);
+ (Arg2, (Name_As_Is, Name_Uppercase, Name_Lowercase));
case Chars (Get_Pragma_Arg (Arg2)) is
when Name_As_Is =>
-- Ghost --
-----------
- -- pragma Ghost [ (static_boolean_EXPRESSION) ];
+ -- pragma Ghost [ (static_boolean_EXPRESSION
+ -- | Assertion_Level) ];
when Pragma_Ghost => Ghost : declare
Context : Node_Id;
Expr : Node_Id;
Id : Entity_Id;
+ Is_Ghost : Boolean := True;
+ Level : Entity_Id;
Orig_Stmt : Node_Id;
Prev_Id : Entity_Id;
Stmt : Node_Id;
if Present (Arg1) then
Expr := Get_Pragma_Arg (Arg1);
- Analyze_And_Resolve (Expr, Standard_Boolean);
-
- if Is_OK_Static_Expression (Expr) then
-
- -- "Ghostness" cannot be turned off once enabled within a
- -- region (SPARK RM 6.9(6)).
+ if Nkind (Expr) /= N_Identifier
+ or else No (Get_Assertion_Level (Chars (Expr)))
+ then
+ Analyze_And_Resolve (Expr, Standard_Boolean);
- if Is_False (Expr_Value (Expr))
- and then Ghost_Config.Ghost_Mode > None
- then
- Error_Pragma
- ("pragma % with value False cannot appear in enabled "
- & "ghost region");
+ if not Is_OK_Static_Expression (Expr) then
+ Error_Pragma_Arg
+ ("expression of pragma % must be static", Expr);
end if;
- -- Otherwise the expression is not static
+ if Is_False (Expr_Value (Expr)) then
+ Is_Ghost := False;
- else
- Error_Pragma_Arg
- ("expression of pragma % must be static", Expr);
+ -- "Ghostness" cannot be turned off once enabled within a
+ -- region (SPARK RM 6.9(6)).
+
+ if Ghost_Config.Ghost_Mode > None then
+ Error_Pragma
+ ("pragma % with value False cannot appear in enabled"
+ & " ghost region");
+ end if;
+ end if;
end if;
end if;
- Set_Is_Ghost_Entity (Id);
+ Level := Assertion_Level_From_Arg (Arg1);
+
+ -- Associate the assertion level before determing the kind of
+ -- ghost entity we should mark the entity as.
+
+ Set_Ghost_Assertion_Level (Id, Level);
+
+ -- Store it on the pragma node as well
+
+ Set_Pragma_Ghost_Assertion_Level (N, Level);
+
+ -- Mark it as a Ghost entity unless it was explicitly marked with
+ -- pragma Ghost (False).
+
+ if Is_Ghost then
+ Set_Is_Ghost_Entity (Id);
+ end if;
end Ghost;
------------
Proc_Id : Entity_Id;
Typ : Entity_Id;
+ Impl_Names : constant Name_List := (Name_By_Any,
+ Name_By_Entry,
+ Name_By_Protected_Procedure,
+ Name_Optional);
begin
Ada_2012_Pragma;
Check_Arg_Count (2);
Check_No_Identifiers;
Check_Arg_Is_Identifier (Arg1);
Check_Arg_Is_Local_Name (Arg1);
- Check_Arg_Is_One_Of (Arg2,
- Name_By_Any,
- Name_By_Entry,
- Name_By_Protected_Procedure,
- Name_Optional);
+ Check_Arg_Is_One_Of (Arg2, Impl_Names);
-- Extract the name of the local procedure
when Pragma_Loop_Optimize => Loop_Optimize : declare
Hint : Node_Id;
+ Hint_Names : constant Name_List := (Name_Ivdep,
+ Name_No_Unroll,
+ Name_Unroll,
+ Name_No_Vector,
+ Name_Vector);
begin
GNAT_Pragma;
Check_At_Least_N_Arguments (1);
Hint := First (Pragma_Argument_Associations (N));
while Present (Hint) loop
- Check_Arg_Is_One_Of (Hint, Name_Ivdep,
- Name_No_Unroll,
- Name_Unroll,
- Name_No_Vector,
- Name_Vector);
+ Check_Arg_Is_One_Of (Hint, Hint_Names);
Next (Hint);
end loop;
when Pragma_Optimize =>
Check_No_Identifiers;
Check_Arg_Count (1);
- Check_Arg_Is_One_Of (Arg1, Name_Time, Name_Space, Name_Off);
+ Check_Arg_Is_One_Of (Arg1, (Name_Time, Name_Space, Name_Off));
------------------------
-- Optimize_Alignment --
-- removal of ignored Ghost code.
if From_Aspect_Specification (N)
- and then Get_Aspect_Id
- (Chars (Identifier (Corresponding_Aspect (N))))
- = Aspect_Ghost_Predicate
+ and then Get_Aspect_Id (Corresponding_Aspect (N))
+ = Aspect_Ghost_Predicate
then
- Mark_Ghost_Pragma
- (N, Name_To_Ghost_Mode (Policy_In_Effect (Name_Ghost)));
+ -- For Ghost_Predicate we have already analyzed the applicable
+ -- ghost policy already and set the policy using Is_Checked and
+ -- Is_Ignored.
+
+ if Is_Ignored (N) then
+ Mark_Ghost_Pragma (N, Opt.Ignore);
+ else
+ Mark_Ghost_Pragma (N, Opt.Check);
+ end if;
else
Mark_Ghost_Pragma (N, Typ);
end if;
-- Check the legality of the mode (no argument = ON)
if Arg_Count = 1 then
- Check_Arg_Is_One_Of (Arg1, Name_Auto, Name_On, Name_Off);
+ Check_Arg_Is_One_Of (Arg1, (Name_Auto, Name_On, Name_Off));
Mode := Chars (Get_Pragma_Arg (Arg1));
else
Mode := Name_On;
GNAT_Pragma;
Check_Arg_Count (1);
Check_No_Identifiers;
- Check_Arg_Is_One_Of (Arg1, Name_Error, Name_Warn, Name_Allow);
+ Check_Arg_Is_One_Of (Arg1, (Name_Error, Name_Warn, Name_Allow));
-- Suppress/Unsuppress can appear as a configuration pragma, or in
-- a declarative part or a package spec.
-- A list that contains all refined states processed so far. The list is
-- used to detect duplicate refinements.
+ Saved_Ghost_Config : constant Ghost_Config_Type := Ghost_Config;
+ -- Ghost configuration before starting to process this pragma
+
procedure Analyze_Refinement_Clause (Clause : Node_Id);
-- Perform full analysis of a single refinement clause
return;
end if;
+ -- Get the Ghost context from the pragma before analyzing its parts
+
+ Set_Ghost_Mode (N);
+
-- Save the scenario for examination by the ABE Processing phase
Record_Elaboration_Scenario (N);
Report_Unrefined_States (Available_States);
Set_Is_Analyzed_Pragma (N);
+
+ Restore_Ghost_Region (Saved_Ghost_Config);
end Analyze_Refined_State_In_Decl_Part;
---------------------------------------------
return False;
end Appears_In;
+ ------------------------
+ -- Apply_Check_Policy --
+ ------------------------
+
+ procedure Apply_Check_Policy (N : Node_Id; Policy : Name_Id) is
+ begin
+ case Policy is
+ when Name_Ignore | Name_Off =>
+ Mark_Is_Ignored (N);
+
+ when Name_Check | Name_On =>
+ Mark_Is_Checked (N);
+
+ when Name_Disable =>
+ Mark_Is_Disabled (N);
+
+ -- That should be exhaustive, the null here is a defence
+ -- against a malformed tree from previous errors.
+
+ when others =>
+ null;
+ end case;
+ end Apply_Check_Policy;
+
-----------------------------------
-- Build_Pragma_Check_Equivalent --
-----------------------------------
-- Check_Applicable_Policy --
-----------------------------
- procedure Check_Applicable_Policy (N : Node_Id) is
- PP : Node_Id;
- Policy : Name_Id;
-
- Ename : constant Name_Id := Original_Aspect_Pragma_Name (N);
+ procedure Check_Applicable_Policy (N : Node_Id; Level : Entity_Id := Empty)
+ is
+ Nam : constant Name_Id := Original_Aspect_Pragma_Name (N);
begin
-- No effect if not valid assertion kind name
- if not Is_Valid_Assertion_Kind (Ename) then
+ if not Is_Valid_Assertion_Kind (Nam) then
return;
end if;
- -- Loop through entries in check policy list
-
- PP := Opt.Check_Policy_List;
- while Present (PP) loop
- declare
- PPA : constant List_Id := Pragma_Argument_Associations (PP);
- Pnm : constant Name_Id := Chars (Get_Pragma_Arg (First (PPA)));
-
- begin
- if Ename = Pnm
- or else Pnm = Name_Assertion
- or else (Pnm = Name_Statement_Assertions
- and then Ename in Name_Assert
- | Name_Assert_And_Cut
- | Name_Assume
- | Name_Loop_Invariant
- | Name_Loop_Variant)
- then
- Policy := Chars (Get_Pragma_Arg (Last (PPA)));
-
- case Policy is
- when Name_Ignore
- | Name_Off
- =>
- Set_Is_Checked (N, False);
- Set_Is_Ignored (N, True);
-
- when Name_Check
- | Name_On
- =>
- Set_Is_Checked (N, True);
- Set_Is_Ignored (N, False);
-
- when Name_Disable =>
- Set_Is_Ignored (N, True);
- Set_Is_Checked (N, False);
- Set_Is_Disabled (N, True);
-
- -- That should be exhaustive, the null here is a defence
- -- against a malformed tree from previous errors.
-
- when others =>
- null;
- end case;
-
- return;
- end if;
-
- PP := Next_Pragma (PP);
- end;
- end loop;
-
- -- If there are no specific entries that matched, then we let the
- -- setting of assertions govern. Note that this provides the needed
- -- compatibility with the RM for the cases of assertion, invariant,
- -- precondition, predicate, and postcondition. Note also that
- -- Assertions_Enabled is forced in CodePeer mode and GNATprove mode.
-
- if Assertions_Enabled then
- Set_Is_Checked (N, True);
- Set_Is_Ignored (N, False);
- else
- Set_Is_Checked (N, False);
- Set_Is_Ignored (N, True);
- end if;
+ Apply_Check_Policy (N, Get_Applicable_Policy (Nam, Level));
end Check_Applicable_Policy;
-------------------------------
Item);
end Check_External_Properties;
- ----------------
- -- Check_Kind --
- ----------------
-
- function Check_Kind (Nam : Name_Id) return Name_Id is
- PP : Node_Id;
-
- begin
- -- Loop through entries in check policy list
-
- PP := Opt.Check_Policy_List;
- while Present (PP) loop
- declare
- PPA : constant List_Id := Pragma_Argument_Associations (PP);
- Pnm : constant Name_Id := Chars (Get_Pragma_Arg (First (PPA)));
-
- begin
- if Nam = Pnm
- or else (Pnm = Name_Assertion
- and then Is_Valid_Assertion_Kind (Nam))
- or else (Pnm = Name_Statement_Assertions
- and then Nam in Name_Assert
- | Name_Assert_And_Cut
- | Name_Assume
- | Name_Loop_Invariant
- | Name_Loop_Variant)
- then
- case Chars (Get_Pragma_Arg (Last (PPA))) is
- when Name_Check
- | Name_On
- =>
- return Name_Check;
-
- when Name_Ignore
- | Name_Off
- =>
- return Name_Ignore;
-
- when Name_Disable =>
- return Name_Disable;
-
- when others =>
- raise Program_Error;
- end case;
-
- else
- PP := Next_Pragma (PP);
- end if;
- end;
- end loop;
-
- -- If there are no specific entries that matched, then we let the
- -- setting of assertions govern. Note that this provides the needed
- -- compatibility with the RM for the cases of assertion, invariant,
- -- precondition, predicate, and postcondition.
-
- if Assertions_Enabled then
- return Name_Check;
- else
- return Name_Ignore;
- end if;
- end Check_Kind;
-
---------------------------
-- Check_Missing_Part_Of --
---------------------------
end if;
end Duplication_Error;
+ --------------------------
+ -- Find_Assertion_Level --
+ --------------------------
+
+ function Find_Assertion_Level (Nam : Name_Id) return Entity_Id is
+ begin
+ for J in Assertion_Levels.First .. Assertion_Levels.Last loop
+ if Chars (Assertion_Levels.Table (J)) = Nam then
+ return Assertion_Levels.Table (J);
+ end if;
+ end loop;
+
+ return Empty;
+ end Find_Assertion_Level;
+
------------------------------
-- Find_Encapsulating_State --
------------------------------
if Nkind (Stmt) = N_Pragma then
if Do_Checks
and then Original_Aspect_Pragma_Name (Stmt) = Prag_Nam
+ and then not From_Same_Pragma (Prag, Stmt)
then
- Duplication_Error
- (Prag => Prag,
- Prev => Stmt);
+ Duplication_Error (Prag => Prag, Prev => Stmt);
end if;
-- Emit an error when a refinement pragma appears on an expression
-- Skip prior pragmas, but check for duplicates
if Nkind (Stmt) = N_Pragma then
- if Do_Checks and then Pragma_Name (Stmt) = Prag_Nam then
- Duplication_Error
- (Prag => Prag,
- Prev => Stmt);
+ if Do_Checks
+ and then Pragma_Name (Stmt) = Prag_Nam
+ and then not From_Same_Pragma (Prag, Stmt)
+ then
+ Duplication_Error (Prag => Prag, Prev => Stmt);
end if;
-- Skip internally generated code
end if;
end Find_Related_Package_Or_Body;
+ ---------------------------
+ -- Get_Applicable_Policy --
+ ---------------------------
+
+ function Get_Applicable_Policy
+ (Nam : Name_Id; Level : Entity_Id) return Name_Id
+ is
+ function Is_Statement_Assertion (Nam : Name_Id) return Boolean
+ is (Nam
+ in Name_Assert
+ | Name_Assert_And_Cut
+ | Name_Assume
+ | Name_Loop_Invariant
+ | Name_Loop_Variant);
+
+ -- Local variables
+
+ Assocs : List_Id;
+ P_Arg : Node_Id;
+ P_Nam : Name_Id;
+ Policy_Prag : Node_Id;
+
+ -- Start of processing for Get_Applicable_Policy
+
+ begin
+ -- Runtime level should always be checked irregardless of other
+ -- policies that are applied.
+
+ if Level = Standard_Level_Runtime then
+ return Name_Check;
+
+ -- Static level or levels that depend on Static should never be
+ -- checked irregardless of other policies that are applied.
+
+ elsif Level = Standard_Level_Static
+ or else Depends_On_Level (Level, Standard_Level_Static)
+ then
+ return Name_Ignore;
+ end if;
+
+ -- Loop through entries in check policy list
+
+ Policy_Prag := Opt.Check_Policy_List;
+ while Present (Policy_Prag) loop
+ Assocs := Pragma_Argument_Associations (Policy_Prag);
+ P_Arg := Get_Pragma_Arg (First (Assocs));
+ P_Nam := Chars (P_Arg);
+
+ if P_Nam = Nam
+ or else P_Nam = Name_Assertion
+ or else (P_Nam = Name_Statement_Assertions
+ and then Is_Statement_Assertion (Nam))
+ or else (Present (Level) and then Entity (P_Arg) = Level)
+ then
+ return Chars (Get_Pragma_Arg (Last (Assocs)));
+ end if;
+
+ Policy_Prag := Next_Pragma (Policy_Prag);
+ end loop;
+
+ -- If there are no specific entries that matched, then we let the
+ -- setting of assertions govern. Note that this provides the
+ -- needed compatibility with the RM for the cases of assertion,
+ -- invariant, precondition, predicate, and postcondition. Note
+ -- also that Assertions_Enabled is forced in CodePeer mode and
+ -- GNATprove mode.
+
+ if Assertions_Enabled then
+ return Name_Check;
+ else
+ return Name_Ignore;
+ end if;
+ end Get_Applicable_Policy;
+
------------------
-- Get_Argument --
------------------
end if;
end Get_Argument;
+ -------------------------
+ -- Get_Assertion_Level --
+ -------------------------
+
+ function Get_Assertion_Level (Nam : Name_Id) return Entity_Id is
+ begin
+ if Nam = No_Name then
+ return Empty;
+ end if;
+
+ return Find_Assertion_Level (Nam);
+ end Get_Assertion_Level;
+
-------------------------
-- Get_Base_Subprogram --
-------------------------
begin
Externals.Init;
Compile_Time_Warnings_Errors.Init;
+ Assertion_Levels.Init;
end Initialize;
--------
Dummy := Dummy + 1;
end ip;
+ ----------------------------
+ -- Insert_Assertion_Level --
+ ----------------------------
+
+ procedure Insert_Assertion_Level (Level : Entity_Id) is
+ Nam : constant Name_Id := Chars (Level);
+
+ Dupl : constant Entity_Id := Find_Assertion_Level (Nam);
+
+ function Same_Dependencies (Self, Other : Entity_Id) return Boolean;
+ -- Check that both levels have the same number of dependencies and the
+ -- names of the dependencies match.
+
+ -----------------------
+ -- Same_Dependencies --
+ -----------------------
+
+ function Same_Dependencies (Self, Other : Entity_Id) return Boolean is
+ Other_El : Elmt_Id;
+ Other_Level : Entity_Id;
+ Self_El : Elmt_Id;
+ Self_Level : Entity_Id;
+
+ begin
+ pragma Assert (Ekind (Self) = E_Assertion_Level);
+ pragma Assert (Ekind (Other) = E_Assertion_Level);
+
+ if List_Length (Parent_Levels (Self))
+ /= List_Length (Parent_Levels (Other))
+ then
+ return False;
+ end if;
+
+ if No (Parent_Levels (Self)) then
+ return True;
+ end if;
+
+ -- Check that dependencies match.
+ -- Note that we are checking for positional and element matching.
+ -- The positional part could be relaxed.
+
+ Self_El := First_Elmt (Parent_Levels (Self));
+ Other_El := First_Elmt (Parent_Levels (Other));
+ while Present (Self_El) loop
+ Self_Level := Node (Self_El);
+ Other_Level := Node (Other_El);
+
+ if Chars (Self_Level) /= Chars (Other_Level) then
+ return False;
+ end if;
+
+ Next_Elmt (Self_El);
+ Next_Elmt (Other_El);
+ end loop;
+
+ return True;
+ end Same_Dependencies;
+
+ -- Start of processing for Insert_Assertion_Level
+
+ begin
+ if No (Dupl) then
+ Assertion_Levels.Append (Level);
+ else
+ if not Same_Dependencies (Level, Dupl) then
+ Error_Msg_N
+ ("conflicting Assertion_Level definition for &", Level);
+ Error_Msg_Sloc := Sloc (Dupl);
+ Error_Msg_NE ("\differs from existing definition #", Level, Dupl);
+ end if;
+ end if;
+ end Insert_Assertion_Level;
+
-----------------------------
-- Is_Config_Static_String --
-----------------------------
Pragma_Annotate => 93,
Pragma_Assert => -1,
Pragma_Assert_And_Cut => -1,
+ Pragma_Assertion_Level => 0,
Pragma_Assertion_Policy => 0,
Pragma_Assume => -1,
Pragma_Assume_No_Invalid_Values => 0,
end case;
end Is_Valid_Assertion_Kind;
+ ------------------------------
+ -- Is_Valid_Assertion_Level --
+ ------------------------------
+
+ function Is_Valid_Assertion_Level (Nam : Name_Id) return Boolean is
+ begin
+ return Present (Get_Assertion_Level (Nam));
+ end Is_Valid_Assertion_Level;
+
--------------------------------------
-- Process_Compilation_Unit_Pragmas --
--------------------------------------
end if;
end Validate_Compile_Time_Warning_Or_Error;
+ ---------------------
+ -- Mark_Is_Checked --
+ ---------------------
+
+ procedure Mark_Is_Checked (N : Node_Id) is
+ begin
+ Set_Is_Checked (N, True);
+ Set_Is_Ignored (N, False);
+ end Mark_Is_Checked;
+
+ ----------------------
+ -- Mark_Is_Disabled --
+ ----------------------
+
+ procedure Mark_Is_Disabled (N : Node_Id) is
+ begin
+ Set_Is_Ignored (N, True);
+ Set_Is_Checked (N, False);
+ Set_Is_Disabled (N, True);
+ end Mark_Is_Disabled;
+
+ ---------------------
+ -- Mark_Is_Ignored --
+ ---------------------
+
+ procedure Mark_Is_Ignored (N : Node_Id) is
+ begin
+ Set_Is_Checked (N, False);
+ Set_Is_Ignored (N, True);
+ end Mark_Is_Ignored;
+
------------------------------------
-- Record_Possible_Body_Reference --
------------------------------------
(Pragma_Extensions_Visible => True,
others => False);
+ function Find_Assertion_Level (Nam : Name_Id) return Entity_Id;
+ -- Find an existing definition with the given name that has been inserted
+ -- into the Assertion_Levels table.
+
+ procedure Insert_Assertion_Level (Level : Entity_Id);
+ -- Insert a new level into the Assertion_Levels table. If there is already
+ -- an entry with the same name check that it has the same dependencies as
+ -- the level you are trying to insert. Raises an error otherwise.
+
-----------------
-- Subprograms --
-----------------
-- in fact of the same kind as the source pragma Prag. This is used
-- in GNATprove_Mode to generate the inherited pre- and postconditions.
- procedure Check_Applicable_Policy (N : Node_Id);
+ procedure Check_Applicable_Policy (N : Node_Id; Level : Entity_Id := Empty);
-- N is either an N_Aspect or an N_Pragma node. There are two cases. If
-- the name of the aspect or pragma is not one of those recognized as
-- an assertion kind by an Assertion_Policy pragma, then the call has
-- is the related variable or state. Ensure legality of the combination and
-- issue an error for an illegal combination.
- function Check_Kind (Nam : Name_Id) return Name_Id;
- -- This function is used in connection with pragmas Assert, Check,
- -- and assertion aspects and pragmas, to determine if Check pragmas
- -- (or corresponding assertion aspects or pragmas) are currently active
- -- as determined by the presence of -gnata on the command line (which
- -- sets the default), and the appearance of pragmas Check_Policy and
- -- Assertion_Policy as configuration pragmas either in a configuration
- -- pragma file, or at the start of the current unit, or locally given
- -- Check_Policy and Assertion_Policy pragmas that are currently active.
- --
- -- The value returned is one of the names Check, Ignore, Disable (On
- -- returns Check, and Off returns Ignore).
- --
- -- Note: for assertion kinds Pre'Class, Post'Class, Invariant'Class,
- -- and Type_Invariant'Class, the name passed is Name_uPre, Name_uPost,
- -- Name_uInvariant, or Name_uType_Invariant, which corresponds to _Pre,
- -- _Post, _Invariant, or _Type_Invariant, which are special names used
- -- in identifiers to represent these attribute references.
-
procedure Check_Missing_Part_Of (Item_Id : Entity_Id);
-- Determine whether the placement within the state space of an abstract
-- state, variable or package instantiation denoted by Item_Id requires the
-- Context denotes the entity of the function, package or procedure where
-- Prag resides.
+ function Get_Assertion_Level (Nam : Name_Id) return Entity_Id;
+ -- Returns the entity of a known Assertion_Level name
+
function Get_SPARK_Mode_From_Annotation
(N : Node_Id) return SPARK_Mode_Type;
-- Given an aspect or pragma SPARK_Mode node, return corresponding mode id
-- Name_uInvariant, and Name_uType_Invariant (_Pre, _Post, _Invariant,
-- and _Type_Invariant).
+ function Is_Valid_Assertion_Level (Nam : Name_Id) return Boolean;
+ -- Return True if Nam is one of the Assertion_Levels declared in the
+ -- current context.
+
procedure Process_Compilation_Unit_Pragmas (N : Node_Id);
-- Called at the start of processing compilation unit N to deal with any
-- special issues regarding pragmas. In particular, we have to deal with
-- Elaboration entity is never a ghost object, regardless of the context
-- in which this routine is called.
- Install_Ghost_Region (None, N);
+ Install_Ghost_Region (None, N, Empty);
-- Here we need the elaboration entity
end if;
end Conditional_Delay;
+ --------------------------------------
+ -- Copy_Assertion_Policy_Attributes --
+ --------------------------------------
+
+ procedure Copy_Assertion_Policy_Attributes (New_Prag, Old_Prag : Node_Id) is
+ begin
+ Set_Is_Checked (New_Prag, Is_Checked (Old_Prag));
+ Set_Is_Ignored (New_Prag, Is_Ignored (Old_Prag));
+ Set_Pragma_Ghost_Assertion_Level
+ (New_Prag, Pragma_Ghost_Assertion_Level (Old_Prag));
+ end Copy_Assertion_Policy_Attributes;
+
-------------------------
-- Copy_Component_List --
-------------------------
Def_Id : Node_Id;
Formal_Spec : Node_Id;
Result : Node_Id;
+ Level : Entity_Id;
begin
-- The structure of the original tree must be replicated without any
-- Create a new entity for the defining unit name
Def_Id := Defining_Unit_Name (Result);
+ Level := Ghost_Assertion_Level (Def_Id);
case Nkind (Def_Id) is
when N_Defining_Identifier =>
when others => raise Program_Error;
end case;
+ -- Copy the relevant Ghost Assertion_Level
+
+ Set_Ghost_Assertion_Level (Def_Id, Level);
+
Set_Defining_Unit_Name (Result, Def_Id);
-- Create new entities for the formal parameters
return Is_Variable (N) and then Paren_Count (N) = 0;
end Denotes_Variable;
+ ----------------------
+ -- Depends_On_Level --
+ ----------------------
+
+ function Depends_On_Level
+ (Self : Entity_Id; Other : Entity_Id) return Boolean
+ is
+ Elm : Elmt_Id;
+ Dep : Entity_Id;
+ begin
+ if No (Self) then
+ return False;
+ elsif No (Other) then
+ return False;
+ end if;
+
+ pragma Assert (Ekind (Self) = E_Assertion_Level);
+ pragma Assert (Ekind (Other) = E_Assertion_Level);
+
+ if No (Parent_Levels (Self)) then
+ return False;
+ end if;
+
+ Elm := First_Elmt (Parent_Levels (Self));
+ while Present (Elm) loop
+ Dep := Node (Elm);
+ if Dep = Other or else Depends_On_Level (Dep, Other) then
+ return True;
+ end if;
+
+ Next_Elmt (Elm);
+ end loop;
+
+ return False;
+ end Depends_On_Level;
+
-----------------------------
-- Depends_On_Discriminant --
-----------------------------
and then In_Open_Scopes (Scope (Pack));
end From_Nested_Package;
+ ----------------------
+ -- From_Same_Aspect --
+ ----------------------
+
+ function From_Same_Aspect (Self, Other : Node_Id) return Boolean is
+ begin
+ return
+ Present (Original_Aspect (Self))
+ and then Present (Original_Aspect (Other))
+ and then Original_Aspect (Self) = Original_Aspect (Other);
+ end From_Same_Aspect;
+
+ ----------------------
+ -- From_Same_Pragma --
+ ----------------------
+
+ function From_Same_Pragma (Self, Other : Node_Id) return Boolean is
+ begin
+ return
+ (Present (Original_Pragma (Self))
+ and then Present (Original_Pragma (Other))
+ and then Original_Pragma (Self) = Original_Pragma (Other))
+ or else (From_Aspect_Specification (Self)
+ and then From_Aspect_Specification (Other)
+ and then From_Same_Aspect
+ (Corresponding_Aspect (Self),
+ Corresponding_Aspect (Other)));
+ end From_Same_Pragma;
+
-----------------------
-- Gather_Components --
-----------------------
if Is_Entity_Name (Subp) then
Subp_Id := Entity (Subp);
+ if No (Subp_Id) then
+ return Empty;
+ end if;
+
if Ekind (Subp_Id) = E_Access_Subprogram_Type then
Subp_Id := Directly_Designated_Type (Subp_Id);
end if;
end if;
end Get_Views;
+ ----------------------------------
+ -- Has_Assertion_Level_Argument --
+ ----------------------------------
+
+ function Has_Assertion_Level_Argument (N : Node_Id) return Boolean is
+ Assocs : List_Id;
+ Assoc : Node_Id;
+ Choice : Node_Id;
+ begin
+ if Nkind (N) = N_Aspect_Specification then
+ if Nkind (Expression (N)) /= N_Aggregate then
+ return False;
+ end if;
+
+ Assocs := Component_Associations (Expression (N));
+
+ if No (Assocs) then
+ return False;
+ end if;
+
+ Assoc := First (Assocs);
+ Choice := First (Choices (Assoc));
+
+ if Nkind (Choice) = N_Identifier then
+ return Present (Get_Assertion_Level (Chars (Choice)));
+ end if;
+
+ return False;
+ else
+ pragma Assert (Nkind (N) = N_Pragma);
+ Assocs := Pragma_Argument_Associations (N);
+ Assoc := First (Assocs);
+ if Present (Assoc) and then Chars (Assoc) /= No_Name then
+ return Present (Get_Assertion_Level (Chars (Assoc)));
+ end if;
+
+ return False;
+ end if;
+ end Has_Assertion_Level_Argument;
+
------------------------------
-- Has_Compatible_Alignment --
------------------------------
-- Policy_In_Effect --
----------------------
- function Policy_In_Effect (Policy : Name_Id) return Name_Id is
+ function Policy_In_Effect
+ (Policy : Name_Id;
+ Level : Name_Id := No_Name) return Name_Id
+ is
function Policy_In_List (List : Node_Id) return Name_Id;
-- Determine the mode of a policy in a N_Pragma list
-- The current Check_Policy pragma matches the requested policy or
-- appears in the single argument form (Assertion, policy_id).
- if Chars (Arg1) in Name_Assertion | Policy then
+ if Chars (Arg1) in Name_Assertion | Policy | Level then
return Chars (Arg2);
end if;
raise Program_Error;
end if;
+ if Present (Level)
+ and then not Is_Valid_Assertion_Level (Level)
+ then
+ raise Program_Error;
+ end if;
+
-- Inspect all policy pragmas that appear within scopes (if any)
Kind := Policy_In_List (Check_Policy_List);
-- of Old_Ent is set and Old_Ent has not yet been Frozen (i.e. Is_Frozen is
-- False).
+ procedure Copy_Assertion_Policy_Attributes (New_Prag, Old_Prag : Node_Id);
+ -- Copy Is_Checked, Is_Ignored and Ghost_Assertion_Level attributes from
+ -- Old_Node.
+
function Copy_Component_List
(R_Typ : Entity_Id;
Loc : Source_Ptr) return List_Id;
function Denotes_Variable (N : Node_Id) return Boolean;
-- Returns True if node N denotes a single variable without parentheses
+ function Depends_On_Level
+ (Self : Entity_Id; Other : Entity_Id) return Boolean;
+ -- Check if Assertion_Level Self depends on the Assertion_Level Other
+ -- either directly or transitively.
+
function Depends_On_Discriminant (N : Node_Id) return Boolean;
-- Returns True if N denotes a discriminant or if N is a range, a subtype
-- indication or a scalar subtype where one of the bounds is a
-- to entities local to the nested package. In that case the package must
-- be installed on the scope stack to prevent spurious visibility errors.
+ function From_Same_Aspect (Self, Other : Node_Id) return Boolean;
+ -- True if aspects Self and Other have the same Orginal_Aspect.
+
+ function From_Same_Pragma (Self, Other : Node_Id) return Boolean;
+ -- True if pragmas Self and Other have the same Original Pragma or
+ -- they are from the same aspect.
+
procedure Gather_Components
(Typ : Entity_Id;
Comp_List : Node_Id;
-- Result of Has_Compatible_Alignment test, description found below. Note
-- that the values are arranged in increasing order of problematicness.
+ function Has_Assertion_Level_Argument (N : Node_Id) return Boolean;
+ -- Returns true if the first argument of a pragma or an aspect is using
+ -- an Assertion_Level association.
+
function Has_Compatible_Alignment
(Obj : Entity_Id;
Expr : Node_Id;
-- legal. They will need to be checked again after subprogram call has
-- been resolved.
+ function Is_Same_Or_Depends_On_Level
+ (Self : Entity_Id; Other : Entity_Id) return Boolean
+ is (Self = Other or else Depends_On_Level (Self, Other));
+ -- Check if Assertion_Level Self is or depends on the Assertion_Level Other
+
function Is_Package_Contract_Annotation (Item : Node_Id) return Boolean;
-- Determine whether aspect specification or pragma Item is one of the
-- following package contract annotations:
-- of the corresponding formal entity, otherwise returns Empty. Also
-- handles the case of references to renamings of formals.
- function Policy_In_Effect (Policy : Name_Id) return Name_Id;
+ function Policy_In_Effect
+ (Policy : Name_Id;
+ Level : Name_Id := No_Name)
+ return Name_Id;
-- Given a policy, return the policy identifier associated with it. If no
-- such policy is in effect, the value returned is No_Name.
-- ancestor of the type of the aggregate in a generic context, if any,
-- when the type is a derived tagged type. Otherwise Empty.
+ -- Aspect_Ghost_Assertion_Level
+ -- Assertion_Level that was originally used in the assertion level
+ -- associations of its arguments. These aspects are transformed to new
+ -- aspects with the associated arguments and the original assertion
+ -- level is stored in this attribute.
+
-- Aspect_On_Partial_View
-- Present on an N_Aspect_Specification node. For an aspect that applies
-- to a type entity, indicates whether the specification appears on the
-- indication carries a null-exclusion indicator, which is distinct from
-- the null-exclusion indicator that may precede the access keyword.
+ -- Original_Pragma
+ -- When aspects with assertion level associations are transformed in to
+ -- individual aspects without the assertion level we store the original
+ -- aspect in this attribute. This is used to avoid duplicate detection on
+ -- these aspects.
+
-- Original_Discriminant
-- Present in identifiers. Used in references to discriminants that
-- appear in generic units. Because the names of the discriminants may be
-- interferes with the Entity field, making it impossible to preserve the
-- original entity at the point of instantiation.
+ -- Original_Pragma
+ -- When pragmas with assertion level associations are transformed in to
+ -- individual pragmas without the assertion level we store the original
+ -- prama in this attribute. This is used to avoid duplicate detection on
+ -- these pragmas.
+
-- Others_Discrete_Choices
-- When a case statement or variant is analyzed, the semantic checks
-- determine the actual list of choices that correspond to an others
-- type, a subsequently generated error message indicates the position
-- of its full declaration.
+ -- Pragma_Ghost_Assertion_Level
+ -- Assertion_Level that was originally used in the assertion level
+ -- associations of its arguments. These pragmas are transformed to new
+ -- pragmas with the associated arguments and the original assertion
+ -- level is stored in this attribute.
+
-- Present_Expr
-- Present in an N_Variant node. This has a meaningful value only after
-- Gigi has back annotated the tree with representation information. At
-- Is_Delayed_Aspect
-- Is_Disabled
-- Import_Interface_Present
+ -- Original_Pragma
+ -- Pragma_Ghost_Assertion_Level
-- Uneval_Old_Warn
-- Note: we should have a section on what pragmas are passed on to
-- Is_Delayed_Aspect
-- Is_Disabled
-- Is_Boolean_Aspect
+ -- Aspect_Ghost_Assertion_Level
-- Aspect_On_Partial_View
+ -- Original_Aspect
-- Note: Aspect_Specification is an Ada 2012 feature
Name_Aggregate_Individually_Assign : constant Name_Id := N + $; -- GNAT
Name_Allow_Integer_Address : constant Name_Id := N + $; -- GNAT
Name_Annotate : constant Name_Id := N + $; -- GNAT
+ Name_Assertion_Level : constant Name_Id := N + $; -- GNAT
Name_Assertion_Policy : constant Name_Id := N + $; -- Ada 05
Name_Assume_No_Invalid_Values : constant Name_Id := N + $; -- GNAT
Name_C_Pass_By_Copy : constant Name_Id := N + $; -- GNAT
Name_Reference_Control_Type : constant Name_Id := N + $;
Name_Get_Element_Access : constant Name_Id := N + $;
+ -- Names used to implement Assertion_Levels
+
+ Name_uDefault_Assertion_Level : constant Name_Id := N + $;
+
-- Names for Ada 202x Aggregate aspect. Name_Aggregate is already
-- present for gprbuild.
Pragma_Aggregate_Individually_Assign,
Pragma_Allow_Integer_Address,
Pragma_Annotate,
+ Pragma_Assertion_Level,
Pragma_Assertion_Policy,
Pragma_Assume_No_Invalid_Values,
Pragma_C_Pass_By_Copy,
Standard_Op_Shift_Right_Arithmetic : Entity_Id;
-- These entities are used for shift operators generated by the expander
+ Standard_Level_Static : Entity_Id;
+ -- Assertion_Level that indicates that the associated entity is never
+ -- checked.
+
+ Standard_Level_Runtime : Entity_Id;
+ -- Assertion_Level that indicates that the associated entity is always
+ -- checked.
+
+ Standard_Level_Default : Entity_Id;
+ -- A special internally defined Assertion_Level that is applied to entities
+ -- that were not using Assertion_Levels syntactically.
+
end Stand;
null;
end Discard_Node;
+ --------------------------
+ -- Make_Assertion_Level --
+ --------------------------
+
+ function Make_Assertion_Level
+ (Loc : Source_Ptr; Nam : Name_Id) return Entity_Id
+ is
+ Level : constant Entity_Id := Make_Defining_Identifier (Loc, Nam);
+ begin
+ Mutate_Ekind (Level, E_Assertion_Level);
+ Set_Etype (Level, Standard_Void_Type);
+ return Level;
+ end Make_Assertion_Level;
+
-------------------------------------------
-- Make_Byte_Aligned_Attribute_Reference --
-------------------------------------------
-- effect (e.g. a call to the parser to parse a list of compilation
-- units), but the List_Id value is not required.
+ function Make_Assertion_Level
+ (Loc : Source_Ptr; Nam : Name_Id) return Entity_Id;
+ -- Create a new Defining_Identifier node for an Assertion_Level
+
function Make_Byte_Aligned_Attribute_Reference
(Sloc : Source_Ptr;
Prefix : Node_Id;
projects / thirdparty / gcc.git / commitdiff
