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
This commit is contained in:
Claire Dross
Arnaud Charlet
parent
374c09e8b0
commit
104c99ef18
@ -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.
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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;
|
||||
|
||||
Loading…
Reference in New Issue
Block a user