[Ada] Create explicit ghost mirror unit for big integers
Pierre-Marie de Rodat
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...
Size: 5236 bytes
Desc: not available
More information about the Gcc-patches