diff options
| author | Claire Dross <dross@adacore.com> | 2017-01-19 13:08:16 +0000 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2017-01-19 14:08:16 +0100 |
| commit | 104c99ef18d7f5550ef18ca443dc2e4b2ac1641a (patch) | |
| tree | 1b2d3ee78f60b1dd2b9a6527f3936ecbb8d3ad00 /gcc/config.gcc | |
| parent | 374c09e8b0560f150266deb324004e482f4c424e (diff) | |
| download | gcc-104c99ef18d7f5550ef18ca443dc2e4b2ac1641a.zip gcc-104c99ef18d7f5550ef18ca443dc2e4b2ac1641a.tar.gz gcc-104c99ef18d7f5550ef18ca443dc2e4b2ac1641a.tar.bz2 | |
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
Diffstat (limited to 'gcc/config.gcc')
0 files changed, 0 insertions, 0 deletions