exp_ch7.adb (Build_Invariant_Procedure_Body): Semi-insert the body into the tree...

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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index ba2c1207e28e2fe2255f6218478416b82bfcb299..9743e60bf2c7b86e205772bca33114ee59f0dab6 100644 (file)
--- 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 0c2180847bae3e0c856919b34f58f476284c028b..93573a29ea349d69979be5f0acfb17376aa77af4 100644 (file)
--- 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 2a453fe0020ee1ce2a73d7bad04549dca54edbb3..fcbf994df82a8e3cab556da63c6c76e89bd8d116 100644 (file)
--- 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;