From 27bb79414764b83bf6c7208d6081afd01f98869f Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Fri, 13 Jan 2017 10:59:17 +0100 Subject: [multiple changes] 2017-01-13 Hristian Kirtchev * exp_util.adb (Add_Inherited_Tagged_DIC): Pass the object parameters of both the parent and the derived type DIC procedure to the reference replacement circuitry. (Find_DIC_Type): Modify the circuitry to present the partial view of a private type in case the private type defines its own DIC pragma. (Replace_Object_And_Primitive_References): Add two optional formal parameters. Update the comment on usage. Update the replacement of references to object parameters. 2017-01-13 Gary Dismukes * einfo.adb, sem_ch6.adb, atree.adb: Minor reformatting and typo fix. 2017-01-13 Ed Schonberg * sem_res.adb (Resolve_Actuals): Apply Scalar_Range_Check to an out parameter that is a type conversion, independently of th range check that may apply to the expression of the conversion, for use in GNATProve. 2017-01-13 Yannick Moy * gnat1drv.adb (Gnat1drv): Move the implicit with for System in GNATprove_Mode here to Frontend. * frontend.adb (Frontend): Move the implicit with for System in GNATprove_Mode here as it ismore correct this way; the old place only worked by chance, since there were no overloaded names. * rtsfind.ads (RE_Id, RE_Unit_Table): Add RE_Tasking_State. * sem_attr.adb (Analyze_Attribute): In GNATprove_Mode, for the four attributes identified in SRM 9(18), add an implicit with to Ada.Task_Identification. * sem_ch8.adb (Analyze_Subprogram_Renaming.Build_Class_Wide_Wrapper): Deal specially with the wrapper introduced for AI05-0071 in GNATprove mode. * checks.adb (Apply_Discriminant_Check, Apply_Selected_Length_Checks, Apply_Selected_Range_Checks): In GNATprove mode, we do not apply the checks, but we still analyze the expression to possibly issue errors on SPARK code when a run-time error can be detected at compile time. (Selected_Length_Checks, Selected_Range_Checks): Perform analysis in GNATprove mode. From-SVN: r244398 --- gcc/ada/sem_attr.adb | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) (limited to 'gcc/ada/sem_attr.adb') diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 494579a..9adbe7a 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -7109,6 +7109,27 @@ package body Sem_Attr is end case; + -- In SPARK some attribute references depend on Tasking_State, so we + -- need to make sure we load this so that gnat2why has the entity + -- available. See SPARK RM 9(18) for the relevant rule. + + if GNATprove_Mode then + declare + Unused : Entity_Id; + begin + case Attr_Id is + when Attribute_Callable | + Attribute_Caller | + Attribute_Count | + Attribute_Terminated => + Unused := RTE (RE_Tasking_State); + + when others => + null; + end case; + end; + end if; + -- All errors raise Bad_Attribute, so that we get out before any further -- damage occurs when an error is detected (for example, if we check for -- one attribute expression, and the check succeeds, we want to be able -- cgit v1.1