exp_ch7.adb (Build_Invariant_Procedure_Body): Semi-insert the body into the tree for GNATprove by setting its Parent field.

2017-01-19  Claire Dross  <dross@adacore.com>

	* exp_ch7.adb (Build_Invariant_Procedure_Body): Semi-insert the
	body into the tree for GNATprove by setting its Parent field. The
	components invariants of composite types are not checked by
	the composite type's invariant procedure in GNATprove mode.
	(Build_Invariant_Procedure_Declaration): Semi-insert the
	declaration into the tree for GNATprove by setting its Parent
	field.
	* freeze.adb (Freeze_Arry_Type):In GNATprove mode, do not add
	the component invariants to the array type  invariant procedure
	so that the procedure can be used to  check the array type
	invariants if any.
	(Freeze_Record_Type): In GNATprove mode, do
	not add the component invariants to the record type  invariant
	procedure so that the procedure can be used to	check the record
	type invariants if any.

From-SVN: r244629

3 files changed, 114 insertions, 52 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index ba2c120..9743e60 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,21 @@
+2017-01-19  Claire Dross  <dross@adacore.com>
+
+	* exp_ch7.adb (Build_Invariant_Procedure_Body): Semi-insert the
+	body into the tree for GNATprove by setting its Parent field. The
+	components invariants of composite types are not checked by
+	the composite type's invariant procedure in GNATprove mode.
+	(Build_Invariant_Procedure_Declaration): Semi-insert the
+	declaration into the tree for GNATprove by setting its Parent
+	field.
+	* freeze.adb (Freeze_Arry_Type):In GNATprove mode, do not add
+	the component invariants to the array type  invariant procedure
+	so that the procedure can be used to  check the array type
+	invariants if any.
+	(Freeze_Record_Type): In GNATprove mode, do
+	not add the component invariants to the record type  invariant
+	procedure so that the procedure can be used to	check the record
+	type invariants if any.
+
 2017-01-19  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* lib-xref-spark_specific.adb: Minor reformatting.
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index 0c21808..93573a2 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -3581,30 +3581,41 @@ package body Exp_Ch7 is
 
          begin
             if Has_Invariants (Comp_Typ) then
-               Proc_Id := Invariant_Procedure (Base_Type (Comp_Typ));
 
-               --  The component type should have an invariant procedure if it
-               --  has invariants of its own or inherits class-wide invariants
-               --  from parent or interface types.
+               --  In GNATprove mode, the component invariants are checked by
+               --  other means. They should not be added to the array type
+               --  invariant procedure, so that the procedure can be used to
+               --  check the array type invariants if any.
 
-               pragma Assert (Present (Proc_Id));
+               if GNATprove_Mode then
+                  null;
 
-               --  Generate:
-               --    <Comp_Typ>Invariant (_object (<Indices>));
+               else
+                  Proc_Id := Invariant_Procedure (Base_Type (Comp_Typ));
 
-               --  Note that the invariant procedure may have a null body if
-               --  assertions are disabled or Assertion_Polity Ignore is in
-               --  effect.
+                  --  The component type should have an invariant procedure
+                  --  if it has invariants of its own or inherits class-wide
+                  --  invariants from parent or interface types.
 
-               if not Has_Null_Body (Proc_Id) then
-                  Append_New_To (Comp_Checks,
-                    Make_Procedure_Call_Statement (Loc,
-                      Name                   =>
-                        New_Occurrence_Of (Proc_Id, Loc),
-                      Parameter_Associations => New_List (
-                        Make_Indexed_Component (Loc,
-                          Prefix      => New_Occurrence_Of (Obj_Id, Loc),
-                          Expressions => New_Copy_List (Indices)))));
+                  pragma Assert (Present (Proc_Id));
+
+                  --  Generate:
+                  --    <Comp_Typ>Invariant (_object (<Indices>));
+
+                  --  Note that the invariant procedure may have a null body if
+                  --  assertions are disabled or Assertion_Policy Ignore is in
+                  --  effect.
+
+                  if not Has_Null_Body (Proc_Id) then
+                     Append_New_To (Comp_Checks,
+                       Make_Procedure_Call_Statement (Loc,
+                         Name                   =>
+                           New_Occurrence_Of (Proc_Id, Loc),
+                         Parameter_Associations => New_List (
+                           Make_Indexed_Component (Loc,
+                             Prefix      => New_Occurrence_Of (Obj_Id, Loc),
+                             Expressions => New_Copy_List (Indices)))));
+                  end if;
                end if;
 
                Produced_Check := True;
@@ -3653,7 +3664,7 @@ package body Exp_Ch7 is
                --    end loop;
 
                --  Note that the invariant procedure may have a null body if
-               --  assertions are disabled or Assertion_Polity Ignore is in
+               --  assertions are disabled or Assertion_Policy Ignore is in
                --  effect.
 
                if Present (Comp_Checks) then
@@ -3928,33 +3939,44 @@ package body Exp_Ch7 is
             --  this case verify the access value itself.
 
             if Has_Invariants (Comp_Typ) then
-               Proc_Id := Invariant_Procedure (Base_Type (Comp_Typ));
 
-               --  The component type should have an invariant procedure if it
-               --  has invariants of its own or inherits class-wide invariants
-               --  from parent or interface types.
+               --  In GNATprove mode, the component invariants are checked by
+               --  other means. They should not be added to the record type
+               --  invariant procedure, so that the procedure can be used to
+               --  check the record type invariants if any.
 
-               pragma Assert (Present (Proc_Id));
+               if GNATprove_Mode then
+                  null;
 
-               --  Generate:
-               --    <Comp_Typ>Invariant (T (_object).<Comp_Id>);
+               else
+                  Proc_Id := Invariant_Procedure (Base_Type (Comp_Typ));
 
-               --  Note that the invariant procedure may have a null body if
-               --  assertions are disabled or Assertion_Polity Ignore is in
-               --  effect.
+                  --  The component type should have an invariant procedure
+                  --  if it has invariants of its own or inherits class-wide
+                  --  invariants from parent or interface types.
 
-               if not Has_Null_Body (Proc_Id) then
-                  Append_New_To (Comp_Checks,
-                    Make_Procedure_Call_Statement (Loc,
-                      Name                   =>
-                        New_Occurrence_Of (Proc_Id, Loc),
-                      Parameter_Associations => New_List (
-                        Make_Selected_Component (Loc,
-                          Prefix        =>
-                            Unchecked_Convert_To
-                              (T, New_Occurrence_Of (Obj_Id, Loc)),
-                          Selector_Name =>
-                            New_Occurrence_Of (Comp_Id, Loc)))));
+                  pragma Assert (Present (Proc_Id));
+
+                  --  Generate:
+                  --    <Comp_Typ>Invariant (T (_object).<Comp_Id>);
+
+                  --  Note that the invariant procedure may have a null body if
+                  --  assertions are disabled or Assertion_Policy Ignore is in
+                  --  effect.
+
+                  if not Has_Null_Body (Proc_Id) then
+                     Append_New_To (Comp_Checks,
+                       Make_Procedure_Call_Statement (Loc,
+                         Name                   =>
+                           New_Occurrence_Of (Proc_Id, Loc),
+                         Parameter_Associations => New_List (
+                           Make_Selected_Component (Loc,
+                             Prefix        =>
+                               Unchecked_Convert_To
+                                 (T, New_Occurrence_Of (Obj_Id, Loc)),
+                             Selector_Name =>
+                               New_Occurrence_Of (Comp_Id, Loc)))));
+                  end if;
                end if;
 
                Produced_Check           := True;
@@ -4667,13 +4689,19 @@ package body Exp_Ch7 is
       Set_Corresponding_Spec (Proc_Body, Proc_Id);
 
       --  The body should not be inserted into the tree when the context is
-      --  ASIS, GNATprove or a generic unit because it is not part of the
-      --  template. Note that the body must still be generated in order to
-      --  resolve the invariants.
+      --  ASIS or a generic unit because it is not part of the template. Note
+      --  that the body must still be generated in order to resolve the
+      --  invariants.
 
-      if ASIS_Mode or GNATprove_Mode or Inside_A_Generic then
+      if ASIS_Mode or Inside_A_Generic then
          null;
 
+      --  Semi-insert the body into the tree for GNATprove by setting its
+      --  Parent field. This allows for proper upstream tree traversals.
+
+      elsif GNATprove_Mode then
+         Set_Parent (Proc_Body, Parent (Declaration_Node (Work_Typ)));
+
       --  Otherwise the body is part of the freezing actions of the type
 
       else
@@ -4865,12 +4893,17 @@ package body Exp_Ch7 is
                     New_Occurrence_Of (Work_Typ, Loc)))));
 
       --  The declaration should not be inserted into the tree when the context
-      --  is ASIS, GNATprove or a generic unit because it is not part of the
-      --  template.
+      --  is ASIS or a generic unit because it is not part of the template.
 
-      if ASIS_Mode or GNATprove_Mode or Inside_A_Generic then
+      if ASIS_Mode or Inside_A_Generic then
          null;
 
+      --  Semi-insert the declaration into the tree for GNATprove by setting
+      --  its Parent field. This allows for proper upstream tree traversals.
+
+      elsif GNATprove_Mode then
+         Set_Parent (Proc_Decl, Parent (Typ_Decl));
+
       --  Otherwise insert the declaration
 
       else
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index 2a453fe..fcbf994 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -2439,9 +2439,15 @@ package body Freeze is
             end if;
 
             --  The array type requires its own invariant procedure in order to
-            --  verify the component invariant over all elements.
-
-            if Has_Invariants (Component_Type (Arr)) then
+            --  verify the component invariant over all elements. In GNATprove
+            --  mode, the component invariants are checked by other means. They
+            --  should not be added to the array type invariant procedure, so
+            --  that the procedure can be used to check the array type
+            --  invariants if any.
+
+            if Has_Invariants (Component_Type (Arr))
+              and then not GNATprove_Mode
+            then
                Set_Has_Own_Invariants (Arr);
 
                --  The array type is an implementation base type. Propagate the
@@ -4362,9 +4368,14 @@ package body Freeze is
                --  order to verify the invariant of each individual component.
                --  Do not consider internal components such as _parent because
                --  parent class-wide invariants are always inherited.
+               --  In GNATprove mode, the component invariants are checked by
+               --  other means. They should not be added to the record type
+               --  invariant procedure, so that the procedure can be used to
+               --  check the recordy type invariants if any.
 
                if Comes_From_Source (Comp)
                  and then Has_Invariants (Etype (Comp))
+                   and then not GNATprove_Mode
                then
                   Set_Has_Own_Invariants (Rec);
                end if;