gcc.gnu.org Git - gcc.git/commit

]> gcc.gnu.org Git - gcc.git/commit

author	Yannick Moy <moy@adacore.com>
	Fri, 3 Sep 2021 07:19:49 +0000 (09:19 +0200)
committer	Pierre-Marie de Rodat <derodat@adacore.com>
	Mon, 4 Oct 2021 08:45:10 +0000 (08:45 +0000)
commit	a5740f2b7285f950e68d7790c37e28a5b768b4e8
tree	38a8dee53c0fd9be033acf6155bf44d54b9e58bd	tree
parent	39d7ff0fd7487bfb188f9e4c186076a106f995f8	commit \| 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 \| blame \| history
gcc/ada/libgnat/a-textio.ads		diff \| blob \| blame \| history
gcc/ada/sem.adb		diff \| blob \| blame \| history

GNU Compiler Collection

RSS Atom

This page took 0.05351 seconds and 5 git commands to generate.