From: Claire Dross Date: Thu, 19 Jan 2017 13:08:16 +0000 (+0000) Subject: exp_ch7.adb (Build_Invariant_Procedure_Body): Semi-insert the body into the tree... X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=104c99ef18d7f5550ef18ca443dc2e4b2ac1641a;p=gcc.git 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 * 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 ba2c1207e28..9743e60bf2c 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 0c2180847ba..93573a29ea3 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 2a453fe0020..fcbf994df82 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;