diff options
| author | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-07-29 15:58:21 +0200 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-07-29 15:58:21 +0200 |
| commit | 09d67391ff9fa5a74a2bf727a50b5199b736fdb0 (patch) | |
| tree | 5d8176dc3daee5dedd24243aaf1340859163f408 /gcc/ada/sinfo.ads | |
| parent | c93af807041bbb683207b8f2025b2641a14469c5 (diff) | |
| download | gcc-09d67391ff9fa5a74a2bf727a50b5199b736fdb0.zip gcc-09d67391ff9fa5a74a2bf727a50b5199b736fdb0.tar.gz gcc-09d67391ff9fa5a74a2bf727a50b5199b736fdb0.tar.bz2 | |
[multiple changes]
2014-07-29 Thomas Quinot <quinot@adacore.com>
* gnat_rm.texi: Document internal attributes used for PolyORB/DSA
distributed stubs generation.
* exp_ch3.adb: Minor reformatting.
2014-07-29 Yannick Moy <moy@adacore.com>
* sinfo.ads: Document constraint between frontend and GNATprove.
From-SVN: r213193
Diffstat (limited to 'gcc/ada/sinfo.ads')
| -rw-r--r-- | gcc/ada/sinfo.ads | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index 479eb6e..dc1d1c5 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -562,12 +562,20 @@ package Sinfo is -- not make sense from a user point-of-view, and that cross-references that -- do not lead to data dependences for subprograms can be safely ignored. - -- In addition pragma Debug statements are removed from the tree (rewritten - -- to NULL stmt), since they should be ignored in formal verification. + -- GNATprove relies on the following frontend behaviors: - -- An error is also issued for missing subunits, similar to the warning - -- issued when generating code, to avoid formal verification of a partial - -- unit. + -- 1. The first declarations in the list of visible declarations of + -- a package declaration for a generic instance, up to the first + -- declaration which comes from source, should correspond to + -- the "mappings nodes" between formal and actual generic parameters. + + -- 2. In addition pragma Debug statements are removed from the tree + -- (rewritten to NULL stmt), since they should be ignored in formal + -- verification. + + -- 3. An error is also issued for missing subunits, similar to the + -- warning issued when generating code, to avoid formal verification + -- of a partial unit. ----------------------- -- Check Flag Fields -- |