===================================================================
@@ -454,10 +454,14 @@
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 @@
-- 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;
===================================================================
@@ -10084,7 +10084,7 @@
-- 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 @@
-- 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 @@
-- 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 @@
-- 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);
===================================================================
@@ -362,7 +362,7 @@
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;
===================================================================
@@ -31,7 +31,6 @@
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,52 +93,29 @@
-----------------------
procedure Expand_SPARK_Call (N : Node_Id) is
- Call_Node : constant Node_Id := N;
- Parent_Subp : Entity_Id;
-
begin
- -- Ignore if previous error
+ -- If the subprogram is a renaming, replace it in the call with the name
+ -- 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 (Call_Node) in N_Has_Etype
- and then Etype (Call_Node) = Any_Type
+ if Nkind (Name (N)) in N_Has_Entity
+ and then Present (Entity (Name (N)))
then
- return;
+ 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;
-
- -- 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);
- end if;
end Expand_SPARK_Call;
------------------------------------------------
===================================================================
@@ -23,10 +23,9 @@
-- --
------------------------------------------------------------------------------
+-- 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.
===================================================================
@@ -937,7 +937,7 @@
-- 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 @@
-- 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 @@
-- 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 @@
-- 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
===================================================================
@@ -1712,7 +1712,7 @@
-- 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);
===================================================================
@@ -2034,12 +2034,22 @@
-- 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 @@
-- 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 @@
-- 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 @@
-- 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 @@
-- 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
===================================================================
@@ -841,7 +841,7 @@
-- 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 @@
-- 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 @@
-- 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;
===================================================================
@@ -274,11 +274,11 @@
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;
===================================================================
@@ -4556,7 +4556,7 @@
-- 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 @@
-- 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 @@
-- 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 @@
-- 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 @@
-- 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 @@
-- 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 @@
-- 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
===================================================================
@@ -3616,7 +3616,7 @@
-- 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 @@
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 @@
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
===================================================================
@@ -3280,7 +3280,7 @@
-- 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 @@
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
===================================================================
@@ -12802,7 +12802,7 @@
-- 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 @@
-- 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
===================================================================
@@ -1693,7 +1693,7 @@
-- 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 @@
-- 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)));
===================================================================
@@ -88,8 +88,9 @@
-- 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 @@
-- 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 @@
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 @@
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 @@
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;
===================================================================
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
+-- 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 @@
-- 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;
===================================================================
@@ -4499,7 +4499,7 @@
-- 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);
===================================================================
@@ -1314,7 +1314,7 @@
-- 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);
===================================================================
@@ -299,15 +299,16 @@
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 @@
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 @@
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 @@
-- 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;
===================================================================
@@ -239,7 +239,7 @@
-- 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 @@
-- 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
===================================================================
@@ -1823,7 +1823,7 @@
-- 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 @@
-- 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,
===================================================================
@@ -538,7 +538,7 @@
-- 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;
===================================================================
@@ -1151,7 +1151,7 @@
-- 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 @@
-- 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;
===================================================================
@@ -5079,7 +5079,7 @@
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);
===================================================================
@@ -44,7 +44,7 @@
function Full_Expander_Active return Boolean is
begin
- return Expander_Active and not SPARK_Mode;
+ return Expander_Active;
end Full_Expander_Active;
----------------------------------
===================================================================
@@ -1996,7 +1996,7 @@
-----------------------------------
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 @@
-- 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
===================================================================
@@ -235,12 +235,12 @@
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
===================================================================
@@ -2718,7 +2718,7 @@
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));
===================================================================
@@ -644,7 +644,7 @@
-- 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 @@
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 @@
-- 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 @@
Actual_Typ := 'P';
end if;
- if SPARK_Mode then
+ if GNATprove_Mode then
Ref := Sloc (Nod);
Def := Sloc (Ent);