aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/contracts.ads
diff options
context:
space:
mode:
authorJustin Squirek <squirek@adacore.com>2020-11-16 09:08:51 -0500
committerPierre-Marie de Rodat <derodat@adacore.com>2020-12-15 06:41:56 -0500
commita1023434a8dd3ce2281a726d30ef370caa425252 (patch)
tree96879e168c070a781a22b5670da318bf9bf47143 /gcc/ada/contracts.ads
parent43852482cafa73da6408120722dcbe7ff6fd3ded (diff)
downloadgcc-a1023434a8dd3ce2281a726d30ef370caa425252.zip
gcc-a1023434a8dd3ce2281a726d30ef370caa425252.tar.gz
gcc-a1023434a8dd3ce2281a726d30ef370caa425252.tar.bz2
[Ada] Postcondition checks performed before finalization
gcc/ada/ * contracts.adb, contracts.ads (Build_Postconditions_Procedure): Add declarations for Postcond_Enabled, Result_Object_For_Postcondition, and Return_Success_For_Postcond, and place all postconditions within an if statement to control their execution for interactions when cleanup actions get generated. (Get_Postcond_Enabled): Created to fetch object declared to handle new expansion of postconditions. (Get_Result_Object_For_Postcond): Created to fetch object declared to handle new expansion of postconditions. (Get_Return_Success_For_Postcond): Created to fetch object declared to handle new expansion of postconditions. * einfo.adb, einfo.ads: Modify flag Stores_Attribute_Old_Prefix to apply to constants, variables, and types. * exp_ch6.adb (Add_Return): Add assignment to Return_Success_For_Postcond. (Expand_Non_Function_Return): Add assignment to Return_Success_For_Postcond (Expand_Simple_Function_Return): Add assignment to Result_Object_For_Postcond and Return_Success_For_Postcond. * exp_ch7.adb (Build_Finalization_Master): Mark finalization masters which finalize types created store 'Old objects as storing 'Old objects. (Build_Finalizer): Created to generated a unified and special expansion for finalization when postconditions are present. (Build_Finalizer_Helper): Renamed Build_Finalizer and added parameter to facilitate the creation of separate finalization routines for 'Old objects and general objects. (Create_Finalizer): Add condition for the insertion of the finalizer spec to avoid malformed trees. (Expand_Cleanup_Actions): Move _postconditions and related declarations to the new declarative section. Fix the loop to properly stop at the subprogram declaration for the postconditions procedure and exclude its body from being moved to the new list of declarations to avoid freezing issues. * exp_prag.adb (Expand_Attributes): Mark temporary created to store 'Old objects as storing a 'Old attribute. * sem_ch6.adb (Find_What_Applies_To): Remove strange exception to postconditions when traversing the scope stack. * sem_prag.adb (Find_Related_Declaration_Or_Body): Use the newly created Enclosing_HSS function to find the HSS for a potentially nested statement. * sem_util.adb, sem_util.ads (Declare_Indirect_Temp): Mark types created to store 'Old objects as storing 'Old attributes. (Enclosing_HSS): Created to find the enclosing handled sequence of statements for a given statement. * snames.ads-tmpl: Add multiple names to aid in the expansion of finalization and to control the evaluation of postconditions. Including _finalization_controller, a new routine to centralize finalization actions and postcondition evaluation.
Diffstat (limited to 'gcc/ada/contracts.ads')
-rw-r--r--gcc/ada/contracts.ads15
1 files changed, 15 insertions, 0 deletions
diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads
index 4782ef5..b8a12ff 100644
--- a/gcc/ada/contracts.ads
+++ b/gcc/ada/contracts.ads
@@ -188,6 +188,21 @@ package Contracts is
-- denoted by Body_Decl. In addition, freeze the contract of the nearest
-- enclosing package body.
+ function Get_Postcond_Enabled (Subp : Entity_Id) return Entity_Id;
+ -- Get the defining identifier for a subprogram's Postcond_Enabled
+ -- object created during the expansion of the subprogram's postconditions.
+
+ function Get_Result_Object_For_Postcond (Subp : Entity_Id) return Entity_Id;
+ -- Get the defining identifier for a subprogram's
+ -- Result_Object_For_Postcond object created during the expansion of the
+ -- subprogram's postconditions.
+
+ function Get_Return_Success_For_Postcond
+ (Subp : Entity_Id) return Entity_Id;
+ -- Get the defining identifier for a subprogram's
+ -- Return_Success_For_Postcond object created during the expansion of the
+ -- subprogram's postconditions.
+
procedure Inherit_Subprogram_Contract
(Subp : Entity_Id;
From_Subp : Entity_Id);