diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2020-02-25 13:58:04 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2020-06-09 04:09:00 -0400 |
| commit | 6859ef489341d436ebf2fd5d41282c4f68b0283d (patch) | |
| tree | 9e9e8df800575371cb6aac225f0c06e947d87417 /gcc/debug.c | |
| parent | 3795dac6fa7e6514cdc4daa138e29d5a4f4d001e (diff) | |
| download | gcc-6859ef489341d436ebf2fd5d41282c4f68b0283d.zip gcc-6859ef489341d436ebf2fd5d41282c4f68b0283d.tar.gz gcc-6859ef489341d436ebf2fd5d41282c4f68b0283d.tar.bz2 | |
[Ada] Annotate Ada.Synchronous_Barriers with SPARK_Mode => Off
2020-06-09 Piotr Trojanek <trojanek@adacore.com>
gcc/ada/
* libgnarl/a-synbar.ads, libgnarl/a-synbar.adb,
libgnarl/a-synbar__posix.ads, libgnarl/a-synbar__posix.adb
(Ada.Synchronous_Barriers): Annotate with SPARK_Mode => Off.
Diffstat (limited to 'gcc/debug.c')
0 files changed, 0 insertions, 0 deletions