mirror/gcc
2
0
Fork 0
mirror of git://gcc.gnu.org/git/gcc.git synced 2025-03-26 21:51:12 +08:00
Code Issues Packages Projects Releases Wiki Activity

exp_spark.adb (Expand_SPARK_Call): Remove procedure.

Browse Source 
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.

From-SVN: r206806
This commit is contained in:
Yannick Moy 2014-01-20 13:47:41 +00:00 committed by Arnaud Charlet
parent f5da7a97f5
commit 4460a9bcc2
17 changed files with 75 additions and 122 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
gcc/ada/ChangeLog
View File

@ -1,3 +1,16 @@
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,

22
gcc/ada/checks.adb
View File

@ -478,7 +478,7 @@ package body Checks is
-- 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;
@ -960,7 +960,7 @@ package body Checks is
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)))
@ -1419,7 +1419,7 @@ package body Checks is
-- 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;
@ -1732,7 +1732,7 @@ package body Checks is
-- 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
@ -1803,7 +1803,7 @@ package body Checks is
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
@ -1914,7 +1914,7 @@ package body Checks is
-- 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;
@ -2945,7 +2945,7 @@ package body Checks is
or else (not Length_Checks_Suppressed (Target_Typ));
begin
if not Full_Expander_Active then
if not Expander_Active then
return;
end if;
@ -3052,7 +3052,7 @@ package body Checks is
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;
@ -6290,7 +6290,7 @@ package body Checks is
-- 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;
@ -8321,7 +8321,7 @@ package body Checks is
-- Start of processing for Selected_Length_Checks
begin
if not Full_Expander_Active then
if not Expander_Active then
return Ret_Result;
end if;
@ -8871,7 +8871,7 @@ package body Checks is
-- Start of processing for Selected_Range_Checks
begin
if not Full_Expander_Active then
if not Expander_Active then
return Ret_Result;
end if;

2
gcc/ada/exp_ch6.adb
View File

@ -9603,7 +9603,7 @@ package body Exp_Ch6 is
-- 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;

8
gcc/ada/exp_ch9.adb
View File

@ -5813,7 +5813,7 @@ package body Exp_Ch9 is
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
@ -6123,7 +6123,7 @@ package body Exp_Ch9 is
-- 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);
@ -6161,7 +6161,7 @@ package body Exp_Ch9 is
-- 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;
@ -12497,7 +12497,7 @@ package body Exp_Ch9 is
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.

2
gcc/ada/exp_disp.adb
View File

@ -696,7 +696,7 @@ package body Exp_Disp is
-- 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

38
gcc/ada/exp_spark.adb
View File

@ -27,7 +27,6 @@ with Atree; use Atree;
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;
@ -38,10 +37,6 @@ package body Exp_SPARK is
-- 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
@ -71,9 +66,6 @@ package body Exp_SPARK is
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);
@ -88,36 +80,6 @@ package body Exp_SPARK is
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 --
------------------------------------------------

9
gcc/ada/opt.adb
View File

@ -38,15 +38,6 @@ package body Opt is
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 --
----------------------------------

12
gcc/ada/opt.ads
View File

@ -1939,9 +1939,6 @@ package Opt is
-- 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
@ -2023,15 +2020,6 @@ package Opt is
-- 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

2
gcc/ada/sem_aggr.adb
View File

@ -1700,7 +1700,7 @@ package body Sem_Aggr is
-- 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);

2
gcc/ada/sem_ch10.adb
View File

@ -2393,7 +2393,7 @@ package body Sem_Ch10 is
-- 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 =>

2
gcc/ada/sem_ch5.adb
View File

@ -2739,7 +2739,7 @@ package body Sem_Ch5 is
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))

6
gcc/ada/sem_ch6.adb
View File

@ -3200,7 +3200,7 @@ package body Sem_Ch6 is
-- 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)
@ -11447,7 +11447,7 @@ package body Sem_Ch6 is
-- 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);
@ -11486,7 +11486,7 @@ package body Sem_Ch6 is
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));

2
gcc/ada/sem_ch8.adb
View File

@ -2203,7 +2203,7 @@ package body Sem_Ch8 is
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;

6
gcc/ada/sem_ch9.adb
View File

@ -1326,7 +1326,7 @@ package body Sem_Ch9 is
-- 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
@ -2142,7 +2142,7 @@ package body Sem_Ch9 is
-- 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);
@ -2990,7 +2990,7 @@ package body Sem_Ch9 is
-- 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);

2
gcc/ada/sem_disp.adb
View File

@ -1264,7 +1264,7 @@ package body Sem_Disp is
-- 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;

26
gcc/ada/sem_res.adb
View File

@ -1762,7 +1762,7 @@ package body Sem_Res is
-- Start of processing for Replace_Actual_Discriminants
begin
if not Full_Expander_Active then
if not Expander_Active then
return;
end if;
@ -2033,7 +2033,7 @@ package body Sem_Res is
-- 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
@ -3608,7 +3608,7 @@ package body Sem_Res is
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);
@ -3624,7 +3624,7 @@ package body Sem_Res is
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)
@ -3687,7 +3687,7 @@ package body Sem_Res is
-- 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;
@ -5756,7 +5756,7 @@ package body Sem_Res is
then
null;
elsif Full_Expander_Active
elsif Expander_Active
and then Is_Type (Etype (Nam))
and then Requires_Transient_Scope (Etype (Nam))
and then
@ -6836,7 +6836,7 @@ package body Sem_Res is
-- 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);
@ -7139,7 +7139,7 @@ package body Sem_Res is
-- 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)
@ -7551,7 +7551,7 @@ package body Sem_Res is
-- 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;
@ -8670,7 +8670,7 @@ package body Sem_Res is
-- 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;
@ -9022,7 +9022,7 @@ package body Sem_Res is
-- 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
@ -9877,7 +9877,7 @@ package body Sem_Res is
-- 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
@ -10387,7 +10387,7 @@ package body Sem_Res is
-- 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;

43
gcc/ada/sinfo.ads
View File

@ -508,18 +508,18 @@ package Sinfo is
-- 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.
@ -527,16 +527,16 @@ package Sinfo is
-- 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
@ -544,11 +544,10 @@ package Sinfo is
-- 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 --