-
- Downloads
ada: Fix propagation of SPARK_Mode for renaming-as-body
The value of SPARK_Mode associated with a renaming-as-body might not be the correct one, when the private part of the package containing the declaration has SPARK_Mode Off while the public part has SPARK_Mode On. This may lead to analysis of code by GNATprove that should not be analyzed. gcc/ada/ * freeze.adb (Build_Renamed_Body): Propagate SPARK_Pragma to body build from renaming, so that locally relevant value is taken into account. * sem_ch6.adb (Analyze_Expression_Function): Propagate SPARK_Pragma to body built from expression function, so that locally relevant value is taken into account.
Loading
Please register or sign in to comment