OpenE2K
/
gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[multiple changes] 

2015-10-26  Gary Dismukes  <dismukes@adacore.com>
        
        * a-reatim.adb, contracts.adb, contracts.ads: Minor reformatting and
        typo corrections.

2015-10-26  Ed Schonberg  <schonberg@adacore.com>
        
        * sem_ch13.adb (Check_Aspect_At_End_Of_Declarations): Do not
        recheck the consistency betwen the freeze point and the end of
        declarations for the expression in an aspect specification,
        because it was done already in the analysis of the generic.
        Furthermore, the delayed analysis of an aspect of the instance
        may produce spurious errors when the generic is a child unit
        that references entities in the parent (which might not be in
        scope at the freeze point of the instance).

2015-10-26  Yannick Moy  <moy@adacore.com>
        
        * sem_res.adb (Resolve_Call): Issue info message
        instead of warning when call cannot be inlined in GNATprove mode.

2015-10-26  Arnaud Charlet  <charlet@adacore.com>
        
        * exp_ch6.adb (Build_Procedure_Form): Use _result as the
        name of the extra parameter, cleaner than a random temp name.
        * gnat1drv.adb (Gnat1drv): Code clean up.

From-SVN: r229314
This commit is contained in:
Arnaud Charlet 2015-10-26 11:12:40 +01:00
parent c1fffdf1fb
commit e96b7045d6
8 changed files with 107 additions and 65 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
gcc/ada/ChangeLog
View File

@ -1,3 +1,30 @@
2015-10-26 Gary Dismukes <dismukes@adacore.com>
* a-reatim.adb, contracts.adb, contracts.ads: Minor reformatting and
typo corrections.
2015-10-26 Ed Schonberg <schonberg@adacore.com>
* sem_ch13.adb (Check_Aspect_At_End_Of_Declarations): Do not
recheck the consistency betwen the freeze point and the end of
declarations for the expression in an aspect specification,
because it was done already in the analysis of the generic.
Furthermore, the delayed analysis of an aspect of the instance
may produce spurious errors when the generic is a child unit
that references entities in the parent (which might not be in
scope at the freeze point of the instance).
2015-10-26 Yannick Moy <moy@adacore.com>
* sem_res.adb (Resolve_Call): Issue info message
instead of warning when call cannot be inlined in GNATprove mode.
2015-10-26 Arnaud Charlet <charlet@adacore.com>
* exp_ch6.adb (Build_Procedure_Form): Use _result as the
name of the extra parameter, cleaner than a random temp name.
* gnat1drv.adb (Gnat1drv): Code clean up.
2015-10-24 Eric Botcazou <ebotcazou@adacore.com>
* gcc-interface/utils2.c (build_binary_op): Tweak formatting.

4
gcc/ada/a-reatim.adb
View File

@ -123,7 +123,7 @@ is
-- rounding of the division operator in particular, to be the same as
-- effects on integer types. To get the correct rounding we first
-- convert Time_Span to its root type Duration, which is represented as
-- an 64-bit signed integer, and then use integer division.
-- a 64-bit signed integer, and then use integer division.
type Duration_Rep is range -(2 ** 63) .. +((2 ** 63 - 1));
@ -131,7 +131,7 @@ is
new Unchecked_Conversion (Duration, Duration_Rep);
begin
return Integer
(To_Integer (Duration (Left)) / To_Integer (Duration (Right)));
(To_Integer (Duration (Left)) / To_Integer (Duration (Right)));
end "/";
function "/" (Left : Time_Span; Right : Integer) return Time_Span is

103
gcc/ada/contracts.adb
View File

@ -268,7 +268,7 @@ package body Contracts is
begin
-- Climb the parent chain looking for an enclosing body. Do not use the
-- scope stack as a body uses the entity of its corresponding spec.
-- scope stack, as a body uses the entity of its corresponding spec.
Par := Parent (Body_Decl);
while Present (Par) loop
@ -300,13 +300,13 @@ package body Contracts is
begin
-- The loop parameter in an element iterator over a formal container
-- is declared with an object declaration but no contracts apply.
-- is declared with an object declaration, but no contracts apply.
if Ekind (Obj_Id) = E_Loop_Parameter then
return;
end if;
-- Do not analyze a contract mutiple times
-- Do not analyze a contract multiple times
Items := Contract (Obj_Id);
@ -318,13 +318,13 @@ package body Contracts is
end if;
end if;
-- Constant related checks
-- Constant-related checks
if Ekind (Obj_Id) = E_Constant then
-- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)).
-- This check is relevant only when SPARK_Mode is on as it is not a
-- standard Ada legality rule. Internally-generated constants that
-- This check is relevant only when SPARK_Mode is on, as it is not
-- a standard Ada legality rule. Internally-generated constants that
-- map generic formals to actuals in instantiations are allowed to
-- be volatile.
@ -336,11 +336,11 @@ package body Contracts is
Error_Msg_N ("constant cannot be volatile", Obj_Id);
end if;
-- Variable related checks
-- Variable-related checks
else pragma Assert (Ekind (Obj_Id) = E_Variable);
-- The following checks are relevant only when SPARK_Mode is on as
-- The following checks are relevant only when SPARK_Mode is on, as
-- they are not standard Ada legality rules. Internally generated
-- temporaries are ignored.
@ -452,7 +452,7 @@ package body Contracts is
-- A ghost object cannot be imported or exported (SPARK RM 6.9(8)). One
-- exception to this is the object that represents the dispatch table of
-- a Ghost tagged type as the symbol needs to be exported.
-- a Ghost tagged type, as the symbol needs to be exported.
if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then
if Is_Exported (Obj_Id) then
@ -479,7 +479,7 @@ package body Contracts is
Ref_State : Node_Id;
begin
-- Do not analyze a contract mutiple times
-- Do not analyze a contract multiple times
if Present (Items) then
if Analyzed (Items) then
@ -506,7 +506,7 @@ package body Contracts is
-- State refinement is required when the package declaration defines at
-- least one abstract state. Null states are not considered. Refinement
-- is not envorced when SPARK checks are turned off.
-- is not enforced when SPARK checks are turned off.
elsif SPARK_Mode /= Off
and then Requires_State_Refinement (Spec_Id, Body_Id)
@ -543,7 +543,7 @@ package body Contracts is
Prag_Nam : Name_Id;
begin
-- Do not analyze a contract mutiple times
-- Do not analyze a contract multiple times
if Present (Items) then
if Analyzed (Items) then
@ -562,7 +562,7 @@ package body Contracts is
if Present (Items) then
-- Locate and store pragmas Initial_Condition and Initializes since
-- Locate and store pragmas Initial_Condition and Initializes, since
-- their order of analysis matters.
Prag := Classifications (Items);
@ -579,7 +579,7 @@ package body Contracts is
Prag := Next_Pragma (Prag);
end loop;
-- Analyze the initialization related pragmas. Initializes must come
-- Analyze the initialization-related pragmas. Initializes must come
-- before Initial_Condition due to item dependencies.
if Present (Init) then
@ -639,7 +639,7 @@ package body Contracts is
if Ekind (Body_Id) = E_Void then
return;
-- Do not analyze a contract mutiple times
-- Do not analyze a contract multiple times
elsif Present (Items) then
if Analyzed (Items) then
@ -663,12 +663,12 @@ package body Contracts is
null;
-- The subprogram body is a completion, analyze all delayed pragmas that
-- apply. Note that when the body is stand alone, the pragmas are always
-- apply. Note that when the body is stand-alone, the pragmas are always
-- analyzed on the spot.
elsif Present (Items) then
-- Locate and store pragmas Refined_Depends and Refined_Global since
-- Locate and store pragmas Refined_Depends and Refined_Global, since
-- their order of analysis matters.
Prag := Classifications (Items);
@ -685,7 +685,7 @@ package body Contracts is
Prag := Next_Pragma (Prag);
end loop;
-- Analyze Refined_Global first as Refined_Depends may mention items
-- Analyze Refined_Global first, as Refined_Depends may mention items
-- classified in the global refinement.
if Present (Ref_Global) then
@ -705,9 +705,9 @@ package body Contracts is
Check_Result_And_Post_State (Body_Id);
-- A stand alone non-volatile function body cannot have an effectively
-- A stand-alone nonvolatile function body cannot have an effectively
-- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
-- check is relevant only when SPARK_Mode is on as it is not a standard
-- check is relevant only when SPARK_Mode is on, as it is not a standard
-- legality rule. The check is performed here because Volatile_Function
-- is processed after the analysis of the related subprogram body.
@ -755,7 +755,7 @@ package body Contracts is
Prag_Nam : Name_Id;
begin
-- Do not analyze a contract mutiple times
-- Do not analyze a contract multiple times
if Present (Items) then
if Analyzed (Items) then
@ -820,7 +820,7 @@ package body Contracts is
Prag := Next_Pragma (Prag);
end loop;
-- Analyze Global first as Depends may mention items classified in
-- Analyze Global first, as Depends may mention items classified in
-- the global categorization.
if Present (Global) then
@ -840,11 +840,11 @@ package body Contracts is
Check_Result_And_Post_State (Subp_Id);
end if;
-- A non-volatile function cannot have an effectively volatile formal
-- A nonvolatile function cannot have an effectively volatile formal
-- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
-- only when SPARK_Mode is on as it is not a standard legality rule. The
-- check is performed here because pragma Volatile_Function is processed
-- after the analysis of the related subprogram declaration.
-- only when SPARK_Mode is on, as it is not a standard legality rule.
-- The check is performed here because pragma Volatile_Function is
-- processed after the analysis of the related subprogram declaration.
if SPARK_Mode = On
and then Ekind_In (Subp_Id, E_Function, E_Generic_Function)
@ -1368,7 +1368,7 @@ package body Contracts is
-- If the pragma is a conjunct in a composite postcondition, it
-- has been processed in reverse order. In the postcondition body
-- if must appear before the others.
-- it must appear before the others.
if Nkind (Item) = N_Pragma
and then From_Aspect_Specification (Item)
@ -1451,7 +1451,7 @@ package body Contracts is
Set_Debug_Info_Needed (Proc_Id);
Set_Postconditions_Proc (Subp_Id, Proc_Id);
-- The related subprogram is a function, create the specification of
-- The related subprogram is a function: create the specification of
-- parameter _Result.
if Present (Result) then
@ -1464,7 +1464,7 @@ package body Contracts is
-- Insert _Postconditions before the first source declaration of the
-- body. This ensures that the body will not cause any premature
-- freezing as it may mention types:
-- freezing, as it may mention types:
-- procedure Proc (Obj : Array_Typ) is
-- procedure _postconditions is
@ -1476,14 +1476,14 @@ package body Contracts is
-- begin
-- In the example above, Obj is of type T but the incorrect placement
-- of _Postconditions will cause a crash in gigi due to an out of
-- of _Postconditions will cause a crash in gigi due to an out-of-
-- order reference. The body of _Postconditions must be placed after
-- the declaration of Temp to preserve correct visibility.
-- Set an explicit End_Lavel to override the sloc of the implicit
-- Set an explicit End_Label to override the sloc of the implicit
-- RETURN statement, and prevent it from inheriting the sloc of one
-- the postconditions: this would cause confusing debug into to be
-- produced, interfering with coverage analysis tools.
-- the postconditions: this would cause confusing debug info to be
-- produced, interfering with coverage-analysis tools.
Proc_Bod :=
Make_Subprogram_Body (Loc,
@ -1701,11 +1701,11 @@ package body Contracts is
procedure Process_Postconditions (Stmts : in out List_Id) is
procedure Process_Body_Postconditions (Post_Nam : Name_Id);
-- Collect all [refined] postconditions of a specific kind denoted
-- by Post_Nam that belong to the body and generate pragma Check
-- by Post_Nam that belong to the body, and generate pragma Check
-- equivalents in list Stmts.
procedure Process_Spec_Postconditions;
-- Collect all [inherited] postconditions of the spec and generate
-- Collect all [inherited] postconditions of the spec, and generate
-- pragma Check equivalents in list Stmts.
---------------------------------
@ -1736,7 +1736,7 @@ package body Contracts is
-- The subprogram body being processed is actually the proper body
-- of a stub with a corresponding spec. The subprogram stub may
-- carry a postcondition pragma in which case it must be taken
-- carry a postcondition pragma, in which case it must be taken
-- into account. The pragma appears after the stub.
if Present (Spec_Id) and then Nkind (Unit_Decl) = N_Subunit then
@ -1867,8 +1867,8 @@ package body Contracts is
-- Prepend a single item to the declarations of the subprogram body
procedure Prepend_To_Decls_Or_Save (Prag : Node_Id);
-- Save a class-wide precondition into Class_Pre or prepend a normal
-- precondition ot the declarations of the body and analyze it.
-- Save a class-wide precondition into Class_Pre, or prepend a normal
-- precondition to the declarations of the body and analyze it.
procedure Process_Inherited_Preconditions;
-- Collect all inherited class-wide preconditions and merge them into
@ -1885,7 +1885,7 @@ package body Contracts is
procedure Merge_Preconditions (From : Node_Id; Into : Node_Id) is
function Expression_Arg (Prag : Node_Id) return Node_Id;
-- Return the boolean expression argument of a precondition while
-- updating its parenteses count for the subsequent merge.
-- updating its parentheses count for the subsequent merge.
function Message_Arg (Prag : Node_Id) return Node_Id;
-- Return the message argument of a precondition
@ -1979,7 +1979,7 @@ package body Contracts is
Check_Prag := Build_Pragma_Check_Equivalent (Prag);
-- Save the sole class-wide precondition (if any) for the next
-- step where it will be merged with inherited preconditions.
-- step, where it will be merged with inherited preconditions.
if Class_Present (Prag) then
pragma Assert (No (Class_Pre));
@ -2032,7 +2032,7 @@ package body Contracts is
Subp_Id => Spec_Id,
Inher_Id => Subp_Id);
-- The spec or an inherited subprogram already yielded
-- The spec of an inherited subprogram already yielded
-- a class-wide precondition. Merge the existing
-- precondition with the current one using "or else".
@ -2081,8 +2081,9 @@ package body Contracts is
end if;
-- The subprogram declaration being processed is actually a body
-- stub. The stub may carry a precondition pragma in which case it
-- must be taken into account. The pragma appears after the stub.
-- stub. The stub may carry a precondition pragma, in which case
-- it must be taken into account. The pragma appears after the
-- stub.
Subp_Decl := Unit_Declaration_Node (Subp_Id);
@ -2125,7 +2126,7 @@ package body Contracts is
-- Start of processing for Process_Preconditions
begin
-- Find the last internally generate declaration starting from the
-- Find the last internally generated declaration, starting from the
-- top of the body declarations. This ensures that discriminals and
-- subtypes are properly visible to the pragma Check equivalents.
@ -2139,7 +2140,7 @@ package body Contracts is
end if;
-- The processing of preconditions is done in reverse order (body
-- first) because each pragma Check equivalent is inserted at the
-- first), because each pragma Check equivalent is inserted at the
-- top of the declarations. This ensures that the final order is
-- consistent with following diagram:
@ -2189,7 +2190,7 @@ package body Contracts is
return;
-- The contract of a generic subprogram or one declared in a generic
-- context is not expanded as the corresponding instance will provide
-- context is not expanded, as the corresponding instance will provide
-- the executable semantics of the contract.
elsif Is_Generic_Subprogram (Subp_Id) or else Inside_A_Generic then
@ -2201,7 +2202,7 @@ package body Contracts is
elsif not Has_Significant_Contract (Subp_Id) then
return;
-- The contract of an ignored Ghost subprogram does not need expansion
-- The contract of an ignored Ghost subprogram does not need expansion,
-- because the subprogram and all calls to it will be removed.
elsif Is_Ignored_Ghost_Entity (Subp_Id) then
@ -2281,7 +2282,7 @@ package body Contracts is
-- Step 3: Handle pragma Contract_Cases. This action must come before
-- the processing of invariants and predicates because those append
-- items to list Smts.
-- items to list Stmts.
Process_Contract_Cases (Stmts);
@ -2322,7 +2323,7 @@ package body Contracts is
begin
-- A pragma cannot be part of more than one First_Pragma/Next_Pragma
-- chains, therefore the node must be replicated. The new pragma is
-- flagged is inherited for distrinction purposes.
-- flagged as inherited for distinction purposes.
if Present (Prag) then
New_Prag := New_Copy_Tree (Prag);
@ -2352,7 +2353,7 @@ package body Contracts is
procedure Instantiate_Subprogram_Contract (Templ : Node_Id; L : List_Id) is
procedure Instantiate_Pragmas (First_Prag : Node_Id);
-- Instantiate all contract-related source pragmas found in the list
-- Instantiate all contract-related source pragmas found in the list,
-- starting with pragma First_Prag. Each instantiated pragma is added
-- to list L.
@ -2403,7 +2404,7 @@ package body Contracts is
is
procedure Save_Global_References_In_List (First_Prag : Node_Id);
-- Save all global references in contract-related source pragmas found
-- in the list starting with pragma First_Prag.
-- in the list, starting with pragma First_Prag.
------------------------------------
-- Save_Global_References_In_List --

8
gcc/ada/contracts.ads
View File

@ -32,7 +32,7 @@ package Contracts is
procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id);
-- Add pragma Prag to the contract of a constant, entry, package [body],
-- subprogram [body] or variable denoted by Id. The following are valid
-- subprogram [body], or variable denoted by Id. The following are valid
-- pragmas:
-- Abstract_State
-- Async_Readers
@ -57,7 +57,7 @@ package Contracts is
-- Volatile_Function
procedure Analyze_Enclosing_Package_Body_Contract (Body_Decl : Node_Id);
-- Analyze the contract of the nearest package body (if any) which encloses
-- Analyze the contract of the nearest package body (if any) enclosing
-- package or subprogram body Body_Decl.
procedure Analyze_Object_Contract (Obj_Id : Entity_Id);
@ -79,7 +79,7 @@ package Contracts is
-- Refined_State
--
-- Freeze_Id is the entity of a [generic] package body or a [generic]
-- subprogram body which "feezes" the contract of Body_Id.
-- subprogram body which "freezes" the contract of Body_Id.
procedure Analyze_Package_Contract (Pack_Id : Entity_Id);
-- Analyze all delayed aspects chained on the contract of package Pack_Id
@ -129,7 +129,7 @@ package Contracts is
-- Test_Case
procedure Create_Generic_Contract (Unit : Node_Id);
-- Create a contract node for a generic package, generic subprogram or a
-- Create a contract node for a generic package, generic subprogram, or a
-- generic body denoted by Unit by collecting all source contract-related
-- pragmas in the contract of the unit.

7
gcc/ada/exp_ch6.adb
View File

@ -5495,7 +5495,7 @@ package body Exp_Ch6 is
procedure Build_Procedure_Form;
-- Create a procedure declaration which emulates the behavior of
-- function Subp, for SPARK_To_C.
-- function Subp, for C-compatible generation.
--------------------------
-- Build_Procedure_Form --
@ -5525,9 +5525,12 @@ package body Exp_Ch6 is
-- Add an extra out parameter to carry the function result
Name_Len := 7;
Name_Buffer (1 .. Name_Len) := "_result";
Append_To (Proc_Formals,
Make_Parameter_Specification (Loc,
Defining_Identifier => Make_Temporary (Loc, 'R'),
Defining_Identifier =>
Make_Defining_Identifier (Loc, Chars => Name_Find),
Out_Present => True,
Parameter_Type => New_Occurrence_Of (Etype (Subp), Loc)));

3
gcc/ada/gnat1drv.adb
View File

@ -1180,8 +1180,9 @@ begin
-- It is not an error to analyze in CodePeer mode a spec which requires
-- a body, in order to generate SCIL for this spec.
-- Ditto for Generate_C_Code mode and generate a C header for a spec.
elsif CodePeer_Mode then
elsif CodePeer_Mode or Generate_C_Code then
Back_End_Mode := Generate_Object;
-- It is not an error to analyze in GNATprove mode a spec which requires

12
gcc/ada/sem_ch13.adb
View File

@ -9103,9 +9103,19 @@ package body Sem_Ch13 is
-- Start of processing for Check_Aspect_At_End_Of_Declarations
begin
-- In an instance we do not perform the consistency check between freeze
-- point and end of declarations, because it was done already in the
-- analysis of the generic. Furthermore, the delayed analysis of an
-- aspect of the instance may produce spurious errors when the generic
-- is a child unit that references entities in the parent (which might
-- not be in scope at the freeze point of the instance).
if In_Instance then
return;
-- Case of aspects Dimension, Dimension_System and Synchronization
if A_Id = Aspect_Synchronization then
elsif A_Id = Aspect_Synchronization then
return;
-- Case of stream attributes, just have to compare entities. However,

8
gcc/ada/sem_res.adb
View File

@ -6409,14 +6409,14 @@ package body Sem_Res is
-- assertions as logic expressions.
elsif In_Assertion_Expr /= 0 then
Error_Msg_NE ("?no contextual analysis of &", N, Nam);
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);
-- Calls cannot be inlined inside default expressions
elsif In_Default_Expr then
Error_Msg_NE ("?no contextual analysis of &", N, Nam);
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);
@ -6429,7 +6429,7 @@ package body Sem_Res is
if No (Body_Id) then
Error_Msg_NE
("?no contextual analysis of & (body not seen yet)",
("info: no contextual analysis of & (body not seen yet)?",
N, Nam);
Set_Is_Inlined_Always (Nam_UA, False);
@ -6445,7 +6445,7 @@ package body Sem_Res is
-- expressions, that are not handled by GNATprove.
elsif Is_Potentially_Unevaluated (N) then
Error_Msg_NE ("?no contextual analysis of &", N, Nam);
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);