+2014-01-20 Yannick Moy <moy@adacore.com>
+
+ * 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 <ebotcazou@adacore.com>
* gcc-interface/decl.c (gnat_to_gnu_entity) <object>: Robustify tests
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
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;
-- 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
-- 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
-- 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;
-- Do not perform this expansion in SPARK mode because it is not
-- necessary.
- if SPARK_Mode then
+ if GNATprove_Mode then
return;
end if;
-- 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;
-- 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
-- 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);
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
-----------------------
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;
-- --
------------------------------------------------------------------------------
--- 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.
-- 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));
-- 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;
-- 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;
-- 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;
-- 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
-- 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
-- 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
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
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;
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;
-- --
-- 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- --
-- 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;
-- 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
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
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;
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
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
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
-- 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;
-- files, which are required to compute frame conditions
-- of subprograms.
- or else SPARK_Mode
+ or else GNATprove_Mode
then
Write_Info_Tab (25);
-- 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;
-- 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;
-- 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
and then
(Instantiation_Location (Sloc (N)) = No_Location
or else Typ = 'i'
- or else SPARK_Mode)
+ or else GNATprove_Mode)
-- Ignore dummy references
-- 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
Actual_Typ := 'P';
end if;
- if SPARK_Mode then
+ if GNATprove_Mode then
Ref := Sloc (Nod);
Def := Sloc (Ent);
function Full_Expander_Active return Boolean is
begin
- return Expander_Active and not SPARK_Mode;
+ return Expander_Active;
end Full_Expander_Active;
----------------------------------
-----------------------------------
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.
-- 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
-- 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;
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;
-- 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;
-- 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);
-- 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;
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.
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
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));
-- 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
-- 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;
-- 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;
-- 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);
-- 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;
-- 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,
-- 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);
-- 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;
-- 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;
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);
-- 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);
-- 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;
-- 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;
-- 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;
-- 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;
-- 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;
-- 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
-- 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);
-- 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)));
-- 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;
-- 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
projects / platform / upstream / linaro-gcc.git / commitdiff