+2016-04-18 Yannick Moy <moy@adacore.com>
+
+ * sem_res.adb (Resolve_Call): Prevent inlining of
+ calls inside expression functions. Factor previous code issuing
+ errors to call Cannot_Inline instead, which does appropriate
+ processing of message for GNATprove.
+
+2016-04-18 Arnaud Charlet <charlet@adacore.com>
+
+ * einfo.ads, sem_ch3.adb, sem_ch8.adb, osint-l.adb, rtsfind.adb,
+ osint-b.adb: Cleanups.
+
+2016-04-18 Yannick Moy <moy@adacore.com>
+
+ * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Only create
+ body to inline in GNATprove mode when SPARK_Mode On applies to
+ subprogram body.
+ * sem_prag.adb, sem_prag.ads (Get_SPARK_Mode_Type): Make function
+ public.
+
+2016-04-18 Eric Botcazou <ebotcazou@adacore.com>
+
+ * layout.adb: Fix minor typo in comment.
+ * inline.adb: Fix minor pasto.
+ * sem_ch12.ads: Fix minor typos in comments.
+
2016-04-18 Ed Schonberg <schonberg@adacore.com>
* sem_disp.adb (Check_Dispatching_Call): Major rewriting to
-- Next_Discriminant (synthesized)
-- Applies to discriminants returned by First/Next_Discriminant. Returns
--- the next language-defined (ie: perhaps non-girder) discriminant by
+-- the next language-defined (i.e. perhaps non-girder) discriminant by
-- following the chain of declared entities as long as the kind of the
-- entity corresponds to a discriminant. Note that the discriminants
-- might be the only components of the record. Returns Empty if there
-- We can now complete the cleanup actions of scopes that contain
-- pending instantiations (skipped for generic units, since we
-- never need any cleanups in generic units).
- -- pending instantiations.
if Expander_Active
and then not Is_Generic_Unit (Main_Unit_Entity)
-- we have no way of doing that or easily figuring it out, so we
-- don't bother.
- -- Historical note. In versions of GNAT prior to Nov 6th, 2010, an
+ -- Historical note. In versions of GNAT prior to Nov 6th, 2011, an
-- odd distinction was made between inherited alignments greater
-- than the computed alignment (where the larger alignment was
-- inherited) and inherited alignments smaller than the computed
-- --
-- B o d y --
-- --
--- Copyright (C) 2001-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 2001-2015, 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- --
-- More_Lib_Files --
--------------------
- function More_Lib_Files return Boolean renames More_Files;
+ function More_Lib_Files return Boolean renames More_Files;
------------------------
-- Next_Main_Lib_File --
-- --
-- B o d y --
-- --
--- Copyright (C) 2001-2007, Free Software Foundation, Inc. --
+-- Copyright (C) 2001-2015, 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- --
-- More_Lib_Files --
--------------------
- function More_Lib_Files return Boolean renames More_Files;
+ function More_Lib_Files return Boolean renames More_Files;
------------------------
-- Next_Main_Lib_File --
declare
U : RT_Unit_Table_Record
- renames RT_Unit_Table (RE_Unit_Table (E));
+ renames RT_Unit_Table (RE_Unit_Table (E));
begin
if No (U.Entity) then
U.Entity := S;
Body_Optional : Boolean := False);
-- Called after semantic analysis, to complete the instantiation of
-- package instances. The flag Inlined_Body is set if the body is
- -- being instantiated on the fly for inlined purposes.
+ -- being instantiated on the fly for inlining purposes.
--
-- The flag Body_Optional indicates that the call is for an instance
-- that precedes the current instance in the same declarative part.
-- appears in the context of some other unit P that contains an instance
-- of G, we compile the body of I2, but not that of I1. However, when we
-- compile U as the main unit, we compile both bodies. This will lead to
- -- lead to link-time errors if the compilation of I1 generates public
- -- symbols, because those in I2 will receive different names in both
- -- cases. This forces us to analyze the body of I1 even when U is not the
- -- main unit. We don't want this additional mechanism to generate an error
+ -- link-time errors if the compilation of I1 generates public symbols,
+ -- because those in I2 will receive different names in both cases.
+ -- This forces us to analyze the body of I1 even when U is not the main
+ -- unit. We don't want this additional mechanism to generate an error
-- when the body of the generic for I1 is not present, and this is the
-- reason for the presence of the flag Body_Optional, which is exchanged
-- between the current procedure and Load_Parent_Of_Generic.
end if;
elsif Is_Dispatching_Operation (Prim)
- and then Disp_Typ /= Full_T
+ and then Disp_Typ /= Full_T
then
-- Verify that it is not otherwise controlled by a
-- Check whether unanalyzed body has an aspect or pragma that may
-- generate a SPARK contract.
+ function Body_Has_SPARK_Mode_On return Boolean;
+ -- Check whether SPARK_Mode On applies to the subprogram body, either
+ -- because it is specified directly on the body, or because it is
+ -- inherited from the enclosing subprogram or package.
+
procedure Build_Subprogram_Declaration;
-- Create a matching subprogram declaration for subprogram body N
return False;
end Body_Has_Contract;
+ ----------------------------
+ -- Body_Has_SPARK_Mode_On --
+ ----------------------------
+
+ function Body_Has_SPARK_Mode_On return Boolean is
+ Decls : constant List_Id := Declarations (N);
+ Item : Node_Id;
+
+ begin
+ -- Check for SPARK_Mode aspect
+
+ if Present (Aspect_Specifications (N)) then
+ Item := First (Aspect_Specifications (N));
+ while Present (Item) loop
+ if Get_Aspect_Id (Item) = Aspect_SPARK_Mode then
+ return No (Expression (Item))
+ or else
+ (Nkind (Expression (Item)) = N_Identifier
+ and then
+ Get_SPARK_Mode_Type (Chars (Expression (Item))) = On);
+ end if;
+
+ Next (Item);
+ end loop;
+ end if;
+
+ -- Check for SPARK_Mode pragma
+
+ if Present (Decls) then
+ Item := First (Decls);
+ while Present (Item) loop
+ if Nkind (Item) = N_Pragma
+ and then Get_Pragma_Id (Item) = Pragma_SPARK_Mode
+ then
+ return Get_SPARK_Mode_From_Pragma (Item) = On;
+ end if;
+
+ Next (Item);
+ end loop;
+ end if;
+
+ -- Applicable SPARK_Mode is inherited from the enclosing subprogram
+ -- or package.
+
+ return SPARK_Mode = On;
+ end Body_Has_SPARK_Mode_On;
+
----------------------------------
-- Build_Subprogram_Declaration --
----------------------------------
and then Present (Spec_Id)
and then
Nkind (Unit_Declaration_Node (Spec_Id)) = N_Subprogram_Declaration
+ and then Body_Has_SPARK_Mode_On
and then Can_Be_Inlined_In_GNATprove_Mode (Spec_Id, Body_Id)
and then not Body_Has_Contract
then
Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id);
- -- If SPARK_Mode for body is not On, disable frontend inlining for this
- -- subprogram in GNATprove mode, as its body should not be analyzed.
-
- if SPARK_Mode /= On
- and then GNATprove_Mode
- and then Present (Spec_Id)
- and then Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Declaration
- then
- Set_Body_To_Inline (Parent (Parent (Spec_Id)), Empty);
- Set_Is_Inlined_Always (Spec_Id, False);
- end if;
-
-- Check completion, and analyze the statements
Check_Completion;
-- array of Boolean type.
when Name_Op_And | Name_Op_Not | Name_Op_Or | Name_Op_Xor =>
- while Id /= Priv_Id loop
+ while Id /= Priv_Id loop
if Valid_Boolean_Arg (Id) and then Is_Base_Type (Id) then
Add_Implicit_Operator (Id);
return True;
-- Equality: look for any non-limited type (result is Boolean)
when Name_Op_Eq | Name_Op_Ne =>
- while Id /= Priv_Id loop
+ while Id /= Priv_Id loop
if Is_Type (Id)
and then not Is_Limited_Type (Id)
and then Is_Base_Type (Id)
-- Comparison operators: scalar type, or array of scalar
when Name_Op_Lt | Name_Op_Le | Name_Op_Gt | Name_Op_Ge =>
- while Id /= Priv_Id loop
+ while Id /= Priv_Id loop
if (Is_Scalar_Type (Id)
or else (Is_Array_Type (Id)
and then Is_Scalar_Type (Component_Type (Id))))
Name_Op_Multiply |
Name_Op_Divide |
Name_Op_Expon =>
- while Id /= Priv_Id loop
+ while Id /= Priv_Id loop
if Is_Numeric_Type (Id) and then Is_Base_Type (Id) then
Add_Implicit_Operator (Id);
return True;
-- Concatenation: any one-dimensional array type
when Name_Op_Concat =>
- while Id /= Priv_Id loop
+ while Id /= Priv_Id loop
if Is_Array_Type (Id)
and then Number_Dimensions (Id) = 1
and then Is_Base_Type (Id)
-- original one, following the renaming chain) is returned. Otherwise the
-- entity is returned unchanged. Should be in Einfo???
- function Get_SPARK_Mode_Type (N : Name_Id) return SPARK_Mode_Type;
- -- Subsidiary to the analysis of pragma SPARK_Mode as well as subprogram
- -- Get_SPARK_Mode_Type. Convert a name into a corresponding value of type
- -- SPARK_Mode_Type.
-
function Has_Extra_Parentheses (Clause : Node_Id) return Boolean;
-- Subsidiary to the analysis of pragmas Depends and Refined_Depends.
-- Determine whether dependency clause Clause is surrounded by extra
function Get_SPARK_Mode_From_Pragma (N : Node_Id) return SPARK_Mode_Type;
-- Given a pragma SPARK_Mode node, return corresponding mode id
+ function Get_SPARK_Mode_Type (N : Name_Id) return SPARK_Mode_Type;
+ -- Subsidiary to the analysis of pragma SPARK_Mode as well as subprogram
+ -- Get_SPARK_Mode_From_Pragma. Convert a name into a corresponding value
+ -- of type SPARK_Mode_Type.
+
procedure Initialize;
-- Initializes data structures used for pragma processing. Must be called
-- before analyzing each new main source program.
-- assertions as logic expressions.
elsif In_Assertion_Expr /= 0 then
- Error_Msg_NE ("info: no contextual analysis of &?", N, Nam);
- Error_Msg_N ("\call appears in assertion expression", N);
- Set_Is_Inlined_Always (Nam_UA, False);
+ Cannot_Inline
+ ("cannot inline & (in assertion expression)?", N, Nam_UA);
-- Calls cannot be inlined inside default expressions
elsif In_Default_Expr then
- Error_Msg_NE ("info: no contextual analysis of &?", N, Nam);
- Error_Msg_N ("\call appears in default expression", N);
- Set_Is_Inlined_Always (Nam_UA, False);
+ Cannot_Inline
+ ("cannot inline & (in default expression)?", N, Nam_UA);
-- Inlining should not be performed during pre-analysis
-- inlined if the corresponding body has not been seen yet.
if No (Body_Id) then
- Error_Msg_NE
- ("info: no contextual analysis of & (body not seen yet)?",
- N, Nam);
- Set_Is_Inlined_Always (Nam_UA, False);
+ Cannot_Inline
+ ("cannot inline & (body not seen yet)?", N, Nam_UA);
-- Nothing to do if there is no body to inline, indicating that
-- the subprogram is not suitable for inlining in GNATprove
elsif No (Body_To_Inline (Nam_Decl)) then
null;
+ -- Do not inline calls inside expression functions, as this
+ -- would prevent interpreting them as logical formulas in
+ -- GNATprove.
+
+ elsif Present (Current_Subprogram)
+ and then
+ Is_Expression_Function_Or_Completion (Current_Subprogram)
+ then
+ Cannot_Inline
+ ("cannot inline & (inside expression function)?",
+ N, Nam_UA);
+
-- Calls cannot be inlined inside potentially unevaluated
-- expressions, as this would create complex actions inside
-- expressions, that are not handled by GNATprove.
elsif Is_Potentially_Unevaluated (N) then
- Error_Msg_NE ("info: no contextual analysis of &?", N, Nam);
- Error_Msg_N
- ("\call appears in potentially unevaluated context", N);
- Set_Is_Inlined_Always (Nam_UA, False);
+ Cannot_Inline
+ ("cannot inline & (in potentially unevaluated context)?",
+ N, Nam_UA);
-- Otherwise, inline the call
projects / thirdparty / gcc.git / commitdiff
