diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index ba2c1207e28e..9743e60bf2c7 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,21 @@ +2017-01-19 Claire Dross + + * 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 * lib-xref-spark_specific.adb: Minor reformatting. diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb index 0c2180847bae..93573a29ea34 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: - -- Invariant (_object ()); + 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: + -- Invariant (_object ()); + + -- 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: - -- Invariant (T (_object).); + 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: + -- Invariant (T (_object).); + + -- 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 2a453fe0020e..fcbf994df82a 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. + -- 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)) then + 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;