diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2018-01-11 08:52:43 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2018-01-11 08:52:43 +0000 |
| commit | 210fef2d1c7b47c0587375d87d4f4a65f28ca57e (patch) | |
| tree | 438021dd8743590fef0f8530f4733004adeeef89 /gcc/ada/cstreams.c | |
| parent | 7d1553e2b65506288b554e948856e9330cee3e5f (diff) | |
| download | gcc-210fef2d1c7b47c0587375d87d4f4a65f28ca57e.zip gcc-210fef2d1c7b47c0587375d87d4f4a65f28ca57e.tar.gz gcc-210fef2d1c7b47c0587375d87d4f4a65f28ca57e.tar.bz2 | |
[Ada] Annotate standard File_Type with Default_Initial_Condition (for SPARK)
GNATprove was emitting spurious checks about objects of the File_Type being
uninitialized and there was no easy to fix that (those checks could only be
silenced by pragma Annotate or by hiding File_Type behind as SPARK wrapper).
Now the full view of File_Type is annotated with Default_Initial_Condition
and GNATprove knows that objects of that type are default-initialized. The
default initialization is implicitly defined in the Ada RM (as indeed
there is no procedure that would take an IN OUT parameter of that type).
Semantics of Ada programs shall not be affected by these annotations,
so no frontend test is provided. It only affects GNATprove.
2018-01-11 Piotr Trojanek <trojanek@adacore.com>
gcc/ada/
* libgnat/a-direio.ads, libgnat/a-sequio.ads, libgnat/a-ststio.ads,
libgnat/a-textio.ads, libgnat/a-witeio.ads, libgnat/a-ztexio.ads
(File_Type): Add Default_Initial_Condition aspect.
From-SVN: r256502
Diffstat (limited to 'gcc/ada/cstreams.c')
0 files changed, 0 insertions, 0 deletions