AI12-0044 is a binding interpretation that restricts type-invariant
checking to occur on in parameters of procedures but not functions after
a call, because such checks done on function calls within type
invariants could cause unbounded recursion. This modifies AI05-0289,
which specified that invariant checks be done for all parameter modes,
but apparently that AI was never fully implemented, so the checks are
added now for procedure parameters of mode in.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* contracts.adb (Add_Invariant_And_Predicate_Checks): Relax the
condition for doing invariant checks so that in-mode parameters
of procedures are also checked (required by AI05-0289, and
restricted to procedures by AI12-0044). This is done in a
procedure's nested postconditions procedure.
* exp_ch6.adb (Expand_Actuals): Also perform postcall invariant
checks for in parameters of procedures (but not functions).
Moved invariant-checking code to end of Expand_Actuals
(including the nested function Is_Public_Subp).diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -1864,13 +1864,15 @@ package body Contracts is
Add_Invariant_Access_Checks (Result);
end if;
- -- Add invariant and predicates for all formals that qualify
+ -- Add invariant checks for all formals that qualify (see AI05-0289
+ -- and AI12-0044).
Formal := First_Formal (Subp_Id);
while Present (Formal) loop
Typ := Etype (Formal);
if Ekind (Formal) /= E_In_Parameter
+ or else Ekind (Subp_Id) = E_Procedure
or else Is_Access_Type (Typ)
then
if Invariant_Checks_OK (Typ) then
diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -2461,46 +2461,6 @@ package body Exp_Ch6 is
Aund : constant Entity_Id := Underlying_Type (E_Actual);
Atyp : Entity_Id;
- function Is_Public_Subp return Boolean;
- -- Check whether the subprogram being called is a visible
- -- operation of the type of the actual. Used to determine
- -- whether an invariant check must be generated on the
- -- caller side.
-
- ---------------------
- -- Is_Public_Subp --
- ---------------------
-
- function Is_Public_Subp return Boolean is
- Pack : constant Entity_Id := Scope (Subp);
- Subp_Decl : Node_Id;
-
- begin
- if not Is_Subprogram (Subp) then
- return False;
-
- -- The operation may be inherited, or a primitive of the
- -- root type.
-
- elsif
- Nkind_In (Parent (Subp), N_Private_Extension_Declaration,
- N_Full_Type_Declaration)
- then
- Subp_Decl := Parent (Subp);
-
- else
- Subp_Decl := Unit_Declaration_Node (Subp);
- end if;
-
- return Ekind (Pack) = E_Package
- and then
- List_Containing (Subp_Decl) =
- Visible_Declarations
- (Specification (Unit_Declaration_Node (Pack)));
- end Is_Public_Subp;
-
- -- Start of processing for By_Ref_Predicate_Check
-
begin
if No (Aund) then
Atyp := E_Actual;
@@ -2518,33 +2478,6 @@ package body Exp_Ch6 is
Append_To (Post_Call,
Make_Predicate_Check (Atyp, Actual));
end if;
-
- -- We generated caller-side invariant checks in two cases:
-
- -- a) when calling an inherited operation, where there is an
- -- implicit view conversion of the actual to the parent type.
-
- -- b) When the conversion is explicit
-
- -- We treat these cases separately because the required
- -- conversion for a) is added later when expanding the call.
-
- if Has_Invariants (Etype (Actual))
- and then
- Nkind (Parent (Subp)) = N_Private_Extension_Declaration
- then
- if Comes_From_Source (N) and then Is_Public_Subp then
- Append_To (Post_Call, Make_Invariant_Call (Actual));
- end if;
-
- elsif Nkind (Actual) = N_Type_Conversion
- and then Has_Invariants (Etype (Expression (Actual)))
- then
- if Comes_From_Source (N) and then Is_Public_Subp then
- Append_To (Post_Call,
- Make_Invariant_Call (Expression (Actual)));
- end if;
- end if;
end By_Ref_Predicate_Check;
-- Processing for IN parameters
@@ -2629,6 +2562,85 @@ package body Exp_Ch6 is
end if;
end if;
+ -- Type-invariant checks for in-out and out parameters, as well as
+ -- for in parameters of procedures (AI05-0289 and AI12-0044).
+
+ if Ekind (Formal) /= E_In_Parameter
+ or else Ekind (Subp) = E_Procedure
+ then
+ Caller_Side_Invariant_Checks : declare
+
+ function Is_Public_Subp return Boolean;
+ -- Check whether the subprogram being called is a visible
+ -- operation of the type of the actual. Used to determine
+ -- whether an invariant check must be generated on the
+ -- caller side.
+
+ ---------------------
+ -- Is_Public_Subp --
+ ---------------------
+
+ function Is_Public_Subp return Boolean is
+ Pack : constant Entity_Id := Scope (Subp);
+ Subp_Decl : Node_Id;
+
+ begin
+ if not Is_Subprogram (Subp) then
+ return False;
+
+ -- The operation may be inherited, or a primitive of the
+ -- root type.
+
+ elsif
+ Nkind_In (Parent (Subp), N_Private_Extension_Declaration,
+ N_Full_Type_Declaration)
+ then
+ Subp_Decl := Parent (Subp);
+
+ else
+ Subp_Decl := Unit_Declaration_Node (Subp);
+ end if;
+
+ return Ekind (Pack) = E_Package
+ and then
+ List_Containing (Subp_Decl) =
+ Visible_Declarations
+ (Specification (Unit_Declaration_Node (Pack)));
+ end Is_Public_Subp;
+
+ -- Start of processing for Caller_Side_Invariant_Checks
+
+ begin
+ -- We generate caller-side invariant checks in two cases:
+
+ -- a) when calling an inherited operation, where there is an
+ -- implicit view conversion of the actual to the parent type.
+
+ -- b) When the conversion is explicit
+
+ -- We treat these cases separately because the required
+ -- conversion for a) is added later when expanding the call.
+
+ if Has_Invariants (Etype (Actual))
+ and then
+ Nkind (Parent (Etype (Actual)))
+ = N_Private_Extension_Declaration
+ then
+ if Comes_From_Source (N) and then Is_Public_Subp then
+ Append_To (Post_Call, Make_Invariant_Call (Actual));
+ end if;
+
+ elsif Nkind (Actual) = N_Type_Conversion
+ and then Has_Invariants (Etype (Expression (Actual)))
+ then
+ if Comes_From_Source (N) and then Is_Public_Subp then
+ Append_To
+ (Post_Call, Make_Invariant_Call (Expression (Actual)));
+ end if;
+ end if;
+ end Caller_Side_Invariant_Checks;
+ end if;
+
Next_Formal (Formal);
Next_Actual (Actual);
end loop;
