diff options
| author | Yannick Moy <moy@adacore.com> | 2021-09-03 09:19:49 +0200 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-10-04 08:45:10 +0000 |
| commit | a5740f2b7285f950e68d7790c37e28a5b768b4e8 (patch) | |
| tree | 38a8dee53c0fd9be033acf6155bf44d54b9e58bd /gcc/expr.c | |
| parent | 39d7ff0fd7487bfb188f9e4c186076a106f995f8 (diff) | |
| download | gcc-a5740f2b7285f950e68d7790c37e28a5b768b4e8.zip gcc-a5740f2b7285f950e68d7790c37e28a5b768b4e8.tar.gz gcc-a5740f2b7285f950e68d7790c37e28a5b768b4e8.tar.bz2 | |
[Ada] Mark Ada.Text_IO in SPARK
gcc/ada/
* libgnat/a-textio.adb: Mark body out of SPARK.
* libgnat/a-textio.ads: Mark spec in SPARK and private part out
of SPARK.
* sem.adb (Semantics.Do_Analyze): Similar to ghost code
attributes, save and restore value of
Ignore_SPARK_Mode_Pragmas_In_Instance.
Diffstat (limited to 'gcc/expr.c')
0 files changed, 0 insertions, 0 deletions