-- postconditions until finalization has been performed when cleanup
-- actions are present.
+ -- NOTE: This flag could be made into a predicate since we should be
+ -- able at compile time to recognize when finalization and cleanup
+ -- actions occur, but in practice this is not possible ???
+
-- Generate:
--
-- Postcond_Enabled : Boolean := True;
-- the postconditions: this would cause confusing debug info to be
-- produced, interfering with coverage-analysis tools.
- -- Also, wrap the postcondition checks in a conditional which can be
- -- used to delay their evaluation when clean-up actions are present.
+ -- NOTE: Coverage-analysis and static-analysis tools rely on the
+ -- postconditions procedure being free of internally generated code
+ -- since some of these tools, like CodePeer, treat _postconditions
+ -- as original source.
-- Generate:
--
-- procedure _postconditions is
-- begin
- -- if Postcond_Enabled and then Return_Success_For_Postcond then
- -- [Stmts];
- -- end if;
+ -- [Stmts];
-- end;
Proc_Bod :=
Handled_Statement_Sequence =>
Make_Handled_Sequence_Of_Statements (Loc,
End_Label => Make_Identifier (Loc, Chars (Proc_Id)),
- Statements => New_List (
- Make_If_Statement (Loc,
- Condition =>
- Make_And_Then (Loc,
- Left_Opnd =>
- New_Occurrence_Of
- (Defining_Identifier
- (Postcond_Enabled_Decl), Loc),
- Right_Opnd =>
- New_Occurrence_Of
- (Defining_Identifier
- (Return_Success_Decl), Loc)),
- Then_Statements => Stmts))));
+ Statements => Stmts));
Insert_After_And_Analyze (Last_Decl, Proc_Bod);
end Build_Postconditions_Procedure;
-- has contract assertions that need to be verified on exit.
-- Also, mark the successful return to signal that postconditions
- -- need to be evaluated when finalization occurs.
+ -- need to be evaluated when finalization occurs by setting
+ -- Return_Success_For_Postcond to be True.
if Ekind (Spec_Id) = E_Procedure
and then Present (Postconditions_Proc (Spec_Id))
-- Generate:
--
-- Return_Success_For_Postcond := True;
- -- _postconditions;
+ -- if Postcond_Enabled then
+ -- _postconditions;
+ -- end if;
Insert_Action (Stmt,
Make_Assignment_Statement (Loc,
Name =>
New_Occurrence_Of
- (Get_Return_Success_For_Postcond (Spec_Id), Loc),
+ (Get_Return_Success_For_Postcond (Spec_Id), Loc),
Expression => New_Occurrence_Of (Standard_True, Loc)));
+ -- Wrap the call to _postconditions within a test of the
+ -- Postcond_Enabled flag to delay postcondition evaluation
+ -- until after finalization when required.
+
Insert_Action (Stmt,
- Make_Procedure_Call_Statement (Loc,
- Name =>
- New_Occurrence_Of (Postconditions_Proc (Spec_Id), Loc)));
+ Make_If_Statement (Loc,
+ Condition =>
+ New_Occurrence_Of (Get_Postcond_Enabled (Spec_Id), Loc),
+ Then_Statements => New_List (
+ Make_Procedure_Call_Statement (Loc,
+ Name =>
+ New_Occurrence_Of
+ (Postconditions_Proc (Spec_Id), Loc)))));
end if;
-- Ada 2020 (AI12-0279): append the call to 'Yield unless this is
-- Generate:
--
-- Return_Success_For_Postcond := True;
- -- _postconditions;
+ -- if Postcond_Enabled then
+ -- _postconditions;
+ -- end if;
Insert_Action (N,
Make_Assignment_Statement (Loc,
(Get_Return_Success_For_Postcond (Scope_Id), Loc),
Expression => New_Occurrence_Of (Standard_True, Loc)));
+ -- Wrap the call to _postconditions within a test of the
+ -- Postcond_Enabled flag to delay postcondition evaluation until
+ -- after finalization when required.
+
Insert_Action (N,
- Make_Procedure_Call_Statement (Loc,
- Name => New_Occurrence_Of (Postconditions_Proc (Scope_Id), Loc)));
+ Make_If_Statement (Loc,
+ Condition =>
+ New_Occurrence_Of (Get_Postcond_Enabled (Scope_Id), Loc),
+ Then_Statements => New_List (
+ Make_Procedure_Call_Statement (Loc,
+ Name =>
+ New_Occurrence_Of
+ (Postconditions_Proc (Scope_Id), Loc)))));
end if;
-- Ada 2020 (AI12-0279)
-- Generate:
--
-- Return_Success_For_Postcond := True;
+ -- if Postcond_Enabled then
+ -- _Postconditions ([exp]);
+ -- end if;
Insert_Action (Exp,
Make_Assignment_Statement (Loc,
(Get_Return_Success_For_Postcond (Scope_Id), Loc),
Expression => New_Occurrence_Of (Standard_True, Loc)));
- -- Generate call to _Postconditions
+ -- Wrap the call to _postconditions within a test of the
+ -- Postcond_Enabled flag to delay postcondition evaluation until
+ -- after finalization when required.
Insert_Action (Exp,
- Make_Procedure_Call_Statement (Loc,
- Name =>
- New_Occurrence_Of (Postconditions_Proc (Scope_Id), Loc),
- Parameter_Associations => New_List (New_Copy_Tree (Exp))));
+ Make_If_Statement (Loc,
+ Condition =>
+ New_Occurrence_Of (Get_Postcond_Enabled (Scope_Id), Loc),
+ Then_Statements => New_List (
+ Make_Procedure_Call_Statement (Loc,
+ Name =>
+ New_Occurrence_Of
+ (Postconditions_Proc (Scope_Id), Loc),
+ Parameter_Associations => New_List (New_Copy_Tree (Exp))))));
end if;
-- Ada 2005 (AI-251): If this return statement corresponds with an
-- -- Perform postcondition checks after general finalization, but
-- -- before finalization of 'Old related objects.
--
- -- if not Raised_Finalization_Exception then
+ -- if not Raised_Finalization_Exception
+ -- and then Return_Success_For_Postcond
+ -- then
-- begin
-- -- Re-enable postconditions and check them
--
-- Generate:
--
- -- if not Raised_Finalization_Exception then
+ -- if not Raised_Finalization_Exception
+ -- and then Return_Success_For_Postcond
+ -- then
-- begin
-- Postcond_Enabled := True;
-- _postconditions [(Result_Obj_For_Postcond[.all])];
Append_To (Fin_Controller_Stmts,
Make_If_Statement (Loc,
Condition =>
- Make_Op_Not (Loc,
+ Make_And_Then (Loc,
+ Left_Opnd =>
+ Make_Op_Not (Loc,
+ Right_Opnd =>
+ New_Occurrence_Of
+ (Raised_Finalization_Exception_Id, Loc)),
Right_Opnd =>
New_Occurrence_Of
- (Raised_Finalization_Exception_Id, Loc)),
+ (Get_Return_Success_For_Postcond (Def_Ent), Loc)),
Then_Statements => New_List (
Make_Block_Statement (Loc,
Handled_Statement_Sequence =>