aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/gcc-interface
diff options
context:
space:
mode:
authorYannick Moy <moy@adacore.com>2022-06-10 17:18:23 +0200
committerPierre-Marie de Rodat <derodat@adacore.com>2022-07-06 13:29:48 +0000
commitbe3bdaa1a53beaa5bb881c079ceaae132fb422a6 (patch)
tree8c1ee1b1cce7b99e11d0ce4e94542a4b343a8822 /gcc/ada/gcc-interface
parent28add0a4c82f52631b434e1e126588cd3f5b7782 (diff)
downloadgcc-be3bdaa1a53beaa5bb881c079ceaae132fb422a6.zip
gcc-be3bdaa1a53beaa5bb881c079ceaae132fb422a6.tar.gz
gcc-be3bdaa1a53beaa5bb881c079ceaae132fb422a6.tar.bz2
[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.
Diffstat (limited to 'gcc/ada/gcc-interface')
0 files changed, 0 insertions, 0 deletions