From f5da7a97f59ad934df6fd6ab1aca0a48571ae399 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Mon, 20 Jan 2014 13:44:07 +0000 Subject: 2014-01-20 Yannick Moy * adabkend.adb, ali-util.adb, errout.adb, exp_ch7.adb, * exp_dbug.adb, freeze.adb, lib-xref.adb, restrict.adb, * sem_attr.adb, sem_ch4.adb, sem_ch5.adb, sem_ch6.adb, sem_ch8.adb, * sem_prag.adb, sem_res.adb, sem_util.adb Rename SPARK_Mode into GNATprove_Mode. * sem_ch13.adb: Remove blank. * exp_spark.adb, exp_spark.ads (Expand_SPARK_Call): Only replace subprograms by alias for renamings, not for inherited primitive operations. * exp_util.adb (Expand_Subtype_From_Expr): Apply the expansion in GNATprove mode. (Remove_Side_Effects): Apply the removal in GNATprove mode, for the full analysis of expressions. * expander.adb (Expand): Call the light SPARK expansion in GNATprove mode. (Expander_Mode_Restore, Expander_Mode_Save_And_Set): Ignore save/restore actions for Expander_Active flag in GNATprove mode, similar to what is done in ASIS mode. * frontend.adb (Frontend): Generic bodies are instantiated in GNATprove mode. * gnat1drv.adb (Adjust_Global_Switches): Set operating mode to Check_Semantics in GNATprove mode, although a light expansion is still performed. (Gnat1drv): Set Back_End_Mode to Declarations_Only in GNATprove mode, and later on special case the GNATprove mode to continue analysis anyway. * lib-writ.adb (Write_ALI): Always generate ALI files in GNATprove mode. * opt.adb, opt.ads (Full_Expander_Active): Make it equivalent to Expander_Active. (SPARK_Mode): Renamed as GNATprove_Mode. * sem_aggr.adb (Aggregate_Constraint_Checks): Add checks in the tree in GNATprove_Mode. * sem_ch12.adb (Analyze_Package_Instantiation): Always instantiate body in GNATprove mode. (Need_Subprogram_Instance_Body): Always instantiate body in GNATprove mode. * sem_ch3.adb (Constrain_Index, Process_Range_Expr_In_Decl): Make sure side effects are removed in GNATprove mode. From-SVN: r206805 --- gcc/ada/expander.adb | 26 ++++++++++++++------------ 1 file changed, 14 insertions(+), 12 deletions(-) (limited to 'gcc/ada/expander.adb') diff --git a/gcc/ada/expander.adb b/gcc/ada/expander.adb index a037dd3..1fd1bc8 100644 --- a/gcc/ada/expander.adb +++ b/gcc/ada/expander.adb @@ -88,8 +88,9 @@ package body Expander is -- The first is when are not generating code. In this mode the -- Full_Analysis flag indicates whether we are performing a complete -- analysis, in which case Full_Analysis = True or a pre-analysis in - -- which case Full_Analysis = False. See the spec of Sem for more - -- info on this. + -- which case Full_Analysis = False. See the spec of Sem for more info + -- on this. Additionally, the GNATprove_Mode flag indicates that a light + -- expansion for formal verification should be used. -- -- The second reason for the Expander_Active flag to be False is that -- we are performing a pre-analysis. During pre-analysis all expansion @@ -107,7 +108,7 @@ package body Expander is -- given that the expansion actions that would normally process it will -- not take place. This prevents cascaded errors due to stack mismatch. - if not Expander_Active then + if not (Expander_Active or (Full_Analysis and GNATprove_Mode)) then Set_Analyzed (N, Full_Analysis); if Serious_Errors_Detected > 0 @@ -127,10 +128,11 @@ package body Expander is Debug_A_Entry ("expanding ", N); begin - -- In SPARK mode we only need a very limited subset of the usual - -- expansions. This limited subset is implemented in Expand_SPARK. + -- In GNATprove mode we only need a very limited subset of + -- the usual expansions. This limited subset is implemented + -- in Expand_SPARK. - if SPARK_Mode then + if GNATprove_Mode then Expand_SPARK (N); -- Here for normal non-SPARK mode @@ -503,10 +505,10 @@ package body Expander is procedure Expander_Mode_Restore is begin - -- Not active (has no effect) in ASIS mode (see comments in spec of - -- Expander_Mode_Save_And_Set). + -- Not active (has no effect) in ASIS and GNATprove modes (see comments + -- in spec of Expander_Mode_Save_And_Set). - if ASIS_Mode then + if ASIS_Mode or GNATprove_Mode then return; end if; @@ -530,10 +532,10 @@ package body Expander is procedure Expander_Mode_Save_And_Set (Status : Boolean) is begin - -- Not active (has no effect) in ASIS mode (see comments in spec of - -- Expander_Mode_Save_And_Set). + -- Not active (has no effect) in ASIS and GNATprove modes (see comments + -- in spec of Expander_Mode_Save_And_Set). - if ASIS_Mode then + if ASIS_Mode or GNATprove_Mode then return; end if; -- cgit v1.1