diff options
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/freeze.adb | 7 | ||||
| -rw-r--r-- | gcc/ada/sem_ch6.adb | 9 |
2 files changed, 16 insertions, 0 deletions
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index c8d20d0..a947018 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -586,6 +586,13 @@ package body Freeze is Next (Param_Spec); end loop; + -- Copy SPARK pragma from renaming declaration + + Set_SPARK_Pragma + (Defining_Unit_Name (Spec), SPARK_Pragma (New_S)); + Set_SPARK_Pragma_Inherited + (Defining_Unit_Name (Spec), SPARK_Pragma_Inherited (New_S)); + -- In GNATprove, prefer to generate an expression function whenever -- possible, to benefit from the more precise analysis in that case -- (as if an implicit postcondition had been generated). diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 0988fad..d3912ff 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -333,6 +333,15 @@ package body Sem_Ch6 is New_Spec := Copy_Subprogram_Spec (Spec); Prev := Current_Entity_In_Scope (Defining_Entity (Spec)); + -- Copy SPARK pragma from expression function + + Set_SPARK_Pragma + (Defining_Unit_Name (New_Spec), + SPARK_Pragma (Defining_Unit_Name (Spec))); + Set_SPARK_Pragma_Inherited + (Defining_Unit_Name (New_Spec), + SPARK_Pragma_Inherited (Defining_Unit_Name (Spec))); + -- If there are previous overloadable entities with the same name, -- check whether any of them is completed by the expression function. -- In a generic context a formal subprogram has no completion. |