+2013-10-10 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * aspects.adb: Add entries in table Canonical_Aspects for aspects
+ Refined_Depends and Refined_Global.
+ * aspects.ads: Add entries in tables Aspect_Id, Aspect_Argument,
+ Aspect_Names, Aspect_Declay, Aspect_On_Body_Or_Stub_OK for
+ aspects Refined_Depends and Refined_Global.
+ * einfo.adb (Contract): Subprogram bodies are now valid owners
+ of contracts.
+ (Set_Contract): Subprogram bodies are now valid
+ owners of contracts.
+ (Write_Field24_Name): Output the contract
+ attribute for subprogram bodies.
+ * exp_ch6.adb (Expand_Subprogram_Contract): New routine.
+ * exp_ch6.ads (Expand_Subprogram_Contract): New routine.
+ * par-prag.adb: Pragmas Refined_Depends and Refined_Global do
+ not require any special processing by the parser.
+ * sem_ch3.adb (Adjust_D): Renamed to Adjust_Decl.
+ (Analyze_Declarations): Code reformatting. Analyze the contract
+ of a subprogram body at the end of the declarative region.
+ * sem_ch6.adb (Analyze_Generic_Subprogram_Body):
+ Subprogram bodies can now have contracts. Use
+ Expand_Subprogram_Contract to handle the various contract
+ assertions.
+ (Analyze_Subprogram_Body_Contract): New null routine.
+ (Analyze_Subprogram_Body_Helper): Subprogram bodies can now have
+ contracts. Use Expand_Subprogram_Contract to handle the various
+ contract assertions.
+ (Analyze_Subprogram_Contract): Add local
+ variable Nam. Update the call to Analyze_PPC_In_Decl_Part. Capture
+ the pragma name in Nam.
+ (Process_PPCs): Removed.
+ * sem_ch6.ads (Analyze_Subprogram_Body_Contract): New routine.
+ (Analyze_Subprogram_Contract): Update the comment on usage.
+ * sem_ch13.adb (Analyze_Aspect_Specifications): Add null
+ implementations for aspects Refined_Depends and Refined_Global.
+ (Check_Aspect_At_Freeze_Point): Aspects Refined_Depends and
+ Refined_Global do not need to be checked at the freeze point.
+ * sem_prag.adb: Add entries in table Sig_Flags
+ for pragmas Refined_Depends and Refined_Global.
+ (Analyze_Contract_Cases_In_Decl_Part): Add local
+ variable Restore. Use Restore to pop the scope.
+ (Analyze_Depends_In_Decl_Part): Add local variable Restore. Use
+ Restore to pop the scope.
+ (Analyze_Global_In_Decl_List): Add local variable Restore. Use Restore
+ to pop the scope.
+ (Analyze_PPC_In_Decl_Part): Renamed to
+ Analyze_Pre_Post_Condition_In_Decl_Part.
+ (Analyze_Pragma):
+ Add null implementations for pragmas Refined_Depends and
+ Refined_Global. Refined_Pre and Refined_Post are now
+ handled by routine Analyze_Refined_Pre_Post_Condition
+ exclusively.
+ (Analyze_Refined_Depends_In_Decl_Part): New
+ null routine.
+ (Analyze_Refined_Global_In_Decl_Part):
+ New null routine.
+ (Analyze_Refined_Pre_Post):
+ Renamed to Analyze_Refined_Pre_Post_Condition.
+ (Analyze_Refined_Pre_Post_Condition): Analyze the boolean
+ expression.
+ (Check_Precondition_Postcondition): Update the call
+ to Analyze_PPC_In_Decl_Part.
+ * sem_prag.ads: Add entries in table
+ Pragma_On_Body_Or_Stub_OK for pragmas Refined_Depends
+ and Refined_Global.
+ (Analyze_PPC_In_Decl_Part): Renamed
+ to Analyze_Pre_Post_Condition_In_Decl_Part. Update the
+ comment on usage.
+ (Analyze_Refined_Depends_In_Decl_Part): New routine.
+ (Analyze_Refined_Global_In_Decl_Part): New routine.
+ (Analyze_Test_Case_In_Decl_Part): Update the comment on usage.
+ * sem_util.adb (Add_Contract_Item): Rename formal Item to Prag
+ and update all occurrences. Subprogram body contracts can now
+ contain pragmas Refined_Depends and Refined_Global.
+ * sem_util.ads (Add_Contract_Item): Rename formal Item to
+ Prag. Update the comment on usage.
+ * sinfo.ads: Update the comment on structure and usage of
+ N_Contract.
+ * snames.ads-tmpl: Add new predefined names for Refined_Depends
+ and Refined_Global. Add entries in table Pragma_Id for
+ Refined_Depends and Refined_Global.
+
+2013-10-10 Robert Dewar <dewar@adacore.com>
+
+ * types.ads: Minor reformatting.
+
2013-10-10 Thomas Quinot <quinot@adacore.com>
* s-taprop-posix.adb: Add missing comment.
Aspect_Pure_05 => Aspect_Pure_05,
Aspect_Pure_12 => Aspect_Pure_12,
Aspect_Pure_Function => Aspect_Pure_Function,
+ Aspect_Refined_Depends => Aspect_Refined_Depends,
+ Aspect_Refined_Global => Aspect_Refined_Global,
Aspect_Refined_Post => Aspect_Refined_Post,
Aspect_Refined_Pre => Aspect_Refined_Pre,
Aspect_Remote_Access_Type => Aspect_Remote_Access_Type,
Aspect_Predicate, -- GNAT
Aspect_Priority,
Aspect_Read,
+ Aspect_Refined_Depends, -- GNAT
+ Aspect_Refined_Global, -- GNAT
Aspect_Refined_Post, -- GNAT
Aspect_Refined_Pre, -- GNAT
Aspect_Relative_Deadline,
Aspect_Predicate => Expression,
Aspect_Priority => Expression,
Aspect_Read => Name,
+ Aspect_Refined_Depends => Expression,
+ Aspect_Refined_Global => Expression,
Aspect_Refined_Post => Expression,
Aspect_Refined_Pre => Expression,
Aspect_Relative_Deadline => Expression,
Aspect_Pure_12 => Name_Pure_12,
Aspect_Pure_Function => Name_Pure_Function,
Aspect_Read => Name_Read,
+ Aspect_Refined_Depends => Name_Refined_Depends,
+ Aspect_Refined_Global => Name_Refined_Global,
Aspect_Refined_Post => Name_Refined_Post,
Aspect_Refined_Pre => Name_Refined_Pre,
Aspect_Relative_Deadline => Name_Relative_Deadline,
Aspect_Pure_12 => Always_Delay,
Aspect_Pure_Function => Always_Delay,
Aspect_Read => Always_Delay,
+ Aspect_Refined_Depends => Always_Delay,
+ Aspect_Refined_Global => Always_Delay,
Aspect_Relative_Deadline => Always_Delay,
Aspect_Remote_Access_Type => Always_Delay,
Aspect_Remote_Call_Interface => Always_Delay,
-- Sem_Prag if the aspects below are implemented by a pragma.
Aspect_On_Body_Or_Stub_OK : constant array (Aspect_Id) of Boolean :=
- (Aspect_Refined_Post => True,
+ (Aspect_Refined_Depends => True,
+ Aspect_Refined_Global => True,
+ Aspect_Refined_Post => True,
Aspect_Refined_Pre => True,
Aspect_SPARK_Mode => True,
Aspect_Warnings => True,
function Contract (Id : E) return N is
begin
pragma Assert
- (Ekind_In (Id, E_Entry, E_Entry_Family)
+ (Ekind_In (Id, E_Entry, E_Entry_Family, E_Subprogram_Body)
or else Is_Subprogram (Id)
or else Is_Generic_Subprogram (Id));
return Node24 (Id);
procedure Set_Contract (Id : E; V : N) is
begin
pragma Assert
- (Ekind_In (Id, E_Entry, E_Entry_Family, E_Void)
+ (Ekind_In (Id, E_Entry, E_Entry_Family, E_Subprogram_Body, E_Void)
or else Is_Subprogram (Id)
or else Is_Generic_Subprogram (Id));
Set_Node24 (Id, V);
when E_Entry |
E_Entry_Family |
+ E_Subprogram_Body |
Subprogram_Kind |
Generic_Subprogram_Kind =>
Write_Str ("Contract");
+ -- The Subprogram_Kind and Generic_Subrpogram_Kind entries
+ -- here are odd, since the assertions for [Set_]Contract do not
+ -- allow these possibilities ???
+
when others =>
Write_Str ("Field24???");
end case;
end if;
end Expand_Simple_Function_Return;
+ --------------------------------
+ -- Expand_Subprogram_Contract --
+ --------------------------------
+
+ procedure Expand_Subprogram_Contract
+ (N : Node_Id;
+ Spec_Id : Entity_Id;
+ Body_Id : Entity_Id)
+ is
+ procedure Add_Invariant_And_Predicate_Checks
+ (Subp_Id : Entity_Id;
+ Stmts : in out List_Id;
+ Result : out Node_Id);
+ -- Process the result of function Subp_Id (if applicable) and all its
+ -- formals. Add invariant and predicate checks where applicable. The
+ -- routine appends all the checks to list Stmts. If Subp_Id denotes a
+ -- function, Result contains the entity of parameter _Result, to be
+ -- used in the creation of procedure _Postconditions.
+
+ procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id);
+ -- Append a node to a list. If there is no list, create a new one. When
+ -- the item denotes a pragma, it is added to the list only when it is
+ -- enabled.
+
+ procedure Build_Postconditions_Procedure
+ (Subp_Id : Entity_Id;
+ Stmts : List_Id;
+ Result : Entity_Id);
+ -- Create the body of procedure _Postconditions which handles various
+ -- assertion actions on exit from subprogram Subp_Id. Stmts is the list
+ -- of statements to be checked on exit. Parameter Result is the entity
+ -- of parameter _Result when Subp_Id denotes a function.
+
+ function Build_Pragma_Check_Equivalent
+ (Prag : Node_Id;
+ Subp_Id : Entity_Id := Empty;
+ Inher_Id : Entity_Id := Empty) return Node_Id;
+ -- Transform a [refined] pre- or postcondition denoted by Prag into an
+ -- equivalent pragma Check. When the pre- or postcondition is inherited,
+ -- the routine corrects the references of all formals of Inher_Id to
+ -- point to the formals of Subp_Id.
+
+ procedure Collect_Body_Postconditions (Stmts : in out List_Id);
+ -- Process all postconditions found in the declarations of the body. The
+ -- routine appends the pragma Check equivalents to list Stmts.
+
+ procedure Collect_Spec_Postconditions
+ (Subp_Id : Entity_Id;
+ Stmts : in out List_Id);
+ -- Process all [inherited] postconditions of subprogram spec Subp_Id.
+ -- The routine appends the pragma Check equivalents to list Stmts.
+
+ procedure Collect_Spec_Preconditions (Subp_Id : Entity_Id);
+ -- Process all [inherited] preconditions of subprogram spec Subp_Id. The
+ -- routine prepends the pragma Check equivalents to the declarations of
+ -- the body.
+
+ procedure Prepend_To_Declarations (Item : Node_Id);
+ -- Prepend a single item to the declarations of the subprogram body
+
+ procedure Process_Contract_Cases
+ (Subp_Id : Entity_Id;
+ Stmts : in out List_Id);
+ -- Process pragma Contract_Cases of subprogram spec Subp_Id. The routine
+ -- appends the expanded code to list Stmts.
+
+ ----------------------------------------
+ -- Add_Invariant_And_Predicate_Checks --
+ ----------------------------------------
+
+ procedure Add_Invariant_And_Predicate_Checks
+ (Subp_Id : Entity_Id;
+ Stmts : in out List_Id;
+ Result : out Node_Id)
+ is
+ procedure Add_Invariant_Access_Checks (Id : Entity_Id);
+ -- Id denotes the return value of a function or a formal parameter.
+ -- Add an invariant check if the type of Id is access to a type with
+ -- invariants. The routine appends the generated code to Stmts.
+
+ function Invariant_Checks_OK (Typ : Entity_Id) return Boolean;
+ -- Determine whether type Typ can benefit from invariant checks. To
+ -- qualify, the type must have a non-null invariant procedure and
+ -- subprogram Subp_Id must appear visible from the point of view of
+ -- the type.
+
+ function Predicate_Checks_OK (Typ : Entity_Id) return Boolean;
+ -- Determine whether type Typ can benefit from predicate checks. To
+ -- qualify, the type must have at least one checked predicate.
+
+ ---------------------------------
+ -- Add_Invariant_Access_Checks --
+ ---------------------------------
+
+ procedure Add_Invariant_Access_Checks (Id : Entity_Id) is
+ Loc : constant Source_Ptr := Sloc (N);
+ Ref : Node_Id;
+ Typ : Entity_Id;
+
+ begin
+ Typ := Etype (Id);
+
+ if Is_Access_Type (Typ) and then not Is_Access_Constant (Typ) then
+ Typ := Designated_Type (Typ);
+
+ if Invariant_Checks_OK (Typ) then
+ Ref :=
+ Make_Explicit_Dereference (Loc,
+ Prefix => New_Occurrence_Of (Id, Loc));
+ Set_Etype (Ref, Typ);
+
+ -- Generate:
+ -- if <Id> /= null then
+ -- <invariant_call (<Ref>)>
+ -- end if;
+
+ Append_Enabled_Item
+ (Item =>
+ Make_If_Statement (Loc,
+ Condition =>
+ Make_Op_Ne (Loc,
+ Left_Opnd => New_Occurrence_Of (Id, Loc),
+ Right_Opnd => Make_Null (Loc)),
+ Then_Statements => New_List (
+ Make_Invariant_Call (Ref))),
+ List => Stmts);
+ end if;
+ end if;
+ end Add_Invariant_Access_Checks;
+
+ -------------------------
+ -- Invariant_Checks_OK --
+ -------------------------
+
+ function Invariant_Checks_OK (Typ : Entity_Id) return Boolean is
+ function Has_Null_Body (Proc_Id : Entity_Id) return Boolean;
+ -- Determine whether the body of procedure Proc_Id contains a sole
+ -- null statement, possibly followed by an optional return.
+
+ function Has_Public_Visibility_Of_Subprogram return Boolean;
+ -- Determine whether type Typ has public visibility of subprogram
+ -- Subp_Id.
+
+ -------------------
+ -- Has_Null_Body --
+ -------------------
+
+ function Has_Null_Body (Proc_Id : Entity_Id) return Boolean is
+ Body_Id : Entity_Id;
+ Decl : Node_Id;
+ Spec : Node_Id;
+ Stmt1 : Node_Id;
+ Stmt2 : Node_Id;
+
+ begin
+ Spec := Parent (Proc_Id);
+ Decl := Parent (Spec);
+
+ -- Retrieve the entity of the invariant procedure body
+
+ if Nkind (Spec) = N_Procedure_Specification
+ and then Nkind (Decl) = N_Subprogram_Declaration
+ then
+ Body_Id := Corresponding_Body (Decl);
+
+ -- The body acts as a spec
+
+ else
+ Body_Id := Proc_Id;
+ end if;
+
+ -- The body will be generated later
+
+ if No (Body_Id) then
+ return False;
+ end if;
+
+ Spec := Parent (Body_Id);
+ Decl := Parent (Spec);
+
+ pragma Assert
+ (Nkind (Spec) = N_Procedure_Specification
+ and then Nkind (Decl) = N_Subprogram_Body);
+
+ Stmt1 := First (Statements (Handled_Statement_Sequence (Decl)));
+
+ -- Look for a null statement followed by an optional return
+ -- statement.
+
+ if Nkind (Stmt1) = N_Null_Statement then
+ Stmt2 := Next (Stmt1);
+
+ if Present (Stmt2) then
+ return Nkind (Stmt2) = N_Simple_Return_Statement;
+ else
+ return True;
+ end if;
+ end if;
+
+ return False;
+ end Has_Null_Body;
+
+ -----------------------------------------
+ -- Has_Public_Visibility_Of_Subprogram --
+ -----------------------------------------
+
+ function Has_Public_Visibility_Of_Subprogram return Boolean is
+ Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
+ Vis_Decls : constant List_Id :=
+ Visible_Declarations (Specification
+ (Unit_Declaration_Node (Scope (Typ))));
+ begin
+ -- An Initialization procedure must be considered visible even
+ -- though it is internally generated.
+
+ if Is_Init_Proc (Defining_Entity (Subp_Decl)) then
+ return True;
+
+ -- Internally generated code is never publicly visible except
+ -- for a subprogram that is the implementation of an expression
+ -- function. In that case the visibility is determined by the
+ -- last check.
+
+ elsif not Comes_From_Source (Subp_Decl)
+ and then
+ (Nkind (Original_Node (Subp_Decl)) /= N_Expression_Function
+ or else not
+ Comes_From_Source (Defining_Entity (Subp_Decl)))
+ then
+ return False;
+
+ -- Determine whether the subprogram is declared in the visible
+ -- declarations of the package containing the type.
+
+ else
+ return List_Containing (Subp_Decl) = Vis_Decls;
+ end if;
+ end Has_Public_Visibility_Of_Subprogram;
+
+ -- Start of processing for Invariant_Checks_OK
+
+ begin
+ return
+ Has_Invariants (Typ)
+ and then Present (Invariant_Procedure (Typ))
+ and then not Has_Null_Body (Invariant_Procedure (Typ))
+ and then Has_Public_Visibility_Of_Subprogram;
+ end Invariant_Checks_OK;
+
+ -------------------------
+ -- Predicate_Checks_OK --
+ -------------------------
+
+ function Predicate_Checks_OK (Typ : Entity_Id) return Boolean is
+ function Has_Checked_Predicate return Boolean;
+ -- Determine whether type Typ has or inherits at least one
+ -- predicate aspect or pragma, for which the applicable policy is
+ -- Checked.
+
+ ---------------------------
+ -- Has_Checked_Predicate --
+ ---------------------------
+
+ function Has_Checked_Predicate return Boolean is
+ Anc : Entity_Id;
+ Pred : Node_Id;
+
+ begin
+ -- Climb the ancestor type chain staring from the input. This
+ -- is done because the input type may lack aspect/pragma
+ -- predicate and simply inherit those from its ancestor.
+
+ -- Note that predicate pragmas include all three cases of
+ -- predicate aspects (Predicate, Dynamic_Predicate,
+ -- Static_Predicate), so this routine checks for all three
+ -- cases.
+
+ Anc := Typ;
+ while Present (Anc) loop
+ Pred := Get_Pragma (Anc, Pragma_Predicate);
+
+ if Present (Pred) and then not Is_Ignored (Pred) then
+ return True;
+ end if;
+
+ Anc := Nearest_Ancestor (Anc);
+ end loop;
+
+ return False;
+ end Has_Checked_Predicate;
+
+ -- Start of processing for Predicate_Checks_OK
+
+ begin
+ return
+ Has_Predicates (Typ)
+ and then Present (Predicate_Function (Typ))
+ and then Has_Checked_Predicate;
+ end Predicate_Checks_OK;
+
+ -- Local variables
+
+ Loc : constant Source_Ptr := Sloc (N);
+ Formal : Entity_Id;
+ Typ : Entity_Id;
+
+ -- Start of processing for Add_Invariant_And_Predicate_Checks
+
+ begin
+ Result := Empty;
+
+ -- Do not generate any checks if no code is being generated
+
+ if not Expander_Active then
+ return;
+ end if;
+
+ -- Process the result of a function
+
+ if Ekind_In (Subp_Id, E_Function, E_Generic_Function) then
+ Typ := Etype (Subp_Id);
+
+ -- Generate _Result which is used in procedure _Postconditions to
+ -- verify the return value.
+
+ Result := Make_Defining_Identifier (Loc, Name_uResult);
+ Set_Etype (Result, Typ);
+
+ -- Add an invariant check when the return type has invariants and
+ -- the related function is visible to the outside.
+
+ if Invariant_Checks_OK (Typ) then
+ Append_Enabled_Item
+ (Item =>
+ Make_Invariant_Call (New_Occurrence_Of (Result, Loc)),
+ List => Stmts);
+ end if;
+
+ -- Add an invariant check when the return type is an access to a
+ -- type with invariants.
+
+ Add_Invariant_Access_Checks (Result);
+ end if;
+
+ -- Add invariant and predicates for all formals that qualify
+
+ Formal := First_Formal (Subp_Id);
+ while Present (Formal) loop
+ Typ := Etype (Formal);
+
+ if Ekind (Formal) /= E_In_Parameter
+ or else Is_Access_Type (Typ)
+ then
+ if Invariant_Checks_OK (Typ) then
+ Append_Enabled_Item
+ (Item =>
+ Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)),
+ List => Stmts);
+ end if;
+
+ Add_Invariant_Access_Checks (Formal);
+
+ if Predicate_Checks_OK (Typ) then
+ Append_Enabled_Item
+ (Item =>
+ Make_Predicate_Check
+ (Typ, New_Reference_To (Formal, Loc)),
+ List => Stmts);
+ end if;
+ end if;
+
+ Next_Formal (Formal);
+ end loop;
+ end Add_Invariant_And_Predicate_Checks;
+
+ -------------------------
+ -- Append_Enabled_Item --
+ -------------------------
+
+ procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id) is
+ begin
+ -- Do not chain ignored or disabled pragmas
+
+ if Nkind (Item) = N_Pragma
+ and then (Is_Ignored (Item) or else Is_Disabled (Item))
+ then
+ null;
+
+ -- Add the item
+
+ else
+ if No (List) then
+ List := New_List;
+ end if;
+
+ Append (Item, List);
+ end if;
+ end Append_Enabled_Item;
+
+ ------------------------------------
+ -- Build_Postconditions_Procedure --
+ ------------------------------------
+
+ procedure Build_Postconditions_Procedure
+ (Subp_Id : Entity_Id;
+ Stmts : List_Id;
+ Result : Entity_Id)
+ is
+ procedure Insert_After_Last_Declaration (Stmt : Node_Id);
+ -- Insert node Stmt after the last declaration of the subprogram body
+
+ -----------------------------------
+ -- Insert_After_Last_Declaration --
+ -----------------------------------
+
+ procedure Insert_After_Last_Declaration (Stmt : Node_Id) is
+ Decls : List_Id := Declarations (N);
+
+ begin
+ -- Ensure that the body has a declaration list
+
+ if No (Decls) then
+ Decls := New_List;
+ Set_Declarations (N, Decls);
+ end if;
+
+ Append_To (Decls, Stmt);
+ end Insert_After_Last_Declaration;
+
+ -- Local variables
+
+ Loc : constant Source_Ptr := Sloc (N);
+ Params : List_Id := No_List;
+ Proc_Id : Entity_Id;
+
+ -- Start of processing for Build_Postconditions_Procedure
+
+ begin
+ -- Do not create the routine if no code is being generated
+
+ if not Expander_Active then
+ return;
+
+ -- Nothing to do if there are no actions to check on exit
+
+ elsif No (Stmts) then
+ return;
+ end if;
+
+ Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions);
+
+ -- The related subprogram is a function, create the specification of
+ -- parameter _Result.
+
+ if Present (Result) then
+ Params := New_List (
+ Make_Parameter_Specification (Loc,
+ Defining_Identifier => Result,
+ Parameter_Type =>
+ New_Reference_To (Etype (Result), Loc)));
+ end if;
+
+ -- Insert _Postconditions after the last declaration of the body.
+ -- This ensures that the body will not cause any premature freezing
+ -- as it may mention types:
+
+ -- procedure Proc (Obj : Array_Typ) is
+ -- procedure _postconditions is
+ -- begin
+ -- ... Obj ...
+ -- end _postconditions;
+
+ -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1));
+ -- begin
+
+ -- In the example above, Obj is of type T but the incorrect placement
+ -- of _Postconditions will cause a crash in gigi due to an out of
+ -- order reference. The body of _Postconditions must be placed after
+ -- the declaration of Temp to preserve correct visibility.
+
+ Insert_After_Last_Declaration (
+ Make_Subprogram_Body (Loc,
+ Specification =>
+ Make_Procedure_Specification (Loc,
+ Defining_Unit_Name => Proc_Id,
+ Parameter_Specifications => Params),
+
+ Declarations => Empty_List,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc, Stmts)));
+
+ -- Set the attributes of the related subprogram to capture the
+ -- generated procedure.
+
+ if Ekind_In (Subp_Id, E_Generic_Procedure, E_Procedure) then
+ Set_Postcondition_Proc (Subp_Id, Proc_Id);
+ end if;
+
+ Set_Has_Postconditions (Subp_Id);
+ end Build_Postconditions_Procedure;
+
+ -----------------------------------
+ -- Build_Pragma_Check_Equivalent --
+ -----------------------------------
+
+ function Build_Pragma_Check_Equivalent
+ (Prag : Node_Id;
+ Subp_Id : Entity_Id := Empty;
+ Inher_Id : Entity_Id := Empty) return Node_Id
+ is
+ Loc : constant Source_Ptr := Sloc (Prag);
+ Prag_Nam : constant Name_Id := Pragma_Name (Prag);
+ Check_Prag : Node_Id;
+ Formals_Map : Elist_Id;
+ Inher_Formal : Entity_Id;
+ Msg_Arg : Node_Id;
+ Nam : Name_Id;
+ Subp_Formal : Entity_Id;
+
+ begin
+ Formals_Map := No_Elist;
+
+ -- When the pre- or postcondition is inherited, map the formals of
+ -- the inherited subprogram to those of the current subprogram.
+
+ if Present (Inher_Id) then
+ pragma Assert (Present (Subp_Id));
+
+ Formals_Map := New_Elmt_List;
+
+ -- Create a relation <inherited formal> => <subprogram formal>
+
+ Inher_Formal := First_Formal (Inher_Id);
+ Subp_Formal := First_Formal (Subp_Id);
+ while Present (Inher_Formal) and then Present (Subp_Formal) loop
+ Append_Elmt (Inher_Formal, Formals_Map);
+ Append_Elmt (Subp_Formal, Formals_Map);
+
+ Next_Formal (Inher_Formal);
+ Next_Formal (Subp_Formal);
+ end loop;
+ end if;
+
+ -- Copy the original pragma while performing substitutions (if
+ -- applicable).
+
+ Check_Prag :=
+ New_Copy_Tree
+ (Source => Prag,
+ Map => Formals_Map,
+ New_Scope => Current_Scope);
+
+ -- Mark the pragma as being internally generated and reset the
+ -- Analyzed flag.
+
+ Set_Comes_From_Source (Check_Prag, False);
+ Set_Analyzed (Check_Prag, False);
+
+ -- For a postcondition pragma within a generic, preserve the pragma
+ -- for later expansion. This is also used when an error was detected,
+ -- thus setting Expander_Active to False.
+
+ if Prag_Nam = Name_Postcondition and then not Expander_Active then
+ return Check_Prag;
+ end if;
+
+ if Present (Corresponding_Aspect (Prag)) then
+ Nam := Chars (Identifier (Corresponding_Aspect (Prag)));
+ else
+ Nam := Prag_Nam;
+ end if;
+
+ -- Convert the copy into pragma Check by correcting the name and
+ -- adding a check_kind argument.
+
+ Set_Pragma_Identifier
+ (Check_Prag, Make_Identifier (Loc, Name_Check));
+
+ Prepend_To (Pragma_Argument_Associations (Check_Prag),
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Make_Identifier (Loc, Nam)));
+
+ -- Update the error message when the pragma is inherited
+
+ if Present (Inher_Id) then
+ Msg_Arg := Last (Pragma_Argument_Associations (Check_Prag));
+
+ if Chars (Msg_Arg) = Name_Message then
+ String_To_Name_Buffer (Strval (Expression (Msg_Arg)));
+
+ -- Insert "inherited" to improve the error message
+
+ if Name_Buffer (1 .. 8) = "failed p" then
+ Insert_Str_In_Name_Buffer ("inherited ", 8);
+ Set_Strval (Expression (Msg_Arg), String_From_Name_Buffer);
+ end if;
+ end if;
+ end if;
+
+ return Check_Prag;
+ end Build_Pragma_Check_Equivalent;
+
+ ---------------------------------
+ -- Collect_Body_Postconditions --
+ ---------------------------------
+
+ procedure Collect_Body_Postconditions (Stmts : in out List_Id) is
+ procedure Collect_Body_Postconditions_Of_Kind (Post_Nam : Name_Id);
+ -- Process postconditions of a particular kind denoted by Post_Nam
+
+ -----------------------------------------
+ -- Collect_Body_Postconditions_Of_Kind --
+ -----------------------------------------
+
+ procedure Collect_Body_Postconditions_Of_Kind (Post_Nam : Name_Id) is
+ Check_Prag : Node_Id;
+ Decl : Node_Id;
+
+ begin
+ pragma Assert (Nam_In (Post_Nam, Name_Postcondition,
+ Name_Refined_Post));
+
+ -- Inspect the declarations of the subprogram body looking for a
+ -- pragma that matches the desired name.
+
+ Decl := First (Declarations (N));
+ while Present (Decl) loop
+ if Nkind (Decl) = N_Pragma then
+ if Pragma_Name (Decl) = Post_Nam then
+ Analyze (Decl);
+ Check_Prag := Build_Pragma_Check_Equivalent (Decl);
+
+ if Expander_Active then
+ Append_Enabled_Item
+ (Item => Check_Prag,
+ List => Stmts);
+
+ -- When analyzing a generic unit, save the pragma for
+ -- later.
+
+ else
+ Prepend_To_Declarations (Check_Prag);
+ end if;
+ end if;
+
+ -- Skip internally generated code
+
+ elsif not Comes_From_Source (Decl) then
+ null;
+
+ -- Postconditions in bodies are usually grouped at the top of
+ -- the declarations. There is no point in inspecting the whole
+ -- source list.
+
+ else
+ exit;
+ end if;
+
+ Next (Decl);
+ end loop;
+ end Collect_Body_Postconditions_Of_Kind;
+
+ -- Start of processing for Collect_Body_Postconditions
+
+ begin
+ Collect_Body_Postconditions_Of_Kind (Name_Refined_Post);
+ Collect_Body_Postconditions_Of_Kind (Name_Postcondition);
+ end Collect_Body_Postconditions;
+
+ ---------------------------------
+ -- Collect_Spec_Postconditions --
+ ---------------------------------
+
+ procedure Collect_Spec_Postconditions
+ (Subp_Id : Entity_Id;
+ Stmts : in out List_Id)
+ is
+ Inher_Subps : constant Subprogram_List :=
+ Inherited_Subprograms (Subp_Id);
+ Check_Prag : Node_Id;
+ Prag : Node_Id;
+ Inher_Subp_Id : Entity_Id;
+
+ begin
+ -- Process the contract of the spec
+
+ Prag := Pre_Post_Conditions (Contract (Subp_Id));
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Postcondition then
+ Check_Prag := Build_Pragma_Check_Equivalent (Prag);
+
+ if Expander_Active then
+ Append_Enabled_Item
+ (Item => Check_Prag,
+ List => Stmts);
+
+ -- When analyzing a generic unit, save the pragma for later
+
+ else
+ Prepend_To_Declarations (Check_Prag);
+ end if;
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+
+ -- Process the contracts of all inherited subprograms, looking for
+ -- class-wide postconditions.
+
+ for Index in Inher_Subps'Range loop
+ Inher_Subp_Id := Inher_Subps (Index);
+
+ Prag := Pre_Post_Conditions (Contract (Inher_Subp_Id));
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Postcondition
+ and then Class_Present (Prag)
+ then
+ Check_Prag :=
+ Build_Pragma_Check_Equivalent
+ (Prag => Prag,
+ Subp_Id => Subp_Id,
+ Inher_Id => Inher_Subp_Id);
+
+ if Expander_Active then
+ Append_Enabled_Item
+ (Item => Check_Prag,
+ List => Stmts);
+
+ -- When analyzing a generic unit, save the pragma for later
+
+ else
+ Prepend_To_Declarations (Check_Prag);
+ end if;
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end loop;
+ end Collect_Spec_Postconditions;
+
+ --------------------------------
+ -- Collect_Spec_Preconditions --
+ --------------------------------
+
+ procedure Collect_Spec_Preconditions (Subp_Id : Entity_Id) is
+ procedure Merge_Preconditions (From : Node_Id; Into : Node_Id);
+ -- Merge two class-wide preconditions by "or else"-ing them. The
+ -- changes are accumulated in parameter Into. Update the error
+ -- message of Into.
+
+ -------------------------
+ -- Merge_Preconditions --
+ -------------------------
+
+ procedure Merge_Preconditions (From : Node_Id; Into : Node_Id) is
+ function Expression_Arg (Prag : Node_Id) return Node_Id;
+ -- Return the boolean expression argument of a precondition while
+ -- updating its parenteses count for the subsequent merge.
+
+ function Message_Arg (Prag : Node_Id) return Node_Id;
+ -- Return the message argument of a precondition
+
+ --------------------
+ -- Expression_Arg --
+ --------------------
+
+ function Expression_Arg (Prag : Node_Id) return Node_Id is
+ Args : constant List_Id := Pragma_Argument_Associations (Prag);
+ Arg : constant Node_Id := Get_Pragma_Arg (Next (First (Args)));
+
+ begin
+ if Paren_Count (Arg) = 0 then
+ Set_Paren_Count (Arg, 1);
+ end if;
+
+ return Arg;
+ end Expression_Arg;
+
+ -----------------
+ -- Message_Arg --
+ -----------------
+
+ function Message_Arg (Prag : Node_Id) return Node_Id is
+ Args : constant List_Id := Pragma_Argument_Associations (Prag);
+ begin
+ return Get_Pragma_Arg (Last (Args));
+ end Message_Arg;
+
+ -- Local variables
+
+ From_Expr : constant Node_Id := Expression_Arg (From);
+ From_Msg : constant Node_Id := Message_Arg (From);
+ Into_Expr : constant Node_Id := Expression_Arg (Into);
+ Into_Msg : constant Node_Id := Message_Arg (Into);
+ Loc : constant Source_Ptr := Sloc (Into);
+
+ -- Start of processing for Merge_Preconditions
+
+ begin
+ -- Merge the two preconditions by "or else"-ing them
+
+ Rewrite (Into_Expr,
+ Make_Or_Else (Loc,
+ Right_Opnd => Relocate_Node (Into_Expr),
+ Left_Opnd => From_Expr));
+
+ -- Merge the two error messages to produce a single message of the
+ -- form:
+
+ -- failed precondition from ...
+ -- also failed inherited precondition from ...
+
+ if not Exception_Locations_Suppressed then
+ Start_String (Strval (Into_Msg));
+ Store_String_Char (ASCII.LF);
+ Store_String_Chars (" also ");
+ Store_String_Chars (Strval (From_Msg));
+
+ Set_Strval (Into_Msg, End_String);
+ end if;
+ end Merge_Preconditions;
+
+ -- Local variables
+
+ Inher_Subps : constant Subprogram_List :=
+ Inherited_Subprograms (Subp_Id);
+ Check_Prag : Node_Id;
+ Class_Pre : Node_Id := Empty;
+ Inher_Subp_Id : Entity_Id;
+ Prag : Node_Id;
+
+ -- Start of processing for Collect_Spec_Preconditions
+
+ begin
+ -- Process the contract of the spec
+
+ Prag := Pre_Post_Conditions (Contract (Subp_Id));
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Precondition then
+ Check_Prag := Build_Pragma_Check_Equivalent (Prag);
+
+ -- Save the sole class-wide precondition (if any) for the next
+ -- step where it will be merged with inherited preconditions.
+
+ if Class_Present (Prag) then
+ Class_Pre := Check_Prag;
+
+ -- Accumulate the corresponding Check pragmas to the top of the
+ -- declarations. Prepending the items ensures that they will
+ -- be evaluated in their original order.
+
+ else
+ Prepend_To_Declarations (Check_Prag);
+ end if;
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+
+ -- Process the contracts of all inherited subprograms, looking for
+ -- class-wide preconditions.
+
+ for Index in Inher_Subps'Range loop
+ Inher_Subp_Id := Inher_Subps (Index);
+
+ Prag := Pre_Post_Conditions (Contract (Inher_Subp_Id));
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Precondition
+ and then Class_Present (Prag)
+ then
+ Check_Prag :=
+ Build_Pragma_Check_Equivalent
+ (Prag => Prag,
+ Subp_Id => Subp_Id,
+ Inher_Id => Inher_Subp_Id);
+
+ -- The spec or an inherited subprogram already yielded a
+ -- class-wide precondition. Merge the existing precondition
+ -- with the current one using "or else".
+
+ if Present (Class_Pre) then
+ Merge_Preconditions (Check_Prag, Class_Pre);
+ else
+ Class_Pre := Check_Prag;
+ end if;
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end loop;
+
+ -- Add the merged class-wide preconditions (if any)
+
+ if Present (Class_Pre) then
+ Prepend_To_Declarations (Class_Pre);
+ end if;
+ end Collect_Spec_Preconditions;
+
+ -----------------------------
+ -- Prepend_To_Declarations --
+ -----------------------------
+
+ procedure Prepend_To_Declarations (Item : Node_Id) is
+ Decls : List_Id := Declarations (N);
+
+ begin
+ -- Ensure that the body has a declarative list
+
+ if No (Decls) then
+ Decls := New_List;
+ Set_Declarations (N, Decls);
+ end if;
+
+ Prepend_To (Decls, Item);
+ end Prepend_To_Declarations;
+
+ ----------------------------
+ -- Process_Contract_Cases --
+ ----------------------------
+
+ procedure Process_Contract_Cases
+ (Subp_Id : Entity_Id;
+ Stmts : in out List_Id)
+ is
+ Prag : Node_Id;
+
+ begin
+ -- Do not build the Contract_Cases circuitry if no code is being
+ -- generated.
+
+ if not Expander_Active then
+ null;
+ end if;
+
+ Prag := Contract_Test_Cases (Contract (Subp_Id));
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Contract_Cases then
+ Expand_Contract_Cases
+ (CCs => Prag,
+ Subp_Id => Subp_Id,
+ Decls => Declarations (N),
+ Stmts => Stmts);
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end Process_Contract_Cases;
+
+ -- Local variables
+
+ Post_Stmts : List_Id := No_List;
+ Result : Entity_Id;
+ Subp_Id : Entity_Id;
+
+ -- Start of processing for Expand_Subprogram_Contract
+
+ begin
+ if Present (Spec_Id) then
+ Subp_Id := Spec_Id;
+ else
+ Subp_Id := Body_Id;
+ end if;
+
+ -- Do not process a predicate function as its body will end up with a
+ -- recursive call to itself and blow up the stack.
+
+ if Ekind (Subp_Id) = E_Function
+ and then Is_Predicate_Function (Subp_Id)
+ then
+ return;
+
+ -- Do not process TSS subprograms
+
+ elsif Get_TSS_Name (Subp_Id) /= TSS_Null then
+ return;
+ end if;
+
+ -- The expansion of a subprogram contract involves the relocation of
+ -- various contract assertions to the declarations of the body in a
+ -- particular order. The order is as follows:
+
+ -- function Example (...) return ... is
+ -- procedure _Postconditions (...) is
+ -- begin
+ -- <refined postconditions from body>
+ -- <postconditions from body>
+ -- <postconditions from spec>
+ -- <inherited postconditions>
+ -- <contract cases>
+ -- <invariant check of function result (if applicable)>
+ -- <invariant and predicate checks of parameters>
+ -- end _Postconditions;
+
+ -- <inherited preconditions>
+ -- <preconditions from spec>
+ -- <preconditions from body>
+ -- <refined preconditions from body>
+
+ -- <source declarations>
+ -- begin
+ -- <source statements>
+
+ -- _Preconditions (Result);
+ -- return Result;
+ -- end Example;
+
+ -- Routine _Postconditions holds all contract assertions that must be
+ -- verified on exit from the related routine.
+
+ -- Collect all [inherited] preconditions from the spec, transform them
+ -- into Check pragmas and add them to the declarations of the body in
+ -- the order outlined above.
+
+ if Present (Spec_Id) then
+ Collect_Spec_Preconditions (Spec_Id);
+ end if;
+
+ -- Transform all [refined] postconditions of the body into Check
+ -- pragmas. The resulting pragmas are accumulated in list Post_Stmts.
+
+ Collect_Body_Postconditions (Post_Stmts);
+
+ -- Transform all [inherited] postconditions from the spec into Check
+ -- pragmas. The resulting pragmas are accumulated in list Post_Stmts.
+
+ if Present (Spec_Id) then
+ Collect_Spec_Postconditions (Spec_Id, Post_Stmts);
+
+ -- Transform pragma Contract_Cases from the spec into its circuitry
+
+ Process_Contract_Cases (Spec_Id, Post_Stmts);
+ end if;
+
+ -- Apply invariant and predicate checks on the result of a function (if
+ -- applicable) and all formals. The resulting checks are accumulated in
+ -- list Post_Stmts.
+
+ Add_Invariant_And_Predicate_Checks (Subp_Id, Post_Stmts, Result);
+
+ -- Construct procedure _Postconditions
+
+ Build_Postconditions_Procedure (Subp_Id, Post_Stmts, Result);
+ end Expand_Subprogram_Contract;
+
--------------------------------
-- Is_Build_In_Place_Function --
--------------------------------
-- Subp_Id's body. All generated code is added to list Stmts. If Stmts is
-- empty, a new list is created.
+ procedure Expand_Subprogram_Contract
+ (N : Node_Id;
+ Spec_Id : Entity_Id;
+ Body_Id : Entity_Id);
+ -- Expand the contracts of a subprogram body and its correspoding spec (if
+ -- any). This routine processes all [refined] pre- and postconditions as
+ -- well as Contract_Cases, invariants and predicates. N is the body of the
+ -- subprogram. Spec_Id denotes the entity of its specification. Body_Id
+ -- denotes the entity of the subprogram body. This routine is not a "pure"
+ -- expansion mechanism as it is invoked during analysis and may perform
+ -- actions for generic subprograms or set up contract assertions for ASIS.
+
procedure Freeze_Subprogram (N : Node_Id);
-- generate the appropriate expansions related to Subprogram freeze
-- nodes (e.g. the filling of the corresponding Dispatch Table for
Pragma_Pure_12 |
Pragma_Pure_Function |
Pragma_Queuing_Policy |
+ Pragma_Refined_Depends |
+ Pragma_Refined_Global |
Pragma_Refined_Post |
Pragma_Refined_Pre |
Pragma_Relative_Deadline |
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_SPARK_Mode);
+ -- Refined_Depends
+
+ -- ??? To be implemented
+
+ when Aspect_Refined_Depends =>
+ null;
+
+ -- Refined_Global
+
+ -- ??? To be implemented
+
+ when Aspect_Refined_Global =>
+ null;
+
-- Refined_Post
when Aspect_Refined_Post =>
Aspect_Postcondition |
Aspect_Pre |
Aspect_Precondition |
+ Aspect_Refined_Depends |
+ Aspect_Refined_Global |
Aspect_Refined_Post |
Aspect_Refined_Pre |
Aspect_SPARK_Mode |
--------------------------
procedure Analyze_Declarations (L : List_Id) is
- D : Node_Id;
- Freeze_From : Entity_Id := Empty;
- Next_Node : Node_Id;
+ Decl : Node_Id;
- procedure Adjust_D;
- -- Adjust D not to include implicit label declarations, since these
+ procedure Adjust_Decl;
+ -- Adjust Decl not to include implicit label declarations, since these
-- have strange Sloc values that result in elaboration check problems.
-- (They have the sloc of the label as found in the source, and that
-- is ahead of the current declarative part).
- --------------
- -- Adjust_D --
- --------------
+ -----------------
+ -- Adjust_Decl --
+ -----------------
- procedure Adjust_D is
+ procedure Adjust_Decl is
begin
- while Present (Prev (D))
- and then Nkind (D) = N_Implicit_Label_Declaration
+ while Present (Prev (Decl))
+ and then Nkind (Decl) = N_Implicit_Label_Declaration
loop
- Prev (D);
+ Prev (Decl);
end loop;
- end Adjust_D;
+ end Adjust_Decl;
+
+ -- Local variables
+
+ Freeze_From : Entity_Id := Empty;
+ Next_Decl : Node_Id;
-- Start of processing for Analyze_Declarations
Check_Later_Vs_Basic_Declarations (L, During_Parsing => False);
end if;
- D := First (L);
- while Present (D) loop
+ Decl := First (L);
+ while Present (Decl) loop
-- Package spec cannot contain a package declaration in SPARK
- if Nkind (D) = N_Package_Declaration
+ if Nkind (Decl) = N_Package_Declaration
and then Nkind (Parent (L)) = N_Package_Specification
then
Check_SPARK_Restriction
("package specification cannot contain a package declaration",
- D);
+ Decl);
end if;
-- Complete analysis of declaration
- Analyze (D);
- Next_Node := Next (D);
+ Analyze (Decl);
+ Next_Decl := Next (Decl);
if No (Freeze_From) then
Freeze_From := First_Entity (Current_Scope);
-- be a freeze point once delayed freezing of bodies is implemented.
-- (This is needed in any case for early instantiations ???).
- if No (Next_Node) then
+ if No (Next_Decl) then
if Nkind_In (Parent (L), N_Component_List,
N_Task_Definition,
N_Protected_Definition)
Freeze_From := First_Entity (Current_Scope);
end if;
- Adjust_D;
- Freeze_All (Freeze_From, D);
+ Adjust_Decl;
+ Freeze_All (Freeze_From, Decl);
Freeze_From := Last_Entity (Current_Scope);
elsif Scope (Current_Scope) /= Standard_Standard
or else No (Private_Declarations (Parent (L)))
or else Is_Empty_List (Private_Declarations (Parent (L)))
then
- Adjust_D;
- Freeze_All (Freeze_From, D);
+ Adjust_Decl;
+ Freeze_All (Freeze_From, Decl);
Freeze_From := Last_Entity (Current_Scope);
end if;
-- care to attach the bodies at a proper place in the tree so as to
-- not cause unwanted freezing at that point.
- elsif not Analyzed (Next_Node)
- and then (Nkind_In (Next_Node, N_Subprogram_Body,
+ elsif not Analyzed (Next_Decl)
+ and then (Nkind_In (Next_Decl, N_Subprogram_Body,
N_Entry_Body,
N_Package_Body,
N_Protected_Body,
N_Task_Body)
or else
- Nkind (Next_Node) in N_Body_Stub)
+ Nkind (Next_Decl) in N_Body_Stub)
then
- Adjust_D;
- Freeze_All (Freeze_From, D);
+ Adjust_Decl;
+ Freeze_All (Freeze_From, Decl);
Freeze_From := Last_Entity (Current_Scope);
end if;
- D := Next_Node;
+ Decl := Next_Decl;
end loop;
- -- One more thing to do, we need to scan the declarations to check for
- -- any precondition/postcondition pragmas (Pre/Post aspects have by this
- -- stage been converted into corresponding pragmas). It is at this point
- -- that we analyze the expressions in such pragmas, to implement the
- -- delayed visibility requirement.
+ -- Analyze the contracts of a subprogram declaration or a body now due
+ -- to delayed visibility requirements of aspects.
- declare
- Decl : Node_Id;
- Subp_Id : Entity_Id;
+ Decl := First (L);
+ while Present (Decl) loop
+ if Nkind (Decl) = N_Subprogram_Body then
+ Analyze_Subprogram_Body_Contract
+ (Defining_Unit_Name (Specification (Decl)));
- begin
- Decl := First (L);
- while Present (Decl) loop
- if Nkind (Decl) = N_Subprogram_Declaration then
- Subp_Id := Defining_Unit_Name (Specification (Decl));
- Analyze_Subprogram_Contract (Subp_Id);
- end if;
+ elsif Nkind (Decl) = N_Subprogram_Declaration then
+ Analyze_Subprogram_Contract
+ (Defining_Unit_Name (Specification (Decl)));
+ end if;
- Next (Decl);
- end loop;
- end;
+ Next (Decl);
+ end loop;
end Analyze_Declarations;
-----------------------------------
-- Create the declaration for an inequality operator that is implicitly
-- created by a user-defined equality operator that yields a boolean.
- procedure Process_PPCs
- (N : Node_Id;
- Spec_Id : Entity_Id;
- Body_Id : Entity_Id);
- -- Called from Analyze[_Generic]_Subprogram_Body to deal with scanning post
- -- conditions for the body and assembling and inserting the _postconditions
- -- procedure. N is the node for the subprogram body and Body_Id/Spec_Id are
- -- the entities for the body and separate spec (if there is no separate
- -- spec, Spec_Id is Empty). Note that invariants and predicates may also
- -- provide postconditions, and are also handled in this procedure.
-
procedure Set_Formal_Validity (Formal_Id : Entity_Id);
-- Formal_Id is an formal parameter entity. This procedure deals with
-- setting the proper validity status for this entity, which depends on
-- Visible generic entity is callable within its own body
Set_Ekind (Gen_Id, Ekind (Body_Id));
- Set_Contract (Body_Id, Empty);
+ Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id)));
Set_Ekind (Body_Id, E_Subprogram_Body);
Set_Convention (Body_Id, Convention (Gen_Id));
Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Gen_Id));
Set_Actual_Subtypes (N, Current_Scope);
- -- Deal with preconditions and postconditions. In formal verification
- -- mode, we keep pre- and postconditions attached to entities rather
- -- than inserted in the code, in order to facilitate a distinct
- -- treatment for them.
+ -- Deal with [refined] preconditions, postconditions, Contract_Cases,
+ -- invariants and predicates associated with the body and its spec.
+ -- Note that this is not pure expansion as Expand_Subprogram_Contract
+ -- prepares the contract assertions for generic subprograms or for
+ -- ASIS. Do not generate contract checks in SPARK mode.
if not SPARK_Mode then
- Process_PPCs (N, Gen_Id, Body_Id);
+ Expand_Subprogram_Contract (N, Gen_Id, Body_Id);
end if;
-- If the generic unit carries pre- or post-conditions, copy them
end if;
end Analyze_Subprogram_Body;
+ --------------------------------------
+ -- Analyze_Subprogram_Body_Contract --
+ --------------------------------------
+
+ -- ??? To be implemented
+
+ procedure Analyze_Subprogram_Body_Contract (Subp : Entity_Id) is
+ pragma Unreferenced (Subp);
+ begin
+ null;
+ end Analyze_Subprogram_Body_Contract;
+
------------------------------------
-- Analyze_Subprogram_Body_Helper --
------------------------------------
end if;
Set_Corresponding_Body (Unit_Declaration_Node (Spec_Id), Body_Id);
- Set_Contract (Body_Id, Empty);
+ Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id)));
Set_Ekind (Body_Id, E_Subprogram_Body);
Set_Scope (Body_Id, Scope (Spec_Id));
Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Spec_Id));
HSS := Handled_Statement_Sequence (N);
Set_Actual_Subtypes (N, Current_Scope);
- -- Deal with preconditions and postconditions. In formal verification
- -- mode, we keep pre- and postconditions attached to entities rather
- -- than inserted in the code, in order to facilitate a distinct
- -- treatment for them.
+ -- Deal with [refined] preconditions, postconditions, Contract_Cases,
+ -- invariants and predicates associated with the body and its spec.
+ -- Note that this is not pure expansion as Expand_Subprogram_Contract
+ -- prepares the contract assertions for generic subprograms or for ASIS.
+ -- Do not generate contract checks in SPARK mode.
if not SPARK_Mode then
- Process_PPCs (N, Spec_Id, Body_Id);
+ Expand_Subprogram_Contract (N, Spec_Id, Body_Id);
end if;
-- Add a declaration for the Protection object, renaming declarations
Items : constant Node_Id := Contract (Subp);
Error_CCase : Node_Id;
Error_Post : Node_Id;
+ Nam : Name_Id;
Prag : Node_Id;
-- Start of processing for Analyze_Subprogram_Contract
Prag := Pre_Post_Conditions (Items);
while Present (Prag) loop
- Analyze_PPC_In_Decl_Part (Prag, Subp);
+ Analyze_Pre_Post_Condition_In_Decl_Part (Prag, Subp);
-- Verify whether a postcondition mentions attribute 'Result and
-- its expression introduces a post-state.
Prag := Contract_Test_Cases (Items);
while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Contract_Cases then
+ Nam := Pragma_Name (Prag);
+
+ if Nam = Name_Contract_Cases then
Analyze_Contract_Cases_In_Decl_Part (Prag);
-- Verify whether contract-cases mention attribute 'Result and
end if;
else
- pragma Assert (Pragma_Name (Prag) = Name_Test_Case);
+ pragma Assert (Nam = Name_Test_Case);
Analyze_Test_Case_In_Decl_Part (Prag, Subp);
end if;
Prag := Classifications (Contract (Subp));
while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Depends then
+ Nam := Pragma_Name (Prag);
+
+ if Nam = Name_Depends then
Analyze_Depends_In_Decl_Part (Prag);
else
- pragma Assert (Pragma_Name (Prag) = Name_Global);
+ pragma Assert (Nam = Name_Global);
Analyze_Global_In_Decl_Part (Prag);
end if;
end if;
end Process_Formals;
- ------------------
- -- Process_PPCs --
- ------------------
-
- procedure Process_PPCs
- (N : Node_Id;
- Spec_Id : Entity_Id;
- Body_Id : Entity_Id)
- is
- Loc : constant Source_Ptr := Sloc (N);
- Prag : Node_Id;
- Parms : List_Id;
-
- Designator : Entity_Id;
- -- Subprogram designator, set from Spec_Id if present, else Body_Id
-
- Precond : Node_Id := Empty;
- -- Set non-Empty if we prepend precondition to the declarations. This
- -- is used to hook up inherited preconditions (adding the condition
- -- expression with OR ELSE, and adding the message).
-
- Inherited_Precond : Node_Id;
- -- Precondition inherited from parent subprogram
-
- Inherited : constant Subprogram_List :=
- Inherited_Subprograms (Spec_Id);
- -- List of subprograms inherited by this subprogram
-
- Plist : List_Id := No_List;
- -- List of generated postconditions
-
- procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id);
- -- Append a node to a list. If there is no list, create a new one. When
- -- the item denotes a pragma, it is added to the list only when it is
- -- enabled.
-
- procedure Check_Access_Invariants (E : Entity_Id);
- -- If the subprogram returns an access to a type with invariants, or
- -- has access parameters whose designated type has an invariant, then
- -- under the same visibility conditions as for other invariant checks,
- -- the type invariant must be applied to the returned value.
-
- procedure Collect_Body_Postconditions (Post_Nam : Name_Id);
- -- Examine the declarations of the body, looking for pragmas with name
- -- Post_Nam. Parameter Post_Nam must denote either Name_Postcondition or
- -- Name_Refined_Post. Chain any relevant postconditions to Plist.
-
- function Grab_PPC (Pspec : Entity_Id := Empty) return Node_Id;
- -- Prag contains an analyzed precondition or postcondition pragma. This
- -- function copies the pragma, changes it to the corresponding Check
- -- pragma and returns the Check pragma as the result. If Pspec is non-
- -- empty, this is the case of inheriting a PPC, where we must change
- -- references to parameters of the inherited subprogram to point to the
- -- corresponding parameters of the current subprogram.
-
- function Has_Checked_Predicate (Typ : Entity_Id) return Boolean;
- -- Determine whether type Typ has or inherits at least one predicate
- -- aspect or pragma, for which the applicable policy is Checked.
-
- function Has_Null_Body (Proc_Id : Entity_Id) return Boolean;
- -- Determine whether the body of procedure Proc_Id contains a sole null
- -- statement, possibly followed by an optional return.
-
- procedure Insert_After_Last_Declaration (Nod : Node_Id);
- -- Insert node Nod after the last declaration of the context
-
- function Is_Public_Subprogram_For (T : Entity_Id) return Boolean;
- -- T is the entity for a private type for which invariants are defined.
- -- This function returns True if the procedure corresponding to the
- -- value of Designator is a public procedure from the point of view of
- -- this type (i.e. its spec is in the visible part of the package that
- -- contains the declaration of the private type). A True value means
- -- that an invariant check is required (for an IN OUT parameter, or
- -- the returned value of a function.
-
- -------------------------
- -- Append_Enabled_Item --
- -------------------------
-
- procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id) is
- begin
- -- Do not chain ignored or disabled pragmas
-
- if Nkind (Item) = N_Pragma
- and then (Is_Ignored (Item) or else Is_Disabled (Item))
- then
- null;
-
- -- Add the item
-
- else
- if No (List) then
- List := New_List;
- end if;
-
- Append (Item, List);
- end if;
- end Append_Enabled_Item;
-
- -----------------------------
- -- Check_Access_Invariants --
- -----------------------------
-
- procedure Check_Access_Invariants (E : Entity_Id) is
- Call : Node_Id;
- Obj : Node_Id;
- Typ : Entity_Id;
-
- begin
- if Is_Access_Type (Etype (E))
- and then not Is_Access_Constant (Etype (E))
- then
- Typ := Designated_Type (Etype (E));
-
- if Has_Invariants (Typ)
- and then Present (Invariant_Procedure (Typ))
- and then not Has_Null_Body (Invariant_Procedure (Typ))
- and then Is_Public_Subprogram_For (Typ)
- then
- Obj :=
- Make_Explicit_Dereference (Loc,
- Prefix => New_Occurrence_Of (E, Loc));
- Set_Etype (Obj, Typ);
-
- Call := Make_Invariant_Call (Obj);
-
- Append_Enabled_Item
- (Make_If_Statement (Loc,
- Condition =>
- Make_Op_Ne (Loc,
- Left_Opnd => Make_Null (Loc),
- Right_Opnd => New_Occurrence_Of (E, Loc)),
- Then_Statements => New_List (Call)),
- List => Plist);
- end if;
- end if;
- end Check_Access_Invariants;
-
- ---------------------------------
- -- Collect_Body_Postconditions --
- ---------------------------------
-
- procedure Collect_Body_Postconditions (Post_Nam : Name_Id) is
- Next_Prag : Node_Id;
-
- begin
- pragma Assert
- (Nam_In (Post_Nam, Name_Postcondition, Name_Refined_Post));
-
- Prag := First (Declarations (N));
- while Present (Prag) loop
- Next_Prag := Next (Prag);
-
- if Nkind (Prag) = N_Pragma then
-
- -- Capture postcondition pragmas
-
- if Pragma_Name (Prag) = Post_Nam then
- Analyze (Prag);
-
- -- All Refined_Post pragmas must be relocated to the body
- -- of the generated _Postconditions routine, otherwise they
- -- will be duplicated twice - once in the declarations of
- -- the body and once in _Postconditions.
-
- if Pragma_Name (Prag) = Name_Refined_Post then
- Remove (Prag);
- end if;
-
- -- If expansion is disabled, as in a generic unit, save
- -- pragma for later expansion.
-
- if not Expander_Active then
- Prepend (Grab_PPC, Declarations (N));
- else
- Append_Enabled_Item (Grab_PPC, Plist);
- end if;
- end if;
-
- -- Skip internally generated code
-
- elsif not Comes_From_Source (Prag) then
- null;
-
- else
- exit;
- end if;
-
- Prag := Next_Prag;
- end loop;
- end Collect_Body_Postconditions;
-
- --------------
- -- Grab_PPC --
- --------------
-
- function Grab_PPC (Pspec : Entity_Id := Empty) return Node_Id is
- Nam : constant Name_Id := Pragma_Name (Prag);
- Map : Elist_Id;
- CP : Node_Id;
-
- Ename : Name_Id;
- -- Effective name of pragma (maybe Pre/Post rather than Precondition/
- -- Postcodition if the pragma came from a Pre/Post aspect). We need
- -- the name right when we generate the Check pragma, since we want
- -- the right set of check policies to apply.
-
- begin
- -- Prepare map if this is the case where we have to map entities of
- -- arguments in the overridden subprogram to corresponding entities
- -- of the current subprogram.
-
- if No (Pspec) then
- Map := No_Elist;
-
- else
- declare
- PF : Entity_Id;
- CF : Entity_Id;
-
- begin
- Map := New_Elmt_List;
- PF := First_Formal (Pspec);
- CF := First_Formal (Designator);
- while Present (PF) loop
- Append_Elmt (PF, Map);
- Append_Elmt (CF, Map);
- Next_Formal (PF);
- Next_Formal (CF);
- end loop;
- end;
- end if;
-
- -- Now we can copy the tree, doing any required substitutions
-
- CP := New_Copy_Tree (Prag, Map => Map, New_Scope => Current_Scope);
-
- -- Set Analyzed to false, since we want to reanalyze the check
- -- procedure. Note that it is only at the outer level that we
- -- do this fiddling, for the spec cases, the already preanalyzed
- -- parameters are not affected.
-
- Set_Analyzed (CP, False);
-
- -- We also make sure Comes_From_Source is False for the copy
-
- Set_Comes_From_Source (CP, False);
-
- -- For a postcondition pragma within a generic, preserve the pragma
- -- for later expansion. This is also used when an error was detected,
- -- thus setting Expander_Active to False.
-
- if Nam = Name_Postcondition
- and then not Expander_Active
- then
- return CP;
- end if;
-
- -- Get effective name of aspect
-
- if Present (Corresponding_Aspect (Prag)) then
- Ename := Chars (Identifier (Corresponding_Aspect (Prag)));
- else
- Ename := Nam;
- end if;
-
- -- Change copy of pragma into corresponding pragma Check
-
- Prepend_To (Pragma_Argument_Associations (CP),
- Make_Pragma_Argument_Association (Sloc (Prag),
- Expression => Make_Identifier (Loc, Ename)));
- Set_Pragma_Identifier (CP, Make_Identifier (Sloc (Prag), Name_Check));
-
- -- If this is inherited case and the current message starts with
- -- "failed p", we change it to "failed inherited p...".
-
- if Present (Pspec) then
- declare
- Msg : constant Node_Id :=
- Last (Pragma_Argument_Associations (CP));
-
- begin
- if Chars (Msg) = Name_Message then
- String_To_Name_Buffer (Strval (Expression (Msg)));
-
- if Name_Buffer (1 .. 8) = "failed p" then
- Insert_Str_In_Name_Buffer ("inherited ", 8);
- Set_Strval
- (Expression (Last (Pragma_Argument_Associations (CP))),
- String_From_Name_Buffer);
- end if;
- end if;
- end;
- end if;
-
- -- Return the check pragma
-
- return CP;
- end Grab_PPC;
-
- ---------------------------
- -- Has_Checked_Predicate --
- ---------------------------
-
- function Has_Checked_Predicate (Typ : Entity_Id) return Boolean is
- Anc : Entity_Id;
- Pred : Node_Id;
-
- begin
- -- Climb the ancestor type chain staring from the input. This is done
- -- because the input type may lack aspect/pragma predicate and simply
- -- inherit those from its ancestor.
-
- -- Note that predicate pragmas include all three cases of predicate
- -- aspects (Predicate, Dynamic_Predicate, Static_Predicate), so this
- -- routine checks for all three cases.
-
- Anc := Typ;
- while Present (Anc) loop
- Pred := Get_Pragma (Anc, Pragma_Predicate);
-
- if Present (Pred) and then not Is_Ignored (Pred) then
- return True;
- end if;
-
- Anc := Nearest_Ancestor (Anc);
- end loop;
-
- return False;
- end Has_Checked_Predicate;
-
- -------------------
- -- Has_Null_Body --
- -------------------
-
- function Has_Null_Body (Proc_Id : Entity_Id) return Boolean is
- Body_Id : Entity_Id;
- Decl : Node_Id;
- Spec : Node_Id;
- Stmt1 : Node_Id;
- Stmt2 : Node_Id;
-
- begin
- Spec := Parent (Proc_Id);
- Decl := Parent (Spec);
-
- -- Retrieve the entity of the invariant procedure body
-
- if Nkind (Spec) = N_Procedure_Specification
- and then Nkind (Decl) = N_Subprogram_Declaration
- then
- Body_Id := Corresponding_Body (Decl);
-
- -- The body acts as a spec
-
- else
- Body_Id := Proc_Id;
- end if;
-
- -- The body will be generated later
-
- if No (Body_Id) then
- return False;
- end if;
-
- Spec := Parent (Body_Id);
- Decl := Parent (Spec);
-
- pragma Assert
- (Nkind (Spec) = N_Procedure_Specification
- and then Nkind (Decl) = N_Subprogram_Body);
-
- Stmt1 := First (Statements (Handled_Statement_Sequence (Decl)));
-
- -- Look for a null statement followed by an optional return statement
-
- if Nkind (Stmt1) = N_Null_Statement then
- Stmt2 := Next (Stmt1);
-
- if Present (Stmt2) then
- return Nkind (Stmt2) = N_Simple_Return_Statement;
- else
- return True;
- end if;
- end if;
-
- return False;
- end Has_Null_Body;
-
- -----------------------------------
- -- Insert_After_Last_Declaration --
- -----------------------------------
-
- procedure Insert_After_Last_Declaration (Nod : Node_Id) is
- Decls : constant List_Id := Declarations (N);
-
- begin
- if No (Decls) then
- Set_Declarations (N, New_List (Nod));
- else
- Append_To (Decls, Nod);
- end if;
- end Insert_After_Last_Declaration;
-
- ------------------------------
- -- Is_Public_Subprogram_For --
- ------------------------------
-
- -- The type T is a private type, its declaration is therefore in
- -- the list of public declarations of some package. The test for a
- -- public subprogram is that its declaration is in this same list
- -- of declarations for the same package (note that all the public
- -- declarations are in one list, and all the private declarations
- -- in another, so this deals with the public/private distinction).
-
- function Is_Public_Subprogram_For (T : Entity_Id) return Boolean is
- DD : constant Node_Id := Unit_Declaration_Node (Designator);
- -- The subprogram declaration for the subprogram in question
-
- TL : constant List_Id :=
- Visible_Declarations
- (Specification (Unit_Declaration_Node (Scope (T))));
- -- The list of declarations containing the private declaration of
- -- the type. We know it is a private type, so we know its scope is
- -- the package in question, and we know it must be in the visible
- -- declarations of this package.
-
- begin
- -- If the subprogram declaration is not a list member, it must be
- -- an Init_Proc, in which case we want to consider it to be a
- -- public subprogram, since we do get initializations to deal with.
- -- Other internally generated subprograms are not public.
-
- if not Is_List_Member (DD)
- and then Is_Init_Proc (Defining_Entity (DD))
- then
- return True;
-
- -- The declaration may have been generated for an expression function
- -- so check whether that function comes from source.
-
- elsif not Comes_From_Source (DD)
- and then
- (Nkind (Original_Node (DD)) /= N_Expression_Function
- or else not Comes_From_Source (Defining_Entity (DD)))
- then
- return False;
-
- -- Otherwise we test whether the subprogram is declared in the
- -- visible declarations of the package containing the type.
-
- else
- return TL = List_Containing (DD);
- end if;
- end Is_Public_Subprogram_For;
-
- -- Local variables
-
- Formal : Node_Id;
- Formal_Typ : Entity_Id;
- Func_Typ : Entity_Id;
- Post_Proc : Entity_Id;
- Result : Node_Id;
-
- -- Start of processing for Process_PPCs
-
- begin
- -- Capture designator from spec if present, else from body
-
- if Present (Spec_Id) then
- Designator := Spec_Id;
- else
- Designator := Body_Id;
- end if;
-
- -- Do not process a predicate function as its body will contain a
- -- recursive call to itself and blow up the stack.
-
- if Ekind (Designator) = E_Function
- and then Is_Predicate_Function (Designator)
- then
- return;
-
- -- Internally generated subprograms, such as type-specific functions,
- -- don't get assertion checks.
-
- elsif Get_TSS_Name (Designator) /= TSS_Null then
- return;
- end if;
-
- -- Grab preconditions from spec
-
- if Present (Spec_Id) then
-
- -- Loop through PPC pragmas from spec. Note that preconditions from
- -- the body will be analyzed and converted when we scan the body
- -- declarations below.
-
- Prag := Pre_Post_Conditions (Contract (Spec_Id));
- while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Precondition then
-
- -- For Pre (or Precondition pragma), we simply prepend the
- -- pragma to the list of declarations right away so that it
- -- will be executed at the start of the procedure. Note that
- -- this processing reverses the order of the list, which is
- -- what we want since new entries were chained to the head of
- -- the list. There can be more than one precondition when we
- -- use pragma Precondition.
-
- if not Class_Present (Prag) then
- Prepend (Grab_PPC, Declarations (N));
-
- -- For Pre'Class there can only be one pragma, and we save
- -- it in Precond for now. We will add inherited Pre'Class
- -- stuff before inserting this pragma in the declarations.
- else
- Precond := Grab_PPC;
- end if;
- end if;
-
- Prag := Next_Pragma (Prag);
- end loop;
-
- -- Now deal with inherited preconditions
-
- for J in Inherited'Range loop
- Prag := Pre_Post_Conditions (Contract (Inherited (J)));
-
- while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Precondition
- and then Class_Present (Prag)
- then
- Inherited_Precond := Grab_PPC (Inherited (J));
-
- -- No precondition so far, so establish this as the first
-
- if No (Precond) then
- Precond := Inherited_Precond;
-
- -- Here we already have a precondition, add inherited one
-
- else
- -- Add new precondition to old one using OR ELSE
-
- declare
- New_Expr : constant Node_Id :=
- Get_Pragma_Arg
- (Next (First (Pragma_Argument_Associations
- (Inherited_Precond))));
- Old_Expr : constant Node_Id :=
- Get_Pragma_Arg
- (Next (First (Pragma_Argument_Associations
- (Precond))));
-
- begin
- if Paren_Count (Old_Expr) = 0 then
- Set_Paren_Count (Old_Expr, 1);
- end if;
-
- if Paren_Count (New_Expr) = 0 then
- Set_Paren_Count (New_Expr, 1);
- end if;
-
- Rewrite (Old_Expr,
- Make_Or_Else (Sloc (Old_Expr),
- Left_Opnd => Relocate_Node (Old_Expr),
- Right_Opnd => New_Expr));
- end;
-
- -- Add new message in the form:
-
- -- failed precondition from bla
- -- also failed inherited precondition from bla
- -- ...
-
- -- Skip this if exception locations are suppressed
-
- if not Exception_Locations_Suppressed then
- declare
- New_Msg : constant Node_Id :=
- Get_Pragma_Arg
- (Last
- (Pragma_Argument_Associations
- (Inherited_Precond)));
- Old_Msg : constant Node_Id :=
- Get_Pragma_Arg
- (Last
- (Pragma_Argument_Associations
- (Precond)));
- begin
- Start_String (Strval (Old_Msg));
- Store_String_Chars (ASCII.LF & " also ");
- Store_String_Chars (Strval (New_Msg));
- Set_Strval (Old_Msg, End_String);
- end;
- end if;
- end if;
- end if;
-
- Prag := Next_Pragma (Prag);
- end loop;
- end loop;
-
- -- If we have built a precondition for Pre'Class (including any
- -- Pre'Class aspects inherited from parent subprograms), then we
- -- insert this composite precondition at this stage.
-
- if Present (Precond) then
- Prepend (Precond, Declarations (N));
- end if;
- end if;
-
- -- Build postconditions procedure if needed and prepend the following
- -- declaration to the start of the declarations for the subprogram.
-
- -- procedure _postconditions [(_Result : resulttype)] is
- -- begin
- -- pragma Check (Refined_Post, condition);
- -- pragma Check (Refined_Post, condition);
- -- pragma Check (Postcondition, condition [,message]);
- -- pragma Check (Postcondition, condition [,message]);
- -- ...
- -- Invariant_Procedure (_Result) ...
- -- Invariant_Procedure (Arg1)
- -- ...
- -- end;
-
- -- First we deal with the postconditions in the body
-
- Collect_Body_Postconditions (Name_Refined_Post);
- Collect_Body_Postconditions (Name_Postcondition);
-
- -- Now deal with any postconditions from the spec
-
- if Present (Spec_Id) then
- Spec_Postconditions : declare
- procedure Process_Contract_Cases (Spec : Node_Id);
- -- This processes the Contract_Test_Cases from Spec, processing
- -- any contract-cases from the list. The caller has checked that
- -- Contract_Test_Cases is non-Empty.
-
- procedure Process_Post_Conditions
- (Spec : Node_Id;
- Class : Boolean);
- -- This processes the Pre_Post_Conditions from Spec, processing
- -- any postconditions from the list. If Class is True, then only
- -- postconditions marked with Class_Present are considered. The
- -- caller has checked that Pre_Post_Conditions is non-Empty.
-
- ----------------------------
- -- Process_Contract_Cases --
- ----------------------------
-
- procedure Process_Contract_Cases (Spec : Node_Id) is
- begin
- -- Loop through Contract_Cases pragmas from spec
-
- Prag := Contract_Test_Cases (Contract (Spec));
- loop
- if Pragma_Name (Prag) = Name_Contract_Cases then
- Expand_Contract_Cases
- (CCs => Prag,
- Subp_Id => Spec_Id,
- Decls => Declarations (N),
- Stmts => Plist);
- end if;
-
- Prag := Next_Pragma (Prag);
- exit when No (Prag);
- end loop;
- end Process_Contract_Cases;
-
- -----------------------------
- -- Process_Post_Conditions --
- -----------------------------
-
- procedure Process_Post_Conditions
- (Spec : Node_Id;
- Class : Boolean)
- is
- Pspec : Node_Id;
-
- begin
- if Class then
- Pspec := Spec;
- else
- Pspec := Empty;
- end if;
-
- -- Loop through PPC pragmas from spec
-
- Prag := Pre_Post_Conditions (Contract (Spec));
- loop
- if Pragma_Name (Prag) = Name_Postcondition
- and then (not Class or else Class_Present (Prag))
- then
- if not Expander_Active then
- Prepend (Grab_PPC (Pspec), Declarations (N));
- else
- Append_Enabled_Item (Grab_PPC (Pspec), Plist);
- end if;
- end if;
-
- Prag := Next_Pragma (Prag);
- exit when No (Prag);
- end loop;
- end Process_Post_Conditions;
-
- -- Start of processing for Spec_Postconditions
-
- begin
- -- Process postconditions expressed as contract-cases
-
- if Present (Contract_Test_Cases (Contract (Spec_Id))) then
- Process_Contract_Cases (Spec_Id);
- end if;
-
- -- Process spec postconditions
-
- if Present (Pre_Post_Conditions (Contract (Spec_Id))) then
- Process_Post_Conditions (Spec_Id, Class => False);
- end if;
-
- -- Process inherited postconditions
-
- for J in Inherited'Range loop
- if Present (Pre_Post_Conditions (Contract (Inherited (J)))) then
- Process_Post_Conditions (Inherited (J), Class => True);
- end if;
- end loop;
- end Spec_Postconditions;
- end if;
-
- -- Add an invariant call to check the result of a function
-
- if Ekind (Designator) /= E_Procedure and then Expander_Active then
- Func_Typ := Etype (Designator);
- Result := Make_Defining_Identifier (Loc, Name_uResult);
-
- Set_Etype (Result, Func_Typ);
-
- -- Add argument for return
-
- Parms := New_List (
- Make_Parameter_Specification (Loc,
- Defining_Identifier => Result,
- Parameter_Type => New_Occurrence_Of (Func_Typ, Loc)));
-
- -- Add invariant call if returning type with invariants and this is a
- -- public function, i.e. a function declared in the visible part of
- -- the package defining the private type.
-
- if Has_Invariants (Func_Typ)
- and then Present (Invariant_Procedure (Func_Typ))
- and then not Has_Null_Body (Invariant_Procedure (Func_Typ))
- and then Is_Public_Subprogram_For (Func_Typ)
- then
- Append_Enabled_Item
- (Make_Invariant_Call (New_Occurrence_Of (Result, Loc)), Plist);
- end if;
-
- -- Same if return value is an access to type with invariants
-
- Check_Access_Invariants (Result);
-
- -- Procedure case
-
- else
- Parms := No_List;
- end if;
-
- -- Add invariant calls and predicate calls for parameters. Note that
- -- this is done for functions as well, since in Ada 2012 they can have
- -- IN OUT args.
-
- if Expander_Active then
- Formal := First_Formal (Designator);
- while Present (Formal) loop
- if Ekind (Formal) /= E_In_Parameter
- or else Is_Access_Type (Etype (Formal))
- then
- Formal_Typ := Etype (Formal);
-
- if Has_Invariants (Formal_Typ)
- and then Present (Invariant_Procedure (Formal_Typ))
- and then not Has_Null_Body (Invariant_Procedure (Formal_Typ))
- and then Is_Public_Subprogram_For (Formal_Typ)
- then
- Append_Enabled_Item
- (Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)),
- Plist);
- end if;
-
- Check_Access_Invariants (Formal);
-
- if Has_Predicates (Formal_Typ)
- and then Present (Predicate_Function (Formal_Typ))
- and then Has_Checked_Predicate (Formal_Typ)
- then
- Append_Enabled_Item
- (Make_Predicate_Check
- (Formal_Typ, New_Occurrence_Of (Formal, Loc)),
- Plist);
- end if;
- end if;
-
- Next_Formal (Formal);
- end loop;
- end if;
-
- -- Build and insert postcondition procedure
-
- if Expander_Active and then Present (Plist) then
- Post_Proc :=
- Make_Defining_Identifier (Loc, Chars => Name_uPostconditions);
-
- -- Insert the corresponding body of a post condition pragma after the
- -- last declaration of the context. This ensures that the body will
- -- not cause any premature freezing as it may mention types:
-
- -- procedure Proc (Obj : Array_Typ) is
- -- procedure _postconditions is
- -- begin
- -- ... Obj ...
- -- end _postconditions;
-
- -- subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1));
- -- begin
-
- -- In the example above, Obj is of type T but the incorrect placement
- -- of _postconditions will cause a crash in gigi due to an out of
- -- order reference. The body of _postconditions must be placed after
- -- the declaration of Temp to preserve correct visibility.
-
- Insert_After_Last_Declaration (
- Make_Subprogram_Body (Loc,
- Specification =>
- Make_Procedure_Specification (Loc,
- Defining_Unit_Name => Post_Proc,
- Parameter_Specifications => Parms),
-
- Declarations => Empty_List,
-
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => Plist)));
-
- Set_Ekind (Post_Proc, E_Procedure);
-
- -- If this is a procedure, set the Postcondition_Proc attribute on
- -- the proper defining entity for the subprogram.
-
- if Ekind (Designator) = E_Procedure then
- Set_Postcondition_Proc (Designator, Post_Proc);
- end if;
-
- Set_Has_Postconditions (Designator);
- end if;
- end Process_PPCs;
-
----------------------------
-- Reference_Body_Formals --
----------------------------
procedure Analyze_Subprogram_Declaration (N : Node_Id);
procedure Analyze_Subprogram_Body (N : Node_Id);
+ procedure Analyze_Subprogram_Body_Contract (Subp : Entity_Id);
+ -- Analyze all delayed aspects chained on the contract of subprogram body
+ -- Subp as if they appeared at the end of a declarative region. The aspects
+ -- in question are:
+ -- Refined_Depends
+ -- Refined_Global
+
procedure Analyze_Subprogram_Contract (Subp : Entity_Id);
-- Analyze all delayed aspects chained on the contract of subprogram Subp
- -- as if they appeared at the end of a declarative region.
+ -- as if they appeared at the end of a declarative region. The aspects in
+ -- question are:
+ -- Contract_Cases
+ -- Postcondition
+ -- Precondition
+ -- Test_Case
function Analyze_Subprogram_Specification (N : Node_Id) return Entity_Id;
-- Analyze subprogram specification in both subprogram declarations
Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N));
All_Cases : Node_Id;
CCase : Node_Id;
+ Restore : Boolean := False;
Subp_Decl : Node_Id;
Subp_Id : Entity_Id;
-- for subprogram bodies because the formals are already visible.
if Requires_Profile_Installation (N, Subp_Decl) then
+ Restore := True;
Push_Scope (Subp_Id);
Install_Formals (Subp_Id);
end if;
Next (CCase);
end loop;
- if Requires_Profile_Installation (N, Subp_Decl) then
+ if Restore then
End_Scope;
end if;
end if;
Last_Clause : Node_Id;
Subp_Decl : Node_Id;
+ Restore_Scope : Boolean := False;
+ -- Gets set True if we do a Push_Scope needing a Pop_Scope on exit
+
-- Start of processing for Analyze_Depends_In_Decl_Part
begin
-- bodies because the formals are already visible.
if Requires_Profile_Installation (N, Subp_Decl) then
+ Restore_Scope := True;
Push_Scope (Subp_Id);
Install_Formals (Subp_Id);
end if;
Next (Clause);
end loop;
- if Requires_Profile_Installation (N, Subp_Decl) then
+ if Restore_Scope then
End_Scope;
end if;
List : Node_Id;
Subp_Decl : Node_Id;
+ Restore_Scope : Boolean := False;
+ -- Set True if we do a Push_Scope requiring a Pop_Scope on exit
+
-- Start of processing for Analyze_Global_In_Decl_List
begin
-- subprogram declarations.
if Requires_Profile_Installation (N, Subp_Decl) then
+ Restore_Scope := True;
Push_Scope (Subp_Id);
Install_Formals (Subp_Id);
end if;
Analyze_Global_List (List);
- if Requires_Profile_Installation (N, Subp_Decl) then
+ if Restore_Scope then
End_Scope;
end if;
end if;
end Analyze_Global_In_Decl_Part;
- ------------------------------
- -- Analyze_PPC_In_Decl_Part --
- ------------------------------
-
- procedure Analyze_PPC_In_Decl_Part (N : Node_Id; S : Entity_Id) is
- Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N));
-
- begin
- -- Install formals and push subprogram spec onto scope stack so that we
- -- can see the formals from the pragma.
-
- Install_Formals (S);
- Push_Scope (S);
-
- -- Preanalyze the boolean expression, we treat this as a spec expression
- -- (i.e. similar to a default expression).
-
- -- In ASIS mode, for a pragma generated from a source aspect, analyze
- -- directly the the original aspect expression, which is shared with
- -- the generated pragma.
-
- if ASIS_Mode and then Present (Corresponding_Aspect (N)) then
- Preanalyze_Assert_Expression
- (Expression (Corresponding_Aspect (N)), Standard_Boolean);
- else
- Preanalyze_Assert_Expression
- (Get_Pragma_Arg (Arg1), Standard_Boolean);
- end if;
-
- -- For a class-wide condition, a reference to a controlling formal must
- -- be interpreted as having the class-wide type (or an access to such)
- -- so that the inherited condition can be properly applied to any
- -- overriding operation (see ARM12 6.6.1 (7)).
-
- if Class_Present (N) then
- Class_Wide_Condition : declare
- T : constant Entity_Id := Find_Dispatching_Type (S);
-
- ACW : Entity_Id := Empty;
- -- Access to T'class, created if there is a controlling formal
- -- that is an access parameter.
-
- function Get_ACW return Entity_Id;
- -- If the expression has a reference to an controlling access
- -- parameter, create an access to T'class for the necessary
- -- conversions if one does not exist.
-
- function Process (N : Node_Id) return Traverse_Result;
- -- ARM 6.1.1: Within the expression for a Pre'Class or Post'Class
- -- aspect for a primitive subprogram of a tagged type T, a name
- -- that denotes a formal parameter of type T is interpreted as
- -- having type T'Class. Similarly, a name that denotes a formal
- -- accessparameter of type access-to-T is interpreted as having
- -- type access-to-T'Class. This ensures the expression is well-
- -- defined for a primitive subprogram of a type descended from T.
- -- Note that this replacement is not done for selector names in
- -- parameter associations. These carry an entity for reference
- -- purposes, but semantically they are just identifiers.
-
- -------------
- -- Get_ACW --
- -------------
-
- function Get_ACW return Entity_Id is
- Loc : constant Source_Ptr := Sloc (N);
- Decl : Node_Id;
-
- begin
- if No (ACW) then
- Decl := Make_Full_Type_Declaration (Loc,
- Defining_Identifier => Make_Temporary (Loc, 'T'),
- Type_Definition =>
- Make_Access_To_Object_Definition (Loc,
- Subtype_Indication =>
- New_Occurrence_Of (Class_Wide_Type (T), Loc),
- All_Present => True));
-
- Insert_Before (Unit_Declaration_Node (S), Decl);
- Analyze (Decl);
- ACW := Defining_Identifier (Decl);
- Freeze_Before (Unit_Declaration_Node (S), ACW);
- end if;
-
- return ACW;
- end Get_ACW;
-
- -------------
- -- Process --
- -------------
-
- function Process (N : Node_Id) return Traverse_Result is
- Loc : constant Source_Ptr := Sloc (N);
- Typ : Entity_Id;
-
- begin
- if Is_Entity_Name (N)
- and then Present (Entity (N))
- and then Is_Formal (Entity (N))
- and then Nkind (Parent (N)) /= N_Type_Conversion
- and then
- (Nkind (Parent (N)) /= N_Parameter_Association
- or else N /= Selector_Name (Parent (N)))
- then
- if Etype (Entity (N)) = T then
- Typ := Class_Wide_Type (T);
-
- elsif Is_Access_Type (Etype (Entity (N)))
- and then Designated_Type (Etype (Entity (N))) = T
- then
- Typ := Get_ACW;
- else
- Typ := Empty;
- end if;
-
- if Present (Typ) then
- Rewrite (N,
- Make_Type_Conversion (Loc,
- Subtype_Mark =>
- New_Occurrence_Of (Typ, Loc),
- Expression => New_Occurrence_Of (Entity (N), Loc)));
- Set_Etype (N, Typ);
- end if;
- end if;
-
- return OK;
- end Process;
-
- procedure Replace_Type is new Traverse_Proc (Process);
-
- -- Start of processing for Class_Wide_Condition
-
- begin
- if not Present (T) then
- Error_Msg_Name_1 :=
- Chars (Identifier (Corresponding_Aspect (N)));
-
- Error_Msg_Name_2 := Name_Class;
-
- Error_Msg_N
- ("aspect `%''%` can only be specified for a primitive "
- & "operation of a tagged type", Corresponding_Aspect (N));
- end if;
-
- Replace_Type (Get_Pragma_Arg (Arg1));
- end Class_Wide_Condition;
- end if;
-
- -- Remove the subprogram from the scope stack now that the pre-analysis
- -- of the precondition/postcondition is done.
-
- End_Scope;
- end Analyze_PPC_In_Decl_Part;
-
--------------------
-- Analyze_Pragma --
--------------------
-- In Ada 95 or 05 mode, these are implementation defined pragmas, so
-- should be caught by the No_Implementation_Pragmas restriction.
- procedure Analyze_Refined_Pre_Post
- (Body_Decl : out Node_Id;
- Spec_Id : out Entity_Id;
- Legal : out Boolean);
+ procedure Analyze_Refined_Pre_Post_Condition;
-- Subsidiary routine to the analysis of pragmas Refined_Pre and
- -- Refined_Post. Body_Decl is the declaration of the subprogram body
- -- [stub] subject to the pragma. Spec_Id is the corresponding spec of
- -- the subprogram body [stub]. Flag Legal denotes whether the pragma
- -- passes all legality rules.
+ -- Refined_Post.
procedure Check_Ada_83_Warning;
-- Issues a warning message for the current pragma if operating in Ada
end if;
end Ada_2012_Pragma;
- ------------------------------
- -- Analyze_Refined_Pre_Post --
- ------------------------------
+ ----------------------------------------
+ -- Analyze_Refined_Pre_Post_Condition --
+ ----------------------------------------
- procedure Analyze_Refined_Pre_Post
- (Body_Decl : out Node_Id;
- Spec_Id : out Entity_Id;
- Legal : out Boolean)
- is
+ procedure Analyze_Refined_Pre_Post_Condition is
+ Body_Decl : Node_Id := Parent (N);
Pack_Spec : Node_Id;
Spec_Decl : Node_Id;
+ Spec_Id : Entity_Id;
Stmt : Node_Id;
begin
- -- Assume that the pragma is illegal
-
- Body_Decl := Parent (N);
- Spec_Id := Empty;
- Legal := False;
-
GNAT_Pragma;
Check_Arg_Count (1);
Check_No_Identifiers;
return;
end if;
- -- If we get here, the placement and legality of the pragma is OK
+ -- Analyze the boolean expression as a "spec expression"
- Legal := True;
- end Analyze_Refined_Pre_Post;
+ Analyze_Pre_Post_Condition_In_Decl_Part (N, Spec_Id);
+ end Analyze_Refined_Pre_Post_Condition;
--------------------------
-- Check_Ada_83_Warning --
-- analyzed.
if SPARK_Mode or else ASIS_Mode then
- Analyze_PPC_In_Decl_Part
+ Analyze_Pre_Post_Condition_In_Decl_Part
(N, Defining_Entity (Unit (Parent (PO))));
end if;
when Pragma_Rational =>
Set_Rational_Profile;
- ------------------
- -- Refined_Post --
- ------------------
+ ---------------------
+ -- Refined_Depends --
+ ---------------------
- -- pragma Refined_Post (boolean_EXPRESSION);
+ -- ??? To be implemented
- when Pragma_Refined_Post => Refined_Post : declare
- Body_Decl : Node_Id;
- Legal : Boolean;
- Spec_Id : Entity_Id;
+ when Pragma_Refined_Depends =>
+ null;
- begin
- -- Verify the legal placement of the pragma. The pragma is left
- -- intentionally semi-analyzed. Process_PPCs does the remaining
- -- analysis of the expression when Refined_Post is converted into
- -- pragma Check.
+ --------------------
+ -- Refined_Global --
+ --------------------
- Analyze_Refined_Pre_Post (Body_Decl, Spec_Id, Legal);
+ -- ??? To be implemented
- -- Analyze the expression when code generation is disabled because
- -- the contract of the related subprogram will never be processed.
+ -- Would be better if these generated an error message saying that
+ -- the feature was not yet implemented ???
- if Legal and then not Expander_Active then
- Analyze_And_Resolve (Get_Pragma_Arg (Arg1), Standard_Boolean);
- end if;
- end Refined_Post;
+ when Pragma_Refined_Global =>
+ null;
+
+ ------------------
+ -- Refined_Post --
+ ------------------
+
+ -- pragma Refined_Post (boolean_EXPRESSION);
+
+ when Pragma_Refined_Post =>
+ Analyze_Refined_Pre_Post_Condition;
-----------------
-- Refined_Pre --
-- pragma Refined_Pre (boolean_EXPRESSION);
- when Pragma_Refined_Pre => Refined_Pre : declare
- Body_Decl : Node_Id;
- Legal : Boolean;
- Restore : Boolean := False;
- Spec_Id : Entity_Id;
-
- begin
- Analyze_Refined_Pre_Post (Body_Decl, Spec_Id, Legal);
-
- if Legal then
- pragma Assert (Present (Body_Decl));
- pragma Assert (Present (Spec_Id));
-
- if Nkind (Body_Decl) = N_Subprogram_Body_Stub
- and then No (Library_Unit (Body_Decl))
- and then Current_Scope /= Spec_Id
- then
- Restore := True;
- Push_Scope (Spec_Id);
- Install_Formals (Spec_Id);
- end if;
-
- -- Convert pragma Refined_Pre into pragma Check. The analysis
- -- of the generated pragma will take care of the expression.
-
- Rewrite (N,
- Make_Pragma (Loc,
- Chars => Name_Check,
- Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression => Make_Identifier (Loc, Pname)),
-
- Make_Pragma_Argument_Association (Sloc (Arg1),
- Expression => Relocate_Node (Get_Pragma_Arg (Arg1))))));
-
- Analyze (N);
-
- if Restore then
- Pop_Scope;
- end if;
- end if;
- end Refined_Pre;
+ when Pragma_Refined_Pre =>
+ Analyze_Refined_Pre_Post_Condition;
-----------------------
-- Relative_Deadline --
when Pragma_Exit => null;
end Analyze_Pragma;
+ ---------------------------------------------
+ -- Analyze_Pre_Post_Condition_In_Decl_Part --
+ ---------------------------------------------
+
+ procedure Analyze_Pre_Post_Condition_In_Decl_Part
+ (Prag : Node_Id;
+ Subp_Id : Entity_Id)
+ is
+ Arg1 : constant Node_Id :=
+ First (Pragma_Argument_Associations (Prag));
+ Expr : Node_Id;
+ Restore : Boolean := False;
+
+ begin
+ -- Ensure that the subprogram and its formals are visible when analyzing
+ -- the expression of the pragma.
+
+ if Current_Scope /= Subp_Id then
+ Restore := True;
+ Push_Scope (Subp_Id);
+ Install_Formals (Subp_Id);
+ end if;
+
+ -- Preanalyze the boolean expression, we treat this as a spec expression
+ -- (i.e. similar to a default expression).
+
+ Expr := Get_Pragma_Arg (Arg1);
+
+ -- In ASIS mode, for a pragma generated from a source aspect, analyze
+ -- the original aspect expression, which is shared with the generated
+ -- pragma.
+
+ if ASIS_Mode and then Present (Corresponding_Aspect (Prag)) then
+ Expr := Expression (Corresponding_Aspect (Prag));
+ end if;
+
+ Preanalyze_Assert_Expression (Expr, Standard_Boolean);
+
+ -- For a class-wide condition, a reference to a controlling formal must
+ -- be interpreted as having the class-wide type (or an access to such)
+ -- so that the inherited condition can be properly applied to any
+ -- overriding operation (see ARM12 6.6.1 (7)).
+
+ if Class_Present (Prag) then
+ Class_Wide_Condition : declare
+ T : constant Entity_Id := Find_Dispatching_Type (Subp_Id);
+
+ ACW : Entity_Id := Empty;
+ -- Access to T'class, created if there is a controlling formal
+ -- that is an access parameter.
+
+ function Get_ACW return Entity_Id;
+ -- If the expression has a reference to an controlling access
+ -- parameter, create an access to T'class for the necessary
+ -- conversions if one does not exist.
+
+ function Process (N : Node_Id) return Traverse_Result;
+ -- ARM 6.1.1: Within the expression for a Pre'Class or Post'Class
+ -- aspect for a primitive subprogram of a tagged type T, a name
+ -- that denotes a formal parameter of type T is interpreted as
+ -- having type T'Class. Similarly, a name that denotes a formal
+ -- accessparameter of type access-to-T is interpreted as having
+ -- type access-to-T'Class. This ensures the expression is well-
+ -- defined for a primitive subprogram of a type descended from T.
+ -- Note that this replacement is not done for selector names in
+ -- parameter associations. These carry an entity for reference
+ -- purposes, but semantically they are just identifiers.
+
+ -------------
+ -- Get_ACW --
+ -------------
+
+ function Get_ACW return Entity_Id is
+ Loc : constant Source_Ptr := Sloc (Prag);
+ Decl : Node_Id;
+
+ begin
+ if No (ACW) then
+ Decl :=
+ Make_Full_Type_Declaration (Loc,
+ Defining_Identifier => Make_Temporary (Loc, 'T'),
+ Type_Definition =>
+ Make_Access_To_Object_Definition (Loc,
+ Subtype_Indication =>
+ New_Occurrence_Of (Class_Wide_Type (T), Loc),
+ All_Present => True));
+
+ Insert_Before (Unit_Declaration_Node (Subp_Id), Decl);
+ Analyze (Decl);
+ ACW := Defining_Identifier (Decl);
+ Freeze_Before (Unit_Declaration_Node (Subp_Id), ACW);
+ end if;
+
+ return ACW;
+ end Get_ACW;
+
+ -------------
+ -- Process --
+ -------------
+
+ function Process (N : Node_Id) return Traverse_Result is
+ Loc : constant Source_Ptr := Sloc (N);
+ Typ : Entity_Id;
+
+ begin
+ if Is_Entity_Name (N)
+ and then Present (Entity (N))
+ and then Is_Formal (Entity (N))
+ and then Nkind (Parent (N)) /= N_Type_Conversion
+ and then
+ (Nkind (Parent (N)) /= N_Parameter_Association
+ or else N /= Selector_Name (Parent (N)))
+ then
+ if Etype (Entity (N)) = T then
+ Typ := Class_Wide_Type (T);
+
+ elsif Is_Access_Type (Etype (Entity (N)))
+ and then Designated_Type (Etype (Entity (N))) = T
+ then
+ Typ := Get_ACW;
+ else
+ Typ := Empty;
+ end if;
+
+ if Present (Typ) then
+ Rewrite (N,
+ Make_Type_Conversion (Loc,
+ Subtype_Mark =>
+ New_Occurrence_Of (Typ, Loc),
+ Expression => New_Occurrence_Of (Entity (N), Loc)));
+ Set_Etype (N, Typ);
+ end if;
+ end if;
+
+ return OK;
+ end Process;
+
+ procedure Replace_Type is new Traverse_Proc (Process);
+
+ -- Start of processing for Class_Wide_Condition
+
+ begin
+ if not Present (T) then
+ Error_Msg_Name_1 :=
+ Chars (Identifier (Corresponding_Aspect (Prag)));
+
+ Error_Msg_Name_2 := Name_Class;
+
+ Error_Msg_N
+ ("aspect `%''%` can only be specified for a primitive "
+ & "operation of a tagged type", Corresponding_Aspect (Prag));
+ end if;
+
+ Replace_Type (Get_Pragma_Arg (Arg1));
+ end Class_Wide_Condition;
+ end if;
+
+ -- Remove the subprogram from the scope stack now that the pre-analysis
+ -- of the precondition/postcondition is done.
+
+ if Restore then
+ End_Scope;
+ end if;
+ end Analyze_Pre_Post_Condition_In_Decl_Part;
+
+ ------------------------------------------
+ -- Analyze_Refined_Depends_In_Decl_Part --
+ ------------------------------------------
+
+ -- ??? To be implemented
+
+ procedure Analyze_Refined_Depends_In_Decl_Part (N : Node_Id) is
+ pragma Unreferenced (N);
+ begin
+ null;
+ end Analyze_Refined_Depends_In_Decl_Part;
+
+ -----------------------------------------
+ -- Analyze_Refined_Global_In_Decl_Part --
+ -----------------------------------------
+
+ -- ??? To be implemented
+
+ procedure Analyze_Refined_Global_In_Decl_Part (N : Node_Id) is
+ pragma Unreferenced (N);
+ begin
+ null;
+ end Analyze_Refined_Global_In_Decl_Part;
+
------------------------------------
-- Analyze_Test_Case_In_Decl_Part --
------------------------------------
Pragma_Queuing_Policy => -1,
Pragma_Rational => -1,
Pragma_Ravenscar => -1,
+ Pragma_Refined_Depends => -1,
+ Pragma_Refined_Global => -1,
Pragma_Refined_Post => -1,
Pragma_Refined_Pre => -1,
Pragma_Relative_Deadline => -1,
-- the pragmas below implement an aspect.
Pragma_On_Body_Or_Stub_OK : constant array (Pragma_Id) of Boolean :=
- (Pragma_Refined_Post => True,
- Pragma_Refined_Pre => True,
- Pragma_SPARK_Mode => True,
- Pragma_Warnings => True,
- others => False);
+ (Pragma_Refined_Depends => True,
+ Pragma_Refined_Global => True,
+ Pragma_Refined_Post => True,
+ Pragma_Refined_Pre => True,
+ Pragma_SPARK_Mode => True,
+ Pragma_Warnings => True,
+ others => False);
-----------------
-- Subprograms --
procedure Analyze_Global_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Global
- procedure Analyze_PPC_In_Decl_Part (N : Node_Id; S : Entity_Id);
- -- Special analyze routine for precondition/postcondition pragma that
- -- appears within a declarative part where the pragma is associated
- -- with a subprogram specification. N is the pragma node, and S is the
- -- entity for the related subprogram. This procedure does a preanalysis
- -- of the expressions in the pragma as "spec expressions" (see section
- -- in Sem "Handling of Default and Per-Object Expressions...").
+ procedure Analyze_Pre_Post_Condition_In_Decl_Part
+ (Prag : Node_Id;
+ Subp_Id : Entity_Id);
+ -- Perform preanalysis of a [refined] precondition or postcondition that
+ -- appears on a subprogram declaration or body [stub]. Prag denotes the
+ -- pragma, Subp_Id is the entity of the related subprogram. The preanalysis
+ -- of the expression is done as "spec expression" (see section "Handling
+ -- of Default and Per-Object Expressions in Sem).
+
+ procedure Analyze_Refined_Depends_In_Decl_Part (N : Node_Id);
+ -- Preform full analysis of delayed pragma Refined_Depends
+
+ procedure Analyze_Refined_Global_In_Decl_Part (N : Node_Id);
+ -- Perform full analysis of delayed pragma Refined_Global
procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id; S : Entity_Id);
- -- Special analyze routine for contract-case and test-case pragmas that
- -- appears within a declarative part where the pragma is associated with
- -- a subprogram specification. N is the pragma node, and S is the entity
- -- for the related subprogram. This procedure does a preanalysis of the
- -- expressions in the pragma as "spec expressions" (see section in Sem
- -- "Handling of Default and Per-Object Expressions...").
+ -- Perform preanalysis of pragma Test_Case that applies to a subprogram
+ -- declaration. Parameter N denotes the pragma, S is the entity of the
+ -- related subprogram. The preanalysis of the expression is done as "spec
+ -- expression" (see section "Handling of Default and Per-Object Expressions
+ -- in Sem).
procedure Check_Applicable_Policy (N : Node_Id);
-- N is either an N_Aspect or an N_Pragma node. There are two cases. If
-- Add_Contract_Item --
-----------------------
- procedure Add_Contract_Item (Item : Node_Id; Subp_Id : Entity_Id) is
+ procedure Add_Contract_Item (Prag : Node_Id; Subp_Id : Entity_Id) is
Items : constant Node_Id := Contract (Subp_Id);
Nam : Name_Id;
begin
- if Present (Items) and then Nkind (Item) = N_Pragma then
- Nam := Pragma_Name (Item);
+ -- The related subprogram [body] must have a contract and the item to be
+ -- added must be a pragma.
- if Nam_In (Nam, Name_Precondition, Name_Postcondition) then
- Set_Next_Pragma (Item, Pre_Post_Conditions (Items));
- Set_Pre_Post_Conditions (Items, Item);
+ pragma Assert (Present (Items));
+ pragma Assert (Nkind (Prag) = N_Pragma);
- elsif Nam_In (Nam, Name_Contract_Cases, Name_Test_Case) then
- Set_Next_Pragma (Item, Contract_Test_Cases (Items));
- Set_Contract_Test_Cases (Items, Item);
+ Nam := Pragma_Name (Prag);
- elsif Nam_In (Nam, Name_Depends, Name_Global) then
- Set_Next_Pragma (Item, Classifications (Items));
- Set_Classifications (Items, Item);
+ -- Contract items related to subprogram bodies
+
+ if Ekind (Subp_Id) = E_Subprogram_Body then
+ if Nam_In (Nam, Name_Refined_Depends, Name_Refined_Global) then
+ Set_Next_Pragma (Prag, Classifications (Items));
+ Set_Classifications (Items, Prag);
-- The pragma is not a proper contract item
raise Program_Error;
end if;
- -- The subprogram has not been properly decorated or the item is illegal
+ -- Contract items related to subprogram declarations
else
- raise Program_Error;
+ if Nam_In (Nam, Name_Precondition, Name_Postcondition) then
+ Set_Next_Pragma (Prag, Pre_Post_Conditions (Items));
+ Set_Pre_Post_Conditions (Items, Prag);
+
+ elsif Nam_In (Nam, Name_Contract_Cases, Name_Test_Case) then
+ Set_Next_Pragma (Prag, Contract_Test_Cases (Items));
+ Set_Contract_Test_Cases (Items, Prag);
+
+ elsif Nam_In (Nam, Name_Depends, Name_Global) then
+ Set_Next_Pragma (Prag, Classifications (Items));
+ Set_Classifications (Items, Prag);
+
+ -- The pragma is not a proper contract item
+
+ else
+ raise Program_Error;
+ end if;
end if;
end Add_Contract_Item;
-- Add A to the list of access types to process when expanding the
-- freeze node of E.
- procedure Add_Contract_Item (Item : Node_Id; Subp_Id : Entity_Id);
- -- Add a contract item (pragma Precondition, Postcondition, Test_Case,
- -- Contract_Cases, Global, Depends) to the contract of a subprogram. Item
- -- denotes a pragma and Subp_Id is the related subprogram.
+ procedure Add_Contract_Item (Prag : Node_Id; Subp_Id : Entity_Id);
+ -- Add one of the following contract item to the contract of a subprogram.
+ -- Prag denotes a pragma and Subp_Id is the related subprogram [body].
+ -- Contract_Cases
+ -- Depends
+ -- Global
+ -- Postcondition
+ -- Precondition
+ -- Refined_Depends
+ -- Refined_Global
+ -- Test_Case
procedure Add_Global_Declaration (N : Node_Id);
-- These procedures adds a declaration N at the library level, to be
--------------
-- This node is used to hold the various parts of an entry or subprogram
- -- contract, consisting in pre- and postconditions on the one hand, and
- -- test-cases on the other hand.
+ -- [body] contract, consisting of precondition, postconditions, contract
+ -- cases, test cases and global dependencies.
- -- It is referenced from an entry, a subprogram or a generic subprogram
- -- entity.
+ -- The node appears in an entry and [generic] subprogram [body] entity.
-- Sprint syntax: <none> as the node should not appear in the tree, but
-- only attached to an entry or [generic] subprogram
-- Classifications (Node3) (set to Empty if none)
-- Pre_Post_Conditions contains a collection of pragmas that correspond
- -- to pre- and postconditions associated with an entry or a subprogram.
- -- The pragmas can either come from source or be the byproduct of aspect
- -- expansion. The ordering in the list is in LIFO fashion.
+ -- to pre- and postconditions associated with an entry or a subprogram
+ -- [body or stub]. The pragmas can either come from source or be the
+ -- byproduct of aspect expansion. The ordering in the list is in LIFO
+ -- fashion.
-- Note that there might be multiple preconditions or postconditions
-- in this list, either because they come from separate pragmas in the
-- Classifications contains pragmas that either categorize subprogram
-- inputs and outputs or establish dependencies between them. Currently
- -- pragmas Depends and Global are stored in this list. The ordering is
- -- in LIFO fashion.
+ -- pragmas Depends, Global, Refined_Depends and Refined_Global are
+ -- stored in this list. The ordering is in LIFO fashion.
-------------------
-- Expanded_Name --
Name_Pure_05 : constant Name_Id := N + $; -- GNAT
Name_Pure_12 : constant Name_Id := N + $; -- GNAT
Name_Pure_Function : constant Name_Id := N + $; -- GNAT
+ Name_Refined_Depends : constant Name_Id := N + $; -- GNAT
+ Name_Refined_Global : constant Name_Id := N + $; -- GNAT
Name_Refined_Post : constant Name_Id := N + $; -- GNAT
Name_Refined_Pre : constant Name_Id := N + $; -- GNAT
Name_Relative_Deadline : constant Name_Id := N + $; -- Ada 05
Pragma_Pure_05,
Pragma_Pure_12,
Pragma_Pure_Function,
+ Pragma_Refined_Depends,
+ Pragma_Refined_Global,
Pragma_Refined_Post,
Pragma_Refined_Pre,
Pragma_Relative_Deadline,
for Physical_Line_Number'Size use 32;
-- Line number type, used for storing physical line numbers (i.e. line
-- numbers in the physical file being compiled, unaffected by the presence
- -- of source reference pragmas.
+ -- of source reference pragmas).
type Column_Number is range 0 .. 32767;
for Column_Number'Size use 16;
projects / thirdparty / gcc.git / commitdiff
