[Ada] Create explicit ghost mirror unit for big integers

Pierre-Marie de Rodat derodat@adacore.com
Wed Nov 10 08:58:31 GMT 2021

So far, only one light runtime units was using the standard unit for
big integers. A special ghost mirror had been created for the reduced
runtimes. In order to use more liberally big integers for proof of the
runtime, rename this ghost mirror into Big_Integers_Ghost at the same
level in the hierarchy of units as Big_Integers.

Tested on x86_64-pc-linux-gnu, committed on trunk


	* Makefile.rtl: Add unit.
	* libgnat/a-nbnbin__ghost.adb: Move...
	* libgnat/a-nbnbig.adb: ... here. Mark ghost as ignored.
	* libgnat/a-nbnbin__ghost.ads: Move...
	* libgnat/a-nbnbig.ads: ... here.  Add comment for purpose of
	this unit. Mark ghost as ignored.
	* libgnat/s-widthu.adb: Use new unit.
	* sem_aux.adb (First_Subtype): Adapt to the case of a ghost type
	whose freeze node is rewritten to a null statement.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: patch.diff
Type: text/x-diff
Size: 5236 bytes
Desc: not available
URL: <https://gcc.gnu.org/pipermail/gcc-patches/attachments/20211110/94ea50e3/attachment-0001.bin>

More information about the Gcc-patches mailing list