exp_ch7.adb (Build_Invariant_Procedure_Body): Semi-insert the body into the tree...
authorClaire Dross <dross@adacore.com>
Thu, 19 Jan 2017 13:08:16 +0000 (13:08 +0000)
committerArnaud Charlet <charlet@gcc.gnu.org>
Thu, 19 Jan 2017 13:08:16 +0000 (14:08 +0100)
commit104c99ef18d7f5550ef18ca443dc2e4b2ac1641a
tree1b2d3ee78f60b1dd2b9a6527f3936ecbb8d3ad00
parent374c09e8b0560f150266deb324004e482f4c424e
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
gcc/ada/ChangeLog
gcc/ada/exp_ch7.adb
gcc/ada/freeze.adb