[Ada] Support ghost generic formal parameters
commitbe3bdaa1a53beaa5bb881c079ceaae132fb422a6
authorYannick Moy <moy@adacore.com>
Fri, 10 Jun 2022 15:18:23 +0000 (10 17:18 +0200)
committerPierre-Marie de Rodat <derodat@adacore.com>
Wed, 6 Jul 2022 13:29:48 +0000 (6 13:29 +0000)
tree8c1ee1b1cce7b99e11d0ce4e94542a4b343a8822
parent28add0a4c82f52631b434e1e126588cd3f5b7782
[Ada] Support ghost generic formal parameters

This adds support in GNAT for ghost generic formal parameters, as
included in SPARK RM 6.9.

gcc/ada/

* ghost.adb (Check_Ghost_Context): Delay checking for generic
associations.
(Check_Ghost_Context_In_Generic_Association): Perform ghost
checking in analyzed generic associations.
(Check_Ghost_Formal_Procedure_Or_Package): Check SPARK RM
6.9(13-14) for formal procedures and packages.
(Check_Ghost_Formal_Variable): Check SPARK RM 6.9(13-14) for
variables.
* ghost.ads: Declarations for the above.
* sem_ch12.adb (Analyze_Associations): Apply delayed checking
for generic associations.
(Analyze_Formal_Object_Declaration): Same.
(Analyze_Formal_Subprogram_Declaration): Same.
(Instantiate_Formal_Package): Same.
(Instantiate_Formal_Subprogram): Same.
(Instantiate_Object): Same.  Copy ghost aspect to newly declared
object for actual for IN formal object. Use new function
Get_Enclosing_Deep_Object to retrieve root object.
(Instantiate_Type): Copy ghost aspect to declared subtype for
actual for formal type.
* sem_prag.adb (Analyze_Pragma): Recognize new allowed
declarations.
* sem_util.adb (Copy_Ghost_Aspect): Copy the ghost aspect
between nodes.
(Get_Enclosing_Deep_Object): New function to return enclosing
deep object (or root for reachable part).
* sem_util.ads (Copy_Ghost_Aspect): Same.
(Get_Enclosing_Deep_Object): Same.
* libgnat/s-imageu.ads: Declare formal subprograms as ghost.
* libgnat/s-valuei.ads: Same.
* libgnat/s-valuti.ads: Same.
gcc/ada/ghost.adb
gcc/ada/ghost.ads
gcc/ada/libgnat/s-imageu.ads
gcc/ada/libgnat/s-valuei.ads
gcc/ada/libgnat/s-valuti.ads
gcc/ada/sem_ch12.adb
gcc/ada/sem_prag.adb
gcc/ada/sem_util.adb
gcc/ada/sem_util.ads