From: charlet Date: Mon, 20 Jan 2014 13:44:07 +0000 (+0000) Subject: 2014-01-20 Yannick Moy X-Git-Tag: upstream/4.9.2~1739 X-Git-Url: http://review.tizen.org/git/?a=commitdiff_plain;h=c39cce408b9bbfdd8c3bf5851b6c8a6abd1e00a1;p=platform%2Fupstream%2Flinaro-gcc.git 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. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@206805 138bc75d-0d04-0410-961f-82ee72b054a4 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index bf0e299..06ed0b9 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,45 @@ +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. + 2014-01-20 Eric Botcazou * gcc-interface/decl.c (gnat_to_gnu_entity) : Robustify tests diff --git a/gcc/ada/adabkend.adb b/gcc/ada/adabkend.adb index 4a77920..4c70a56 100644 --- a/gcc/ada/adabkend.adb +++ b/gcc/ada/adabkend.adb @@ -235,12 +235,12 @@ package body Adabkend is if Is_Switch (Argv) then Fail ("Object file name missing after -gnatO"); - -- In SPARK_Mode, such an object file is never written, and the - -- call to Set_Output_Object_File_Name may fail (e.g. when the - -- object file name does not have the expected suffix). So we - -- skip that call when SPARK_Mode is set. + -- In GNATprove_Mode, such an object file is never written, and + -- the call to Set_Output_Object_File_Name may fail (e.g. when + -- the object file name does not have the expected suffix). So + -- we skip that call when GNATprove_Mode is set. - elsif SPARK_Mode then + elsif GNATprove_Mode then Output_File_Name_Seen := True; else diff --git a/gcc/ada/ali-util.adb b/gcc/ada/ali-util.adb index 92380f8..98f79ba 100644 --- a/gcc/ada/ali-util.adb +++ b/gcc/ada/ali-util.adb @@ -274,11 +274,11 @@ package body ALI.Util is Error_Msg ("{ had errors, must be fixed, and recompiled"); Set_Name_Table_Info (Afile, Int (No_Unit_Id)); - -- In formal verification mode, object files are never - -- generated, so No_Object=True is not considered an error. + -- In GNATprove mode, object files are never generated, so + -- No_Object=True is not considered an error. elsif ALIs.Table (Idread).No_Object - and then not SPARK_Mode + and then not GNATprove_Mode and then not Ignore_Errors then Error_Msg_File_1 := Withs.Table (W).Sfile; diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb index 2c783b2..ab4dcfe 100644 --- a/gcc/ada/errout.adb +++ b/gcc/ada/errout.adb @@ -239,7 +239,7 @@ package body Errout is -- an error status. These errors are handled in the driver of the -- verification process instead. - elsif SPARK_Mode and not Frame_Condition_Mode then + elsif GNATprove_Mode and not Frame_Condition_Mode then return False; else @@ -2970,7 +2970,7 @@ package body Errout is -- Suppress "size too small" errors in CodePeer mode and SPARK mode, -- since pragma Pack is also ignored in these configurations. - if CodePeer_Mode or SPARK_Mode then + if CodePeer_Mode or GNATprove_Mode then return True; -- When a size is wrong for a frozen type there is no explicit size diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb index 8449f6a..a523858 100644 --- a/gcc/ada/exp_ch7.adb +++ b/gcc/ada/exp_ch7.adb @@ -937,7 +937,7 @@ package body Exp_Ch7 is -- Do not create finalization masters in SPARK mode because they result -- in unwanted expansion. - elsif SPARK_Mode then + elsif GNATprove_Mode then return; end if; @@ -2813,7 +2813,7 @@ package body Exp_Ch7 is -- Do not perform this expansion in SPARK mode because it is not -- necessary. - if SPARK_Mode then + if GNATprove_Mode then return; end if; @@ -2975,7 +2975,7 @@ package body Exp_Ch7 is -- Do not perform this expansion in SPARK mode because we do not create -- finalizers in the first place. - if SPARK_Mode then + if GNATprove_Mode then return; end if; @@ -3658,7 +3658,7 @@ package body Exp_Ch7 is -- this node and enclosed expression are not expanded, so do not apply -- any transformations here. - elsif SPARK_Mode + elsif GNATprove_Mode and then Nkind (Wrap_Node) = N_Pragma and then Get_Pragma_Id (Wrap_Node) = Pragma_Check then diff --git a/gcc/ada/exp_dbug.adb b/gcc/ada/exp_dbug.adb index 7dd7206..7d74ed1 100644 --- a/gcc/ada/exp_dbug.adb +++ b/gcc/ada/exp_dbug.adb @@ -1314,7 +1314,7 @@ package body Exp_Dbug is -- name as being qualified, as Qualify_Entity_Name may be called more -- than once on the same entity. - elsif SPARK_Mode then + elsif GNATprove_Mode then if Has_Homonym (Ent) then Get_Name_String (Chars (Ent)); Append_Homonym_Number (Ent); diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb index a4415e8..fb7aad2 100644 --- a/gcc/ada/exp_spark.adb +++ b/gcc/ada/exp_spark.adb @@ -31,7 +31,6 @@ with Sem_Aux; use Sem_Aux; with Sem_Res; use Sem_Res; with Sem_Util; use Sem_Util; with Sinfo; use Sinfo; -with Stand; use Stand; package body Exp_SPARK is @@ -94,51 +93,28 @@ package body Exp_SPARK is ----------------------- procedure Expand_SPARK_Call (N : Node_Id) is - Call_Node : constant Node_Id := N; - Parent_Subp : Entity_Id; - begin - -- Ignore if previous error - - if Nkind (Call_Node) in N_Has_Etype - and then Etype (Call_Node) = Any_Type - then - return; - end if; - - -- Call using access to subprogram with explicit dereference - - if Nkind (Name (Call_Node)) = N_Explicit_Dereference then - Parent_Subp := Empty; - - -- Case of call to simple entry, where the Name is a selected component - -- whose prefix is the task, and whose selector name is the entry name - - elsif Nkind (Name (Call_Node)) = N_Selected_Component then - Parent_Subp := Empty; - - -- Case of call to member of entry family, where Name is an indexed - -- component, with the prefix being a selected component giving the - -- task and entry family name, and the index being the entry index. - - elsif Nkind (Name (Call_Node)) = N_Indexed_Component then - Parent_Subp := Empty; - - -- Normal case - - else - Parent_Subp := Alias (Entity (Name (Call_Node))); - end if; - -- If the subprogram is a renaming, replace it in the call with the name - -- of the actual subprogram being called. - - if Present (Parent_Subp) then - Parent_Subp := Ultimate_Alias (Parent_Subp); - - -- The below setting of Entity is suspect, see F109-018 discussion??? - - Set_Entity (Name (Call_Node), Parent_Subp); + -- of the actual subprogram being called. We distinguish renamings from + -- inherited primitive operations, which both have an Alias component, + -- by looking at the parent node of the entity. The entity for a + -- renaming has the function or procedure specification node as + -- parent, while an inherited primitive operation has the derived + -- type declaration as parent. + + if Nkind (Name (N)) in N_Has_Entity + and then Present (Entity (Name (N))) + then + declare + E : constant Entity_Id := Entity (Name (N)); + begin + if Nkind_In (Parent (E), N_Function_Specification, + N_Procedure_Specification) + and then Present (Alias (E)) + then + Set_Entity (Name (N), Ultimate_Alias (E)); + end if; + end; end if; end Expand_SPARK_Call; diff --git a/gcc/ada/exp_spark.ads b/gcc/ada/exp_spark.ads index c422bc7..750d66b 100644 --- a/gcc/ada/exp_spark.ads +++ b/gcc/ada/exp_spark.ads @@ -23,10 +23,9 @@ -- -- ------------------------------------------------------------------------------ --- This package implements a light expansion which is used in formal --- verification mode (SPARK_Mode = True). Instead of a complete expansion --- of nodes for code generation, this SPARK expansion targets generation --- of intermediate code for formal verification. +-- This package implements a light expansion which is used in GNATprove mode. +-- Instead of a complete expansion of nodes for code generation, this light +-- expansion targets generation of intermediate code for formal verification. -- Expand_SPARK is called directly by Expander.Expand. diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index a14b1bc..5bac112 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -2034,12 +2034,22 @@ package body Exp_Util is -- may be constants that depend on the bounds of a string literal, both -- standard string types and more generally arrays of characters. - if not Expander_Active + -- In GNATprove mode, we also need the more precise subtype to be set. + + if not (Expander_Active or GNATprove_Mode) and then (No (Etype (Exp)) or else not Is_String_Type (Etype (Exp))) then return; end if; + -- In GNATprove mode, Unc_Type might not be complete when analyzing + -- a generic unit. As generic units are not analyzed directly in + -- GNATprove, return here rather than failing later. + + if GNATprove_Mode and then No (Underlying_Type (Unc_Type)) then + return; + end if; + if Nkind (Exp) = N_Slice then declare Slice_Type : constant Entity_Id := Etype (First_Index (Exp_Typ)); @@ -6862,9 +6872,11 @@ package body Exp_Util is -- Start of processing for Remove_Side_Effects begin - -- Handle cases in which there is nothing to do + -- Handle cases in which there is nothing to do. In GNATprove mode, + -- removal of side effects is useful for the light expansion of + -- renamings. - if not Expander_Active then + if not (Expander_Active or (Full_Analysis and GNATprove_Mode)) then return; end if; @@ -7074,7 +7086,7 @@ package body Exp_Util is -- free if the resulting value is captured by a variable or a -- constant. - if SPARK_Mode + if GNATprove_Mode and then Nkind (Parent (Exp)) = N_Object_Declaration then goto Leave; @@ -7119,7 +7131,7 @@ package body Exp_Util is -- types, use a different approach which ignores the secondary stack -- and "copies" the returned object. - if SPARK_Mode then + if GNATprove_Mode then Res := New_Reference_To (Def_Id, Loc); Ref_Type := Exp_Type; @@ -7156,7 +7168,7 @@ package body Exp_Util is -- Do not generate a 'reference in SPARK mode since the access -- type is not created in the first place. - if SPARK_Mode then + if GNATprove_Mode then New_Exp := E; -- Otherwise generate reference, marking the value as non-null 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; diff --git a/gcc/ada/expander.ads b/gcc/ada/expander.ads index df59442..6c8c649 100644 --- a/gcc/ada/expander.ads +++ b/gcc/ada/expander.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2008, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2013, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -150,18 +150,20 @@ package Expander is -- Saves the current setting of the Expander_Active flag on an internal -- stack and then sets the flag to the given value. -- - -- Note: this routine has no effect in ASIS_Mode. In ASIS_Mode, all - -- expansion activity is always off, since we want the original semantic - -- tree for ASIS purposes without any expansion. This is achieved by - -- setting Expander_Active False in ASIS_Mode. In situations such as - -- the call to Instantiate_Bodies in Frontend, Expander_Mode_Save_And_Set - -- may be called to temporarily turn the expander on, but this will have - -- no effect in ASIS mode. + -- Note: this routine has no effect in ASIS and GNATprove modes. In ASIS + -- mode, all expansion activity is always off, since we want the original + -- semantic tree for ASIS purposes without any expansion. In GNATprove + -- mode, a very light expansion is performed on specific nodes. Both are + -- achieved by setting Expander_Active False in ASIS and GNATprove modes. + -- In situations such as the call to Instantiate_Bodies in Frontend, + -- Expander_Mode_Save_And_Set may be called to temporarily turn the + -- expander on, but this will have no effect in ASIS and GNATprove modes. procedure Expander_Mode_Restore; -- Restores the setting of the Expander_Active flag using the top entry -- pushed onto the stack by Expander_Mode_Save_And_Reset, popping the - -- stack, except that if any errors have been detected, then the state - -- of the flag is left set to False. Disabled for ASIS_Mode (see above). + -- stack, except that if any errors have been detected, then the state of + -- the flag is left set to False. Disabled for ASIS and GNATprove modes + -- (see above). end Expander; diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index f6c6067..122d6b2 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -3280,7 +3280,7 @@ package body Freeze is -- general, neither CodePeer not GNATprove care about the -- internal representation of objects. - and then not (CodePeer_Mode or SPARK_Mode) + and then not (CodePeer_Mode or GNATprove_Mode) then -- If implicit packing enabled, do it @@ -4230,7 +4230,7 @@ package body Freeze is and then not Is_Limited_Composite (E) and then not Is_Packed (Root_Type (E)) and then not Has_Component_Size_Clause (Root_Type (E)) - and then not (CodePeer_Mode or SPARK_Mode) + and then not (CodePeer_Mode or GNATprove_Mode) then -- Compute number of elements in array diff --git a/gcc/ada/frontend.adb b/gcc/ada/frontend.adb index 8a64134..2d5c36f 100644 --- a/gcc/ada/frontend.adb +++ b/gcc/ada/frontend.adb @@ -362,7 +362,7 @@ begin if Operating_Mode = Generate_Code or else (Operating_Mode = Check_Semantics - and then ASIS_Mode) + and then (ASIS_Mode or GNATprove_Mode)) then Instantiate_Bodies; end if; diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index 24341ac..f1bc2f8 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -299,15 +299,16 @@ procedure Gnat1drv is Formal_Extensions := True; end if; - -- Enable SPARK_Mode when using -gnatd.F switch + -- Enable GNATprove_Mode when using -gnatd.F switch if Debug_Flag_Dot_FF then - SPARK_Mode := True; + GNATprove_Mode := True; end if; - -- SPARK_Mode is also activated by default in the gnat2why executable + -- GNATprove_Mode is also activated by default in the gnat2why + -- executable. - if SPARK_Mode then + if GNATprove_Mode then -- Set strict standard interpretation of compiler permissions @@ -384,11 +385,10 @@ procedure Gnat1drv is Polling_Required := False; - -- Set operating mode to Generate_Code, but full front-end expansion - -- is not desirable in SPARK mode, so a light expansion is performed - -- instead. + -- Set operating mode to Check_Semantics, but a light front-end + -- expansion is still performed. - Operating_Mode := Generate_Code; + Operating_Mode := Check_Semantics; -- Skip call to gigi @@ -1054,17 +1054,13 @@ begin elsif CodePeer_Mode then Back_End_Mode := Generate_Object; - -- It is not an error to analyze in SPARK mode a spec which requires a - -- body, when the body is not available. During frame condition + -- It is not an error to analyze in GNATprove mode a spec which requires + -- a body, when the body is not available. During frame condition -- generation, the corresponding ALI file is generated. During -- translation to Why, Why code is generated for the spec. - elsif SPARK_Mode then - if Frame_Condition_Mode then - Back_End_Mode := Declarations_Only; - else - Back_End_Mode := Generate_Object; - end if; + elsif GNATprove_Mode then + Back_End_Mode := Declarations_Only; -- In all other cases (specs which have bodies, generics, and bodies -- where subunits are missing), we cannot generate code and we generate @@ -1168,10 +1164,11 @@ begin -- since representations are largely symbolic there. if Back_End_Mode = Declarations_Only - and then (not (Back_Annotate_Rep_Info or Generate_SCIL) - or else Main_Kind = N_Subunit - or else Targparm.Frontend_Layout_On_Target - or else Targparm.VM_Target /= No_VM) + and then + (not (Back_Annotate_Rep_Info or Generate_SCIL or GNATprove_Mode) + or else Main_Kind = N_Subunit + or else Targparm.Frontend_Layout_On_Target + or else Targparm.VM_Target /= No_VM) then Sem_Ch13.Validate_Unchecked_Conversions; Sem_Ch13.Validate_Address_Clauses; 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; diff --git a/gcc/ada/lib-xref.adb b/gcc/ada/lib-xref.adb index 972d963..4cf52c9 100644 --- a/gcc/ada/lib-xref.adb +++ b/gcc/ada/lib-xref.adb @@ -644,7 +644,7 @@ package body Lib.Xref is -- in SPARK mode when the related context comes from an instance. or else - (SPARK_Mode + (GNATprove_Mode and then In_Extended_Main_Code_Unit (N) and then (Typ = 'm' or else Typ = 'r' or else Typ = 's')) then @@ -899,7 +899,7 @@ package body Lib.Xref is and then (Instantiation_Location (Sloc (N)) = No_Location or else Typ = 'i' - or else SPARK_Mode) + or else GNATprove_Mode) -- Ignore dummy references @@ -986,7 +986,7 @@ package body Lib.Xref is -- the renaming, which is needed to compute a valid set of effects -- (reads, writes) for the enclosing subprogram. - if SPARK_Mode then + if GNATprove_Mode then Ent := Get_Through_Renamings (Ent); -- If no enclosing object, then it could be a reference to any @@ -1015,7 +1015,7 @@ package body Lib.Xref is Actual_Typ := 'P'; end if; - if SPARK_Mode then + if GNATprove_Mode then Ref := Sloc (Nod); Def := Sloc (Ent); diff --git a/gcc/ada/opt.adb b/gcc/ada/opt.adb index 9f1f2d8..298b7e3 100644 --- a/gcc/ada/opt.adb +++ b/gcc/ada/opt.adb @@ -44,7 +44,7 @@ package body Opt is function Full_Expander_Active return Boolean is begin - return Expander_Active and not SPARK_Mode; + return Expander_Active; end Full_Expander_Active; ---------------------------------- diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index 06d9a4b..ea5f179 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -1996,7 +1996,7 @@ package Opt is ----------------------------------- Frame_Condition_Mode : Boolean := False; - -- Specific mode to be used in combination with SPARK_Mode. If set to + -- Specific mode to be used in combination with GNATprove_Mode. If set to -- true, ALI files containing the frame conditions (global effects) are -- generated, and Why files are *not* generated. If not true, Why files -- are generated. Set by debug flag -gnatd.G. @@ -2010,7 +2010,7 @@ package Opt is -- The mode applicable to the whole compilation. The global mode can be set -- in a configuration file such as gnat.adc. - SPARK_Mode : Boolean := False; + GNATprove_Mode : Boolean := False; -- Specific compiling mode targeting formal verification through the -- generation of Why code for those parts of the input code that belong to -- the SPARK 2014 subset of Ada. Set True by the gnat2why executable or by diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb index 668c444..ff2d7eb 100644 --- a/gcc/ada/restrict.adb +++ b/gcc/ada/restrict.adb @@ -538,7 +538,7 @@ package body Restrict is -- set in gnat1drv.adb so that we have consistency between each -- compilation. - if CodePeer_Mode or SPARK_Mode then + if CodePeer_Mode or GNATprove_Mode then return; end if; diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb index 5aec38a..6724593 100644 --- a/gcc/ada/sem_aggr.adb +++ b/gcc/ada/sem_aggr.adb @@ -454,10 +454,14 @@ package body Sem_Aggr is Check_Unset_Reference (Exp); end if; - -- This is really expansion activity, so make sure that expansion - -- is on and is allowed. + -- This is really expansion activity, so make sure that expansion is + -- on and is allowed. In GNATprove mode, we also want check flags to be + -- added in the tree, so that the formal verification can rely on those + -- to be present. - if not Expander_Active or else In_Spec_Expression then + if not (Expander_Active or GNATprove_Mode) + or In_Spec_Expression + then return; end if; @@ -996,10 +1000,10 @@ package body Sem_Aggr is -- frozen so that initialization procedures can properly be called -- in the resolution that follows. The replacement of boxes with -- initialization calls is properly an expansion activity but it must - -- be done during revolution. + -- be done during resolution. if Expander_Active - and then Present (Component_Associations (N)) + and then Present (Component_Associations (N)) then declare Comp : Node_Id; diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 231d0b2..d6ca597 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -4499,7 +4499,7 @@ package body Sem_Attr is -- not suffer from the out-of-order issue described above. Thus, this -- expansion is skipped in SPARK mode. - if not Is_Entity_Name (P) and then not SPARK_Mode then + if not Is_Entity_Name (P) and then not GNATprove_Mode then P_Type := Base_Type (P_Type); Set_Etype (N, P_Type); Set_Etype (P, P_Type); diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 1572e4f..f509ba4 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -3616,7 +3616,7 @@ package body Sem_Ch12 is -- We instantiate the body if we are generating code, if we are -- generating cross-reference information, or if we are building - -- trees for ASIS use. + -- trees for ASIS use or GNATprove use. declare Enclosing_Body_Present : Boolean := False; @@ -3724,7 +3724,7 @@ package body Sem_Ch12 is and then not Inline_Now and then (Operating_Mode = Generate_Code or else (Operating_Mode = Check_Semantics - and then ASIS_Mode)); + and then (ASIS_Mode or GNATprove_Mode))); -- If front_end_inlining is enabled, do not instantiate body if -- within a generic context. @@ -4390,17 +4390,18 @@ package body Sem_Ch12 is or else Is_Inlined (Subp) or else Is_Inlined (Alias (Subp))) - -- Must be generating code or analyzing code in ASIS mode + -- Must be generating code or analyzing code in ASIS mode or GNATprove + -- mode. and then (Operating_Mode = Generate_Code or else (Operating_Mode = Check_Semantics - and then ASIS_Mode)) + and then (ASIS_Mode or GNATprove_Mode))) -- The body is needed when generating code (full expansion), in ASIS - -- mode for other tools, and in SPARK mode (special expansion) for + -- mode for other tools, and in GNATprove mode (special expansion) for -- formal verification of the body itself. - and then (Expander_Active or ASIS_Mode) + and then (Expander_Active or ASIS_Mode or GNATprove_Mode) -- No point in inlining if ABE is inevitable diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 1586244..fa5ed8d 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -2718,7 +2718,7 @@ package body Sem_Ch13 is Prepend (Aitem, Visible_Declarations (Specification (N))); - elsif Nkind (N) = N_Package_Instantiation then + elsif Nkind (N) = N_Package_Instantiation then declare Spec : constant Node_Id := Specification (Instance_Spec (N)); diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 01d6ddd..86e233b 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -10084,7 +10084,7 @@ package body Sem_Ch3 is -- SPARK mode. Since this is legal code with respect to theorem -- proving, do not emit the error. - if SPARK_Mode + if GNATprove_Mode and then Nkind (Exp) = N_Function_Call and then Nkind (Parent (Exp)) = N_Object_Declaration and then not Comes_From_Source @@ -12223,12 +12223,12 @@ package body Sem_Ch3 is -- needed, since checks may cause duplication of the expressions -- which must not be reevaluated. - -- The forced evaluation removes side effects from expressions, - -- which should occur also in SPARK mode. Otherwise, we end up with + -- The forced evaluation removes side effects from expressions, which + -- should occur also in GNATprove mode. Otherwise, we end up with -- unexpected insertions of actions at places where this is not -- supposed to occur, e.g. on default parameters of a call. - if Expander_Active then + if Expander_Active or GNATprove_Mode then Force_Evaluation (Low_Bound (R)); Force_Evaluation (High_Bound (R)); end if; @@ -18865,11 +18865,11 @@ package body Sem_Ch3 is -- duplication of the expression without forcing evaluation. -- The forced evaluation removes side effects from expressions, - -- which should occur also in SPARK mode. Otherwise, we end up + -- which should occur also in GNATprove mode. Otherwise, we end up -- with unexpected insertions of actions at places where this is -- not supposed to occur, e.g. on default parameters of a call. - if Expander_Active then + if Expander_Active or GNATprove_Mode then Force_Evaluation (Lo); Force_Evaluation (Hi); end if; @@ -18980,11 +18980,11 @@ package body Sem_Ch3 is -- Case of other than an explicit N_Range node -- The forced evaluation removes side effects from expressions, which - -- should occur also in SPARK mode. Otherwise, we end up with unexpected - -- insertions of actions at places where this is not supposed to occur, - -- e.g. on default parameters of a call. + -- should occur also in GNATprove mode. Otherwise, we end up with + -- unexpected insertions of actions at places where this is not + -- supposed to occur, e.g. on default parameters of a call. - elsif Expander_Active then + elsif Expander_Active or GNATprove_Mode then Get_Index_Bounds (R, Lo, Hi); Force_Evaluation (Lo); Force_Evaluation (Hi); diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb index 52aa233..d458192 100644 --- a/gcc/ada/sem_ch4.adb +++ b/gcc/ada/sem_ch4.adb @@ -1823,7 +1823,7 @@ package body Sem_Ch4 is -- In formal verification mode, keep track of all reads and writes -- through explicit dereferences. - if SPARK_Mode then + if GNATprove_Mode then SPARK_Specific.Generate_Dereference (N); end if; @@ -4613,7 +4613,7 @@ package body Sem_Ch4 is -- In SPARK mode, this is made into an error to simplify -- the processing of the formal verification backend. - if SPARK_Mode then + if GNATprove_Mode then Apply_Compile_Time_Constraint_Error (N, "component not present in }", CE_Discriminant_Check_Failed, diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index a29aece..ec7c12e 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -1712,7 +1712,7 @@ package body Sem_Ch5 is -- Do not perform this expansion in SPARK mode, since the formal -- verification directly deals with the source form of the iterator. - and then not SPARK_Mode + and then not GNATprove_Mode then declare Id : constant Entity_Id := Make_Temporary (Loc, 'R', Iter_Name); diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 3b5eee1..3f33536 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -1151,7 +1151,7 @@ package body Sem_Ch6 is -- prepares the contract assertions for generic subprograms or for -- ASIS. Do not generate contract checks in SPARK mode. - if not SPARK_Mode then + if not GNATprove_Mode then Expand_Subprogram_Contract (N, Gen_Id, Body_Id); end if; @@ -3188,7 +3188,7 @@ package body Sem_Ch6 is -- prepares the contract assertions for generic subprograms or for ASIS. -- Do not generate contract checks in SPARK mode. - if not SPARK_Mode then + if not GNATprove_Mode then Expand_Subprogram_Contract (N, Spec_Id, Body_Id); end if; diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb index 61d9766..7f60859 100644 --- a/gcc/ada/sem_ch8.adb +++ b/gcc/ada/sem_ch8.adb @@ -5079,7 +5079,7 @@ package body Sem_Ch8 is if Is_Object (E) and then Present (Renamed_Object (E)) - and then not SPARK_Mode + and then not GNATprove_Mode then Generate_Reference (E, N); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 19d8877..d08f133 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -4556,7 +4556,7 @@ package body Sem_Prag is -- N_Contract node. if Acts_As_Spec (PO) - and then (SPARK_Mode or Formal_Extensions) + and then (GNATprove_Mode or Formal_Extensions) then declare Prag : constant Node_Id := New_Copy_Tree (N); @@ -4596,7 +4596,7 @@ package body Sem_Prag is -- where there is no later point at which the aspect will be -- analyzed. - if SPARK_Mode or else ASIS_Mode then + if GNATprove_Mode or else ASIS_Mode then Analyze_Pre_Post_Condition_In_Decl_Part (N, Defining_Entity (Unit (Parent (PO)))); end if; @@ -8345,7 +8345,9 @@ package body Sem_Prag is -- user code: we want to generate checks for analysis purposes, as -- set respectively by -gnatC and -gnatd.F - if (CodePeer_Mode or SPARK_Mode) and then Comes_From_Source (N) then + if (CodePeer_Mode or GNATprove_Mode) + and then Comes_From_Source (N) + then return; end if; @@ -13700,7 +13702,7 @@ package body Sem_Prag is -- in these modes. if not Restriction_Active (No_Initialize_Scalars) - and then not (CodePeer_Mode or SPARK_Mode) + and then not (CodePeer_Mode or GNATprove_Mode) then Init_Or_Norm_Scalars := True; Initialize_Scalars := True; @@ -13819,7 +13821,7 @@ package body Sem_Prag is -- Pragma always active unless in CodePeer or SPARK mode, since -- this causes walk order issues. - if not (CodePeer_Mode or SPARK_Mode) then + if not (CodePeer_Mode or GNATprove_Mode) then Process_Inline (Enabled); end if; @@ -15460,7 +15462,7 @@ package body Sem_Prag is -- incorrect negative results in SPARK mode, so ignore this pragma -- in these modes. - if not (CodePeer_Mode or SPARK_Mode) then + if not (CodePeer_Mode or GNATprove_Mode) then Normalize_Scalars := True; Init_Or_Norm_Scalars := True; end if; @@ -15921,7 +15923,7 @@ package body Sem_Prag is -- complex front-end expansions related to pragma Pack, -- so disable handling of pragma Pack in these cases. - if CodePeer_Mode or SPARK_Mode then + if CodePeer_Mode or GNATprove_Mode then null; -- Don't attempt any packing for VM targets. We possibly diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 9a76e04a..12d9d31 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -1693,7 +1693,7 @@ package body Sem_Res is -- case of Ada 2012 constructs such as quantified expressions, which are -- expanded in two separate steps. - if SPARK_Mode then + if GNATprove_Mode then Analyze_And_Resolve (N, T); else Analyze_And_Resolve (N, T, Suppress => All_Checks); @@ -4206,7 +4206,7 @@ package body Sem_Res is -- in scope at the point of reference, so the reference should -- be ignored for computing effects of subprograms. - and then not SPARK_Mode + and then not GNATprove_Mode then Set_Entity (Selector_Name (Parent (A)), F); Generate_Reference (F, Selector_Name (Parent (A))); diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 08acd70..7a1920c 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -12802,7 +12802,7 @@ package body Sem_Util is -- In formal verification mode, keep track of all reads and -- writes through explicit dereferences. - if SPARK_Mode then + if GNATprove_Mode then SPARK_Specific.Generate_Dereference (N, 'm'); end if; @@ -12897,11 +12897,12 @@ package body Sem_Util is -- Generate a reference only if the assignment comes from -- source. This excludes, for example, calls to a dispatching - -- assignment operation when the left-hand side is tagged. + -- assignment operation when the left-hand side is tagged. In + -- GNATprove mode, we need those references also on generated + -- code, as these are used to compute the local effects of + -- subprograms. - -- Why is SPARK mode different here ??? - - if Modification_Comes_From_Source or SPARK_Mode then + if Modification_Comes_From_Source or GNATprove_Mode then Generate_Reference (Ent, Exp, 'm'); -- If the target of the assignment is the bound variable