Skip to content

R
riscv-gcc-1
Commit 539ca5ec by Arnaud Charlet
Options

[multiple changes] 

2016-04-18  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): In GNATprove
	mode, collect inherited class-wide conditions to generate the
	corresponding pragmas.
	* sem_prag.ads (Build_Pragma_Check_Equivalent): Moved from contracts
	* contracts.adb (Collect_Inherited_Class_Wide_Conditions): New
	procedure for overriding subprograms, used to generate the pragmas
	corresponding to an inherited class- wide pre- or postcondition.
	* sem_prag.adb (Build_Pragma_Check_Equivalent): moved here
	from contracts.adb (Replace_Condition_Entities): Subsidiary
	Build_Pragma_Check_Equivalent, to implement the proper semantics
	of inherited class-wide conditions, as given in AI12-0113.
	(Process_Class_Wide_Condition): Removed.
	(Collect_Inherited_Class_Wide_Conditions): Iterate over pragmas
	in contract of subprogram, to collect inherited class-wide
	conditions.
	(Build_Pragma_Check_Equivalent): Moved to sem_prag.adb

2016-04-18  Yannick Moy  <moy@adacore.com>

	* a-calend.adb (Ada.Calendar): Mark package body as SPARK_Mode Off.
	* a-calend.ads (Ada.Calendar): Mark package spec as
	SPARK_Mode and add synchronous external abstract state Clock_Time.

From-SVN: r235113
parent fd22e260
Showing with 71 additions and 163 deletions
gcc/ada/ChangeLog
2016-04-18 Ed Schonberg <schonberg@adacore.com>
* sem_ch6.adb (Analyze_Subprogram_Body_Helper): In GNATprove
mode, collect inherited class-wide conditions to generate the
corresponding pragmas.
* sem_prag.ads (Build_Pragma_Check_Equivalent): Moved from contracts
* contracts.adb (Collect_Inherited_Class_Wide_Conditions): New
procedure for overriding subprograms, used to generate the pragmas
corresponding to an inherited class- wide pre- or postcondition.
* sem_prag.adb (Build_Pragma_Check_Equivalent): moved here
from contracts.adb (Replace_Condition_Entities): Subsidiary
Build_Pragma_Check_Equivalent, to implement the proper semantics
of inherited class-wide conditions, as given in AI12-0113.
(Process_Class_Wide_Condition): Removed.
(Collect_Inherited_Class_Wide_Conditions): Iterate over pragmas
in contract of subprogram, to collect inherited class-wide
conditions.
(Build_Pragma_Check_Equivalent): Moved to sem_prag.adb
2016-04-18 Yannick Moy <moy@adacore.com>
* a-calend.adb (Ada.Calendar): Mark package body as SPARK_Mode Off.
* a-calend.ads (Ada.Calendar): Mark package spec as
SPARK_Mode and add synchronous external abstract state Clock_Time.
2016-04-18 Yannick Moy <moy@adacore.com> 2016-04-18 Yannick Moy <moy@adacore.com>
* sem_res.adb (Resolve_Call): Prevent inlining of * sem_res.adb (Resolve_Call): Prevent inlining of
......
gcc/ada/a-calend.adb
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
-- -- -- --
-- B o d y -- -- B o d y --
-- -- -- --
-- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- -- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
-- -- -- --
-- GNAT is free software; you can redistribute it and/or modify it under -- -- 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- -- -- terms of the GNU General Public License as published by the Free Soft- --
...@@ -35,7 +35,9 @@ with Interfaces.C; ...@@ -35,7 +35,9 @@ with Interfaces.C;
with System.OS_Primitives; with System.OS_Primitives;
package body Ada.Calendar is package body Ada.Calendar with
SPARK_Mode => Off
is
-------------------------- --------------------------
-- Implementation Notes -- -- Implementation Notes --
......
gcc/ada/a-calend.ads
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
-- -- -- --
-- S p e c -- -- S p e c --
-- -- -- --
-- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- -- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
-- -- -- --
-- This specification is derived from the Ada Reference Manual for use with -- -- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow -- -- GNAT. The copyright notice above, and the license provisions that follow --
...@@ -33,7 +33,12 @@ ...@@ -33,7 +33,12 @@
-- -- -- --
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
package Ada.Calendar is package Ada.Calendar with
SPARK_Mode,
Abstract_State => (Clock_Time with Synchronous,
External => (Async_Readers,
Async_Writers))
is
type Time is private; type Time is private;
...@@ -49,7 +54,9 @@ package Ada.Calendar is ...@@ -49,7 +54,9 @@ package Ada.Calendar is
subtype Day_Duration is Duration range 0.0 .. 86_400.0; subtype Day_Duration is Duration range 0.0 .. 86_400.0;
function Clock return Time; function Clock return Time with
Volatile_Function,
Global => Clock_Time;
-- The returned time value is the number of nanoseconds since the start -- The returned time value is the number of nanoseconds since the start
-- of Ada time (1901-01-01 00:00:00.0 UTC). If leap seconds are enabled, -- of Ada time (1901-01-01 00:00:00.0 UTC). If leap seconds are enabled,
-- the result will contain all elapsed leap seconds since the start of -- the result will contain all elapsed leap seconds since the start of
...@@ -108,6 +115,10 @@ package Ada.Calendar is ...@@ -108,6 +115,10 @@ package Ada.Calendar is
Time_Error : exception; Time_Error : exception;
private private
-- Mark private part as SPARK_Mode Off to avoid accounting for variable
-- Invalid_Time_Zone_Offset in abstract state.
pragma SPARK_Mode (Off);
pragma Inline (Clock); pragma Inline (Clock);
pragma Inline (Year); pragma Inline (Year);
......
gcc/ada/contracts.adb
...@@ -1432,15 +1432,6 @@ package body Contracts is ...@@ -1432,15 +1432,6 @@ package body Contracts is
-- of statements to be checked on exit. Parameter Result is the entity -- of statements to be checked on exit. Parameter Result is the entity
-- of parameter _Result when Subp_Id denotes a function. -- of parameter _Result when Subp_Id denotes a function.
function Build_Pragma_Check_Equivalent
(Prag : Node_Id;
Subp_Id : Entity_Id := Empty;
Inher_Id : Entity_Id := Empty) return Node_Id;
-- Transform a [refined] pre- or postcondition denoted by Prag into an
-- equivalent pragma Check. When the pre- or postcondition is inherited,
-- the routine corrects the references of all formals of Inher_Id to
-- point to the formals of Subp_Id.
procedure Process_Contract_Cases (Stmts : in out List_Id); procedure Process_Contract_Cases (Stmts : in out List_Id);
-- Process pragma Contract_Cases. This routine prepends items to the -- Process pragma Contract_Cases. This routine prepends items to the
-- body declarations and appends items to list Stmts. -- body declarations and appends items to list Stmts.
...@@ -1860,155 +1851,6 @@ package body Contracts is ...@@ -1860,155 +1851,6 @@ package body Contracts is
Analyze (Proc_Bod); Analyze (Proc_Bod);
end Build_Postconditions_Procedure; end Build_Postconditions_Procedure;
-----------------------------------
-- Build_Pragma_Check_Equivalent --
-----------------------------------
function Build_Pragma_Check_Equivalent
(Prag : Node_Id;
Subp_Id : Entity_Id := Empty;
Inher_Id : Entity_Id := Empty) return Node_Id
is
function Suppress_Reference (N : Node_Id) return Traverse_Result;
-- Detect whether node N references a formal parameter subject to
-- pragma Unreferenced. If this is the case, set Comes_From_Source
-- to False to suppress the generation of a reference when analyzing
-- N later on.
------------------------
-- Suppress_Reference --
------------------------
function Suppress_Reference (N : Node_Id) return Traverse_Result is
Formal : Entity_Id;
begin
if Is_Entity_Name (N) and then Present (Entity (N)) then
Formal := Entity (N);
-- The formal parameter is subject to pragma Unreferenced.
-- Prevent the generation of a reference by resetting the
-- Comes_From_Source flag.
if Is_Formal (Formal)
and then Has_Pragma_Unreferenced (Formal)
then
Set_Comes_From_Source (N, False);
end if;
end if;
return OK;
end Suppress_Reference;
procedure Suppress_References is
new Traverse_Proc (Suppress_Reference);
-- Local variables
Loc : constant Source_Ptr := Sloc (Prag);
Prag_Nam : constant Name_Id := Pragma_Name (Prag);
Check_Prag : Node_Id;
Formals_Map : Elist_Id;
Inher_Formal : Entity_Id;
Msg_Arg : Node_Id;
Nam : Name_Id;
Subp_Formal : Entity_Id;
-- Start of processing for Build_Pragma_Check_Equivalent
begin
Formals_Map := No_Elist;
-- When the pre- or postcondition is inherited, map the formals of
-- the inherited subprogram to those of the current subprogram.
if Present (Inher_Id) then
pragma Assert (Present (Subp_Id));
Formals_Map := New_Elmt_List;
-- Create a relation <inherited formal> => <subprogram formal>
Inher_Formal := First_Formal (Inher_Id);
Subp_Formal := First_Formal (Subp_Id);
while Present (Inher_Formal) and then Present (Subp_Formal) loop
Append_Elmt (Inher_Formal, Formals_Map);
Append_Elmt (Subp_Formal, Formals_Map);
Next_Formal (Inher_Formal);
Next_Formal (Subp_Formal);
end loop;
end if;
-- Copy the original pragma while performing substitutions (if
-- applicable).
Check_Prag :=
New_Copy_Tree
(Source => Prag,
Map => Formals_Map,
New_Scope => Current_Scope);
-- Mark the pragma as being internally generated and reset the
-- Analyzed flag.
Set_Analyzed (Check_Prag, False);
Set_Comes_From_Source (Check_Prag, False);
-- The tree of the original pragma may contain references to the
-- formal parameters of the related subprogram. At the same time
-- the corresponding body may mark the formals as unreferenced:
-- procedure Proc (Formal : ...)
-- with Pre => Formal ...;
-- procedure Proc (Formal : ...) is
-- pragma Unreferenced (Formal);
-- ...
-- This creates problems because all pragma Check equivalents are
-- analyzed at the end of the body declarations. Since all source
-- references have already been accounted for, reset any references
-- to such formals in the generated pragma Check equivalent.
Suppress_References (Check_Prag);
if Present (Corresponding_Aspect (Prag)) then
Nam := Chars (Identifier (Corresponding_Aspect (Prag)));
else
Nam := Prag_Nam;
end if;
-- Convert the copy into pragma Check by correcting the name and
-- adding a check_kind argument.
Set_Pragma_Identifier
(Check_Prag, Make_Identifier (Loc, Name_Check));
Prepend_To (Pragma_Argument_Associations (Check_Prag),
Make_Pragma_Argument_Association (Loc,
Expression => Make_Identifier (Loc, Nam)));
-- Update the error message when the pragma is inherited
if Present (Inher_Id) then
Msg_Arg := Last (Pragma_Argument_Associations (Check_Prag));
if Chars (Msg_Arg) = Name_Message then
String_To_Name_Buffer (Strval (Expression (Msg_Arg)));
-- Insert "inherited" to improve the error message
if Name_Buffer (1 .. 8) = "failed p" then
Insert_Str_In_Name_Buffer ("inherited ", 8);
Set_Strval (Expression (Msg_Arg), String_From_Name_Buffer);
end if;
end if;
end if;
return Check_Prag;
end Build_Pragma_Check_Equivalent;
---------------------------- ----------------------------
-- Process_Contract_Cases -- -- Process_Contract_Cases --
---------------------------- ----------------------------
......
gcc/ada/sem_ch6.adb
...@@ -3754,6 +3754,17 @@ package body Sem_Ch6 is ...@@ -3754,6 +3754,17 @@ package body Sem_Ch6 is
Build_Body_To_Inline (N, Spec_Id); Build_Body_To_Inline (N, Spec_Id);
end if; end if;
-- When generating code, inherited pre/postconditions are handled
-- when expanding the corresponding contract. If GNATprove mode we
-- must process them when the body is analyzed.
if GNATprove_Mode
and then Present (Spec_Id)
and then Present (Overridden_Operation (Spec_Id))
then
Collect_Inherited_Class_Wide_Conditions (Spec_Id, N);
end if;
-- Ada 2005 (AI-262): In library subprogram bodies, after the analysis -- Ada 2005 (AI-262): In library subprogram bodies, after the analysis
-- of the specification we have to install the private withed units. -- of the specification we have to install the private withed units.
-- This holds for child units as well. -- This holds for child units as well.
......
gcc/ada/sem_prag.ads
...@@ -244,6 +244,16 @@ package Sem_Prag is ...@@ -244,6 +244,16 @@ package Sem_Prag is
procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id); procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id);
-- Perform preanalysis of pragma Test_Case -- Perform preanalysis of pragma Test_Case
function Build_Pragma_Check_Equivalent
(Prag : Node_Id;
Subp_Id : Entity_Id := Empty;
Inher_Id : Entity_Id := Empty) return Node_Id;
-- Transform a [refined] pre- or postcondition denoted by Prag into an
-- equivalent pragma Check. When the pre- or postcondition is inherited,
-- the routine replaces the references of all formals of Inher_Id and
-- primitive operations of its controlling type by references to the
-- corresponding entities of Subp_Id and the descendant type.
procedure Check_Applicable_Policy (N : Node_Id); procedure Check_Applicable_Policy (N : Node_Id);
-- N is either an N_Aspect or an N_Pragma node. There are two cases. If -- N is either an N_Aspect or an N_Pragma node. There are two cases. If
-- the name of the aspect or pragma is not one of those recognized as -- the name of the aspect or pragma is not one of those recognized as
...@@ -301,6 +311,13 @@ package Sem_Prag is ...@@ -301,6 +311,13 @@ package Sem_Prag is
-- state, variable or package instantiation denoted by Item_Id requires the -- state, variable or package instantiation denoted by Item_Id requires the
-- use of indicator/option Part_Of. If this is the case, emit an error. -- use of indicator/option Part_Of. If this is the case, emit an error.
procedure Collect_Inherited_Class_Wide_Conditions
(Subp : Entity_Id;
Bod : Node_Id);
-- When analyzing an overriding subprogram, check whether the overridden
-- operations have class-wide pre/postconditions, and generate the
-- corresponding pragmas.
procedure Collect_Subprogram_Inputs_Outputs procedure Collect_Subprogram_Inputs_Outputs
(Subp_Id : Entity_Id; (Subp_Id : Entity_Id;
Synthesize : Boolean := False; Synthesize : Boolean := False;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment