projects / platform / upstream / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 39d7ff0) | patch
[Ada] Mark Ada.Text_IO in SPARK
authorYannick Moy <moy@adacore.com>
Fri, 3 Sep 2021 07:19:49 +0000 (09:19 +0200)
committerPierre-Marie de Rodat <derodat@adacore.com>
Mon, 4 Oct 2021 08:45:10 +0000 (08:45 +0000)
commita5740f2b7285f950e68d7790c37e28a5b768b4e8
tree38a8dee53c0fd9be033acf6155bf44d54b9e58bdtree | snapshot
parent39d7ff0fd7487bfb188f9e4c186076a106f995f8commit | diff
[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.
gcc/ada/libgnat/a-textio.adb diff | blob | history
gcc/ada/libgnat/a-textio.ads diff | blob | history
gcc/ada/sem.adb diff | blob | history
Domain: System / Toolchain;