2014-01-20 Yannick Moy <moy@adacore.com>
+ * exp_spark.adb (Expand_SPARK_Call): Remove procedure.
+ * opt.adb, opt.ads (Full_Expander_Active): Remove function.
+ * checks.adb, exp_ch6.adb, exp_ch9.adb, exp_disp.adb, sem_aggr.adb,
+ * sem_ch10.adb, sem_ch5.adb, sem_ch6.adb, sem_ch8.adb, sem_ch9.adb,
+ * sem_disp.adb, sem_res.adb Replace Full_Expander_Active by
+ Expander_Active.
+
+2014-01-20 Yannick Moy <moy@adacore.com>
+
+ * sinfo.ads Update documentation of GNATprove mode.
+
+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,
-- are cases (e.g. with pragma Debug) where generating the checks
-- can cause real trouble).
- if not Full_Expander_Active then
+ if not Expander_Active then
return;
end if;
if Backend_Overflow_Checks_On_Target
or else not Do_Overflow_Check (N)
- or else not Full_Expander_Active
+ or else not Expander_Active
or else (Present (Parent (N))
and then Nkind (Parent (N)) = N_Type_Conversion
and then Integer_Promotion_Possible (Parent (N)))
-- Nothing to do if discriminant checks are suppressed or else no code
-- is to be generated
- if not Full_Expander_Active
+ if not Expander_Active
or else Discriminant_Checks_Suppressed (T_Typ)
then
return;
-- Proceed here in SUPPRESSED or CHECKED modes
- if Full_Expander_Active
+ if Expander_Active
and then not Backend_Divide_Checks_On_Target
and then Check_Needed (Right, Division_Check)
then
Right : constant Node_Id := Right_Opnd (N);
begin
- if Full_Expander_Active
+ if Expander_Active
and then not Backend_Divide_Checks_On_Target
and then Check_Needed (Right, Division_Check)
then
-- the frontend to expand these checks, which are dealt with directly
-- in the formal verification backend.
- if not Full_Expander_Active then
+ if not Expander_Active then
return;
end if;
or else (not Length_Checks_Suppressed (Target_Typ));
begin
- if not Full_Expander_Active then
+ if not Expander_Active then
return;
end if;
or else (not Range_Checks_Suppressed (Target_Typ));
begin
- if not Full_Expander_Active or else not Checks_On then
+ if not Expander_Active or else not Checks_On then
return;
end if;
-- enhanced to check for an always True value in the condition and to
-- generate a compilation warning???
- if not Full_Expander_Active or else not Checks_On then
+ if not Expander_Active or else not Checks_On then
return;
end if;
-- Start of processing for Selected_Length_Checks
begin
- if not Full_Expander_Active then
+ if not Expander_Active then
return Ret_Result;
end if;
-- Start of processing for Selected_Range_Checks
begin
- if not Full_Expander_Active then
+ if not Expander_Active then
return Ret_Result;
end if;
-- may end up with a call that is neither resolved to an entity, nor
-- an indirect call.
- if not Full_Expander_Active then
+ if not Expander_Active then
return False;
end if;
Ldecl2 : Node_Id;
begin
- if Full_Expander_Active then
+ if Expander_Active then
-- If we have no handled statement sequence, we may need to build
-- a dummy sequence consisting of a null statement. This can be
-- barrier just as a protected function, and discard the protected
-- version of it because it is never called.
- if Full_Expander_Active then
+ if Expander_Active then
B_F := Build_Barrier_Function (N, Ent, Prot);
Func := Barrier_Function (Ent);
Set_Corresponding_Spec (B_F, Func);
-- condition does not reference any of the generated renamings
-- within the function.
- if Full_Expander_Active and then Scope (Entity (Cond)) /= Func then
+ if Expander_Active and then Scope (Entity (Cond)) /= Func then
Set_Declarations (B_F, Empty_List);
end if;
Error_Msg_CRT ("protected body", N);
return;
- elsif Full_Expander_Active then
+ elsif Expander_Active then
-- Associate discriminals with the first subprogram or entry body to
-- be expanded.
-- Expand_Dispatching_Call is called directly from the semantics,
-- so we only proceed if the expander is active.
- if not Full_Expander_Active
+ if not Expander_Active
-- And there is no need to expand the call if we are compiling under
-- restriction No_Dispatching_Calls; the semantic analyzer has
with Einfo; use Einfo;
with Exp_Dbug; use Exp_Dbug;
with Exp_Util; use Exp_Util;
-with Sem_Aux; use Sem_Aux;
with Sem_Res; use Sem_Res;
with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo;
-- Local Subprograms --
-----------------------
- procedure Expand_SPARK_Call (N : Node_Id);
- -- This procedure contains common processing for function and procedure
- -- calls: replacement of renaming by subprogram renamed
-
procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
-- Perform name evaluation for a renamed object
N_Subprogram_Body =>
Qualify_Entity_Names (N);
- when N_Subprogram_Call =>
- Expand_SPARK_Call (N);
-
when N_Expanded_Name |
N_Identifier =>
Expand_Potential_Renaming (N);
end case;
end Expand_SPARK;
- -----------------------
- -- Expand_SPARK_Call --
- -----------------------
-
- procedure Expand_SPARK_Call (N : Node_Id) is
- begin
- -- 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 (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;
-
------------------------------------------------
-- Expand_SPARK_N_Object_Renaming_Declaration --
------------------------------------------------
SU : constant := Storage_Unit;
-- Shorthand for System.Storage_Unit
- --------------------------
- -- Full_Expander_Active --
- --------------------------
-
- function Full_Expander_Active return Boolean is
- begin
- return Expander_Active;
- end Full_Expander_Active;
-
----------------------------------
-- Register_Opt_Config_Switches --
----------------------------------
-- this flag, see package Expander. Indeed this flag might more logically
-- be in the spec of Expander, but it is referenced by Errout, and it
-- really seems wrong for Errout to depend on Expander.
- --
- -- Note: for many purposes, it is more appropriate to test the flag
- -- Full_Expander_Active, which also checks that SPARK mode is not active.
Static_Dispatch_Tables : Boolean := True;
-- This flag indicates if the backend supports generation of statically
-- for integers are limited to the strict minimum with this option. Set by
-- debug flag -gnatd.D.
- function Full_Expander_Active return Boolean;
- pragma Inline (Full_Expander_Active);
- -- Returns the value of (Expander_Active and not SPARK_Mode). This "flag"
- -- indicates that expansion is fully active, that is, not in the reduced
- -- mode for SPARK (True) or that expansion is either deactivated, or active
- -- in the reduced mode for SPARK (False). For more information on full
- -- expansion, see package Expander. For more information on reduced
- -- SPARK expansion, see package Exp_SPARK.
-
private
-- The following type is used to save and restore settings of switches in
-- performed safely.
if Single_Elmt
- or else not Full_Expander_Active
+ or else not Expander_Active
or else In_Spec_Expression
then
Analyze_And_Resolve (Expr, Component_Typ);
-- expansion is active, because the context may be generic and the
-- flag not defined yet.
- if Full_Expander_Active then
+ if Expander_Active then
Insert_After (N,
Make_Assignment_Statement (Loc,
Name =>
if No (Iter)
or else No (Iterator_Specification (Iter))
- or else not Full_Expander_Active
+ or else not Expander_Active
then
if Present (Iter)
and then Present (Iterator_Specification (Iter))
-- body may be the rewritting of an expression function, and we need to
-- verify that the original node is in the source.
- if Full_Expander_Active
+ if Expander_Active
and then Comes_From_Source (Original_Node (N))
and then Present (Prot_Typ)
and then Present (Spec_Id)
-- parameter block, and it is this local variable that may
-- require an actual subtype.
- if Full_Expander_Active then
+ if Expander_Active then
Decl := Build_Actual_Subtype (T, Renamed_Object (Formal));
else
Decl := Build_Actual_Subtype (T, Formal);
end if;
if Nkind (N) = N_Accept_Statement
- and then Full_Expander_Active
+ and then Expander_Active
then
Set_Actual_Subtype (Renamed_Object (Formal),
Defining_Identifier (Decl));
if Is_Actual
and then Is_Abstract_Subprogram (Formal_Spec)
- and then Full_Expander_Active
+ and then Expander_Active
then
declare
Stream_Prim : Entity_Id;
-- for the discriminals and privals and finally a declaration for the
-- entry family index (if applicable).
- if Full_Expander_Active
+ if Expander_Active
and then Is_Protected_Type (P_Type)
then
Install_Private_Data_Declarations
-- Also skip if expander is not active
- and then Full_Expander_Active
+ and then Expander_Active
then
Expand_N_Protected_Type_Declaration (N);
Process_Full_View (N, T, Def_Id);
-- Also skip if expander is not active
- and then Full_Expander_Active
+ and then Expander_Active
then
Expand_N_Task_Type_Declaration (N);
Process_Full_View (N, T, Def_Id);
-- emitted after those tables are built, to prevent access before
-- elaboration in gigi.
- if Body_Is_Last_Primitive and then Full_Expander_Active then
+ if Body_Is_Last_Primitive and then Expander_Active then
declare
Subp_Body : constant Node_Id := Unit_Declaration_Node (Subp);
Elmt : Elmt_Id;
-- Start of processing for Replace_Actual_Discriminants
begin
- if not Full_Expander_Active then
+ if not Expander_Active then
return;
end if;
-- If we are generating code in distributed mode, perform
-- semantic checks against corresponding remote entities.
- if Full_Expander_Active
+ if Expander_Active
and then Get_PCS_Name /= Name_No_DSA
then
Check_Subtype_Conformant
elsif Nkind (A) = N_Function_Call
and then Is_Limited_Record (Etype (F))
and then not Is_Constrained (Etype (F))
- and then Full_Expander_Active
+ and then Expander_Active
and then (Is_Controlled (Etype (F)) or else Has_Task (Etype (F)))
then
Establish_Transient_Scope (A, Sec_Stack => False);
elsif Nkind (A) = N_Op_Concat
and then Nkind (N) = N_Procedure_Call_Statement
- and then Full_Expander_Active
+ and then Expander_Active
and then
not (Is_Intrinsic_Subprogram (Nam)
and then Chars (Nam) = Name_Asm)
-- be removed in the expansion of the wrapped construct.
if (Is_Controlled (DDT) or else Has_Task (DDT))
- and then Full_Expander_Active
+ and then Expander_Active
then
Establish_Transient_Scope (A, Sec_Stack => False);
end if;
then
null;
- elsif Full_Expander_Active
+ elsif Expander_Active
and then Is_Type (Etype (Nam))
and then Requires_Transient_Scope (Etype (Nam))
and then
-- Protected functions can return on the secondary stack, in which
-- case we must trigger the transient scope mechanism.
- elsif Full_Expander_Active
+ elsif Expander_Active
and then Requires_Transient_Scope (Etype (Nam))
then
Establish_Transient_Scope (N, Sec_Stack => True);
-- Why the Expander_Active test here ???
- if Full_Expander_Active
+ if Expander_Active
and then
(Ekind_In (T, E_Anonymous_Access_Type,
E_Anonymous_Access_Subprogram_Type)
-- We must preserve the original entity in a generic setting, so that
-- the legality of the operation can be verified in an instance.
- if not Full_Expander_Active then
+ if not Expander_Active then
return;
end if;
-- transformation while analyzing generic units, as type information
-- would be lost when reanalyzing the constant node in the instance.
- if Is_Discrete_Type (Typ) and then Full_Expander_Active then
+ if Is_Discrete_Type (Typ) and then Expander_Active then
if Is_OK_Static_Expression (L) then
Fold_Uint (L, Expr_Value (L), Is_Static_Expression (L));
end if;
-- helpful for coverage analysis. However this should not happen in
-- generics.
- if Full_Expander_Active then
+ if Expander_Active then
declare
Reloc_L : constant Node_Id := Relocate_Node (L);
begin
-- expression coincides with the target type.
if Ada_Version >= Ada_2005
- and then Full_Expander_Active
+ and then Expander_Active
and then Operand_Typ /= Target_Typ
then
declare
-- premature (e.g. if the slice is within a transient scope). This needs
-- to be done only if expansion is enabled.
- elsif Full_Expander_Active then
+ elsif Expander_Active then
Ensure_Defined (Typ => Slice_Subtype, N => N);
end if;
end Set_Slice_Subtype;
-- simply ignore these nodes, since they are not relevant to the task
-- of back annotating representation information.
- ----------------
- -- SPARK Mode --
- ----------------
+ --------------------
+ -- GNATprove Mode --
+ --------------------
- -- When a file is compiled in SPARK mode (-gnatd.F), a very light expansion
- -- is performed and the analysis must generate a tree in a form that meets
- -- additional requirements.
+ -- When a file is compiled in GNATprove mode (-gnatd.F), a very light
+ -- expansion is performed and the analysis must generate a tree in a
+ -- form that meets additional requirements.
- -- The SPARK expansion does two transformations of the tree, that cannot be
- -- postponed after the frontend semantic analysis:
+ -- This light expansion does two transformations of the tree, that cannot
+ -- be postponed after the frontend semantic analysis:
- -- 1. Replace renamings by renamed (object/subprogram). This requires
+ -- 1. Replace object renamings by renamed object. This requires
-- introducing temporaries at the point of the renaming, which must be
-- properly analyzed.
-- local effects/call-graphs in ALI files, with the completely
-- qualified names (in particular the suffix to distinguish homonyms).
- -- The tree after SPARK expansion should be fully analyzed semantically,
- -- which sometimes requires the insertion of semantic pre-analysis, for
- -- example for subprogram contracts and pragma check/assert. In particular,
- -- all expression must have their proper type, and semantic links should be
- -- set between tree nodes (partial to full view, etc.) Some kinds of nodes
- -- should be either absent, or can be ignored by the formal verification
- -- backend:
+ -- The tree after this light expansion should be fully analyzed
+ -- semantically, which sometimes requires the insertion of semantic
+ -- pre-analysis, for example for subprogram contracts and pragma
+ -- check/assert. In particular, all expression must have their proper type,
+ -- and semantic links should be set between tree nodes (partial to full
+ -- view, etc.) Some kinds of nodes should be either absent, or can be
+ -- ignored by the formal verification backend:
-- N_Object_Renaming_Declaration: can be ignored safely
- -- N_Expression_Function: absent (rewitten)
+ -- N_Expression_Function: absent (rewritten)
-- N_Expression_With_Actions: absent (not generated)
-- SPARK cross-references are generated from the regular cross-references
-- collected during semantic analysis, in particular on all dereferences.
-- These SPARK cross-references are output in a separate section of ALI
-- files, as described in spark_xrefs.adb. They are the basis for the
- -- computation of data dependences in the formal verification backend.
- -- This implies that all cross-references should be generated in this mode,
- -- even those that would not make sense from a user point-of-view, and that
- -- cross-references that do not lead to data dependences for subprograms
- -- can be safely ignored.
+ -- computation of data dependences in GNATprove. This implies that all
+ -- cross-references should be generated in this mode, even those that would
+ -- not make sense from a user point-of-view, and that cross-references that
+ -- do not lead to data dependences for subprograms can be safely ignored.
------------------------
-- Common Flag Fields --
projects / platform / upstream / linaro-gcc.git / commitdiff