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/lib-writ.adb | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'gcc/ada/lib-writ.adb') diff --git a/gcc/ada/lib-writ.adb b/gcc/ada/lib-writ.adb index f794162..015c628 100644 --- a/gcc/ada/lib-writ.adb +++ b/gcc/ada/lib-writ.adb @@ -841,7 +841,7 @@ package body Lib.Writ is -- files, which are required to compute frame conditions -- of subprograms. - or else SPARK_Mode + or else GNATprove_Mode then Write_Info_Tab (25); @@ -973,9 +973,10 @@ package body Lib.Writ is -- If we are not generating code, and there is an up to date ALI file -- file accessible, read it, and acquire the compilation arguments from - -- this file. + -- this file. In GNATprove mode, always generate the ALI file, which + -- contains a special section for formal verification. - if Operating_Mode /= Generate_Code then + if Operating_Mode /= Generate_Code and then not GNATprove_Mode then if Up_To_Date_ALI_File_Exists then Update_Tables_From_ALI_File; return; @@ -1488,7 +1489,7 @@ package body Lib.Writ is -- Output SPARK cross-reference information if needed - if Opt.Xref_Active and then SPARK_Mode then + if Opt.Xref_Active and then GNATprove_Mode then SPARK_Specific.Collect_SPARK_Xrefs (Sdep_Table => Sdep_Table, Num_Sdep => Num_Sdep); SPARK_Specific.Output_SPARK_Xrefs; -- cgit v1.1