FreeChainXenon/gcc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

[multiple changes]

Browse source 
2014-07-30  Pat Rogers  <rogers@adacore.com>

	* gnat_rm.texi: Minor word error.

2014-07-30  Ed Schonberg  <schonberg@adacore.com>

	* exp_prag.adb (Expand_Old): Insert declarationss of temporaries
	created to capture the value of the prefix of 'Old at the
	beginning of the current declarative part, to prevent data flow
	anomalies in the postcondition procedure that will follow.

2014-07-30  Yannick Moy  <moy@adacore.com>

	* debug.adb: Retire debug flag -gnatdQ.
	* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Check SPARK_Mode
	on decl, not on body.  Ignore predicate functions.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Remove use of
	debug flag -gnatdQ.  Correctly analyze SPARK_Mode on decl and
	body when generating a decl for a body on which SPARK_Mode aspect
	is given.
	* sem_prag.adb (Analyze_Pragma|SPARK_Mode): Reorder tests for
	attaching pragma to entity, to account for declaration not coming
	from source.
	* sem_res.adb (Resolve_Call): Issue warning and flag subprogram
	as not always inlined in GNATprove mode, when called in an
	assertion context.

From-SVN: r213271
This commit is contained in:
Arnaud Charlet 2014-07-30 15:54:18 +02:00
parent d3e16619ae
commit 2178830b04
9 changed files with 131 additions and 35 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 @@
2014-07-30 Pat Rogers <rogers@adacore.com>
* gnat_rm.texi: Minor word error.
2014-07-30 Ed Schonberg <schonberg@adacore.com>
* exp_prag.adb (Expand_Old): Insert declarationss of temporaries
created to capture the value of the prefix of 'Old at the
beginning of the current declarative part, to prevent data flow
anomalies in the postcondition procedure that will follow.
2014-07-30 Yannick Moy <moy@adacore.com>
* debug.adb: Retire debug flag -gnatdQ.
* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Check SPARK_Mode
on decl, not on body. Ignore predicate functions.
* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Remove use of
debug flag -gnatdQ. Correctly analyze SPARK_Mode on decl and
body when generating a decl for a body on which SPARK_Mode aspect
is given.
* sem_prag.adb (Analyze_Pragma|SPARK_Mode): Reorder tests for
attaching pragma to entity, to account for declaration not coming
from source.
* sem_res.adb (Resolve_Call): Issue warning and flag subprogram
as not always inlined in GNATprove mode, when called in an
assertion context.
2014-07-30 Vincent Celier <celier@adacore.com>
* debug.adb: Minor comment update.

7
gcc/ada/debug.adb
View file

@ -80,7 +80,7 @@ package body Debug is
-- dN No file name information in exception messages
-- dO Output immediate error messages
-- dP Do not check for controlled objects in preelaborable packages
-- dQ Enable inlining of bodies-without-decl in GNATprove mode
-- dQ
-- dR Bypass check for correct version of s-rpc
-- dS Never convert numbers to machine numbers in Sem_Eval
-- dT Convert to machine numbers only for constant declarations
@ -438,11 +438,6 @@ package body Debug is
-- in preelaborable packages, but this restriction is a huge pain,
-- especially in the predefined library units.
-- dQ Enable inlining of bodies-without-decl in GNATprove mode. A decl is
-- created by the frontend so that the usual frontend inlining
-- mechanism can be used for formal verification. Under a debug flag
-- until fully reliable.
-- dR Bypass the check for a proper version of s-rpc being present
-- to use the -gnatz? switch. This allows debugging of the use
-- of stubs generation without needing to have GLADE (or some

5
gcc/ada/exp_prag.adb
View file

@ -440,6 +440,9 @@ package body Exp_Prag is
-- Generate a temporary to capture the value of the prefix:
-- Temp : <Pref type>;
-- Place that temporary at the beginning of declarations, to
-- prevent anomolies in the GNATprove flow analysis pass in
-- the precondition procedure that follows.
Decl :=
Make_Object_Declaration (Loc,
@ -448,7 +451,7 @@ package body Exp_Prag is
New_Occurrence_Of (Etype (Pref), Loc));
Set_No_Initialization (Decl);
Append_To (Decls, Decl);
Prepend_To (Decls, Decl);
-- Evaluate the prefix, generate:
-- Temp := <Pref>;

2
gcc/ada/gnat_rm.texi
View file

@ -7215,7 +7215,7 @@ The meaning of a test case is that there is at least one context where
that context, then @code{Ensures} holds when the subprogram returns.
Mode @code{Nominal} indicates that the input context should also satisfy the
precondition of the subprogram, and the output context should also satisfy its
postcondition. More @code{Robustness} indicates that the precondition and
postcondition. Mode @code{Robustness} indicates that the precondition and
postcondition of the subprogram should be ignored for this test case.
@node Pragma Thread_Local_Storage

19
gcc/ada/inline.adb
View file

@ -1692,13 +1692,14 @@ package body Inline is
elsif Is_Generic_Instance (Spec_Id) then
return False;
-- Only inline subprograms whose body is marked SPARK_Mode On. Other
-- subprogram bodies should not be analyzed.
-- Only inline subprograms whose spec is marked SPARK_Mode On. For
-- the subprogram body, a similar check is performed after the body
-- is analyzed, as this is where a pragma SPARK_Mode might be inserted.
elsif Present (Body_Id)
and then (No (SPARK_Pragma (Body_Id))
or else
Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) /= On)
elsif Present (Spec_Id)
and then (No (SPARK_Pragma (Spec_Id))
or else
Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) /= On)
then
return False;
@ -1708,6 +1709,12 @@ package body Inline is
elsif Instantiation_Location (Sloc (Id)) /= No_Location then
return False;
-- Predicate functions are treated specially by GNATprove. Do not inline
-- them.
elsif Is_Predicate_Function (Id) then
return False;
-- Otherwise, this is a subprogram declared inside the private part of a
-- package, or inside a package body, or locally in a subprogram, and it
-- does not have any contract. Inline it.

2
gcc/ada/sem_ch13.adb
View file

@ -1497,7 +1497,7 @@ package body Sem_Ch13 is
-- Start of processing for Analyze_One_Aspect
begin
-- Skip aspect if already analyzed (not clear if this is needed)
-- Skip aspect if already analyzed, to avoid looping in some cases
if Analyzed (Aspect) then
goto Continue;

42
gcc/ada/sem_ch6.adb
View file

@ -3034,10 +3034,6 @@ package body Sem_Ch6 is
if No (Spec_Id)
and then GNATprove_Mode
-- Under a debug flag until remaining issues are fixed
and then Debug_Flag_QQ
-- Inlining does not apply during pre-analysis of code
and then Full_Analysis
@ -3077,13 +3073,51 @@ package body Sem_Ch6 is
New_Decl : constant Node_Id :=
Make_Subprogram_Declaration (Loc,
Copy_Separate_Tree (Specification (N)));
SPARK_Mode_Aspect : Node_Id;
Aspects : List_Id;
Prag, Aspect : Node_Id;
begin
Insert_Before (N, New_Decl);
Move_Aspects (From => N, To => New_Decl);
-- Mark the newly moved aspects as not analyzed, so that
-- their effect on New_Decl is properly analyzed.
Aspect := First (Aspect_Specifications (New_Decl));
while Present (Aspect) loop
Set_Analyzed (Aspect, False);
Next (Aspect);
end loop;
Analyze (New_Decl);
-- The analysis of the generated subprogram declaration
-- may have introduced pragmas, which need to be
-- analyzed.
Prag := Next (New_Decl);
while Prag /= N loop
Analyze (Prag);
Next (Prag);
end loop;
Spec_Id := Defining_Entity (New_Decl);
-- If aspect SPARK_Mode was specified on the body, it
-- needs to be repeated on the generated decl and the
-- body. Since the original aspect was moved to the
-- generated decl, copy it for the body.
if Has_Aspect (Spec_Id, Aspect_SPARK_Mode) then
SPARK_Mode_Aspect :=
New_Copy (Find_Aspect (Spec_Id, Aspect_SPARK_Mode));
Set_Analyzed (SPARK_Mode_Aspect, False);
Aspects := New_List;
Append (SPARK_Mode_Aspect, Aspects);
Set_Aspect_Specifications (N, Aspects);
end if;
Set_Specification (N, Body_Spec);
Body_Id := Analyze_Subprogram_Specification (Body_Spec);
Set_Corresponding_Spec (N, Spec_Id);

10
gcc/ada/sem_prag.adb
View file

@ -19830,11 +19830,6 @@ package body Sem_Prag is
raise Pragma_Exit;
end if;
-- Skip internally generated code
elsif not Comes_From_Source (Stmt) then
null;
elsif Nkind (Stmt) in N_Generic_Declaration then
Error_Pragma
("incorrect placement of pragma% on a generic");
@ -19869,6 +19864,11 @@ package body Sem_Prag is
Set_SPARK_Pragma_Inherited (Spec_Id, False);
return;
-- Skip internally generated code
elsif not Comes_From_Source (Stmt) then
null;
-- The pragma does not apply to a legal construct, issue an
-- error and stop the analysis.

52
gcc/ada/sem_res.adb
View file

@ -6210,7 +6210,6 @@ package body Sem_Res is
if GNATprove_Mode
and then Is_Overloadable (Nam)
and then SPARK_Mode = On
and then Full_Analysis
then
-- Retrieve the body to inline from the ultimate alias of Nam, if
-- there is one, otherwise calls that should be inlined end up not
@ -6220,23 +6219,54 @@ package body Sem_Res is
Nam_Alias : constant Entity_Id := Ultimate_Alias (Nam);
Decl : constant Node_Id := Unit_Declaration_Node (Nam_Alias);
begin
if Nkind (Decl) = N_Subprogram_Declaration
and then Can_Be_Inlined_In_GNATprove_Mode (Nam_Alias, Empty)
and then No (Corresponding_Body (Decl))
-- If the subprogram is not eligible for inlining in GNATprove
-- mode, do nothing.
if not Can_Be_Inlined_In_GNATprove_Mode (Nam_Alias, Empty)
or else Nkind (Decl) /= N_Subprogram_Declaration
or else not Is_Inlined_Always (Nam_Alias)
then
Error_Msg_NE
("?cannot inline call to & (body not seen yet)", N, Nam);
null;
-- Calls cannot be inlined inside assertions, as GNATprove treats
-- assertions as logic expressions.
elsif In_Assertion_Expr /= 0 then
Error_Msg_NE ("?cannot inline call to &", N, Nam);
Error_Msg_N ("\call appears in assertion expression", N);
Set_Is_Inlined_Always (Nam_Alias, False);
elsif Nkind (Decl) = N_Subprogram_Declaration
and then Present (Body_To_Inline (Decl))
and then Is_Inlined (Nam_Alias)
then
if Is_Potentially_Unevaluated (N) then
-- Inlining should not be performed during pre-analysis
elsif Full_Analysis then
-- With the one-pass inlining technique, a call cannot be
-- inlined if the corresponding body has not been seen yet.
if No (Corresponding_Body (Decl)) then
Error_Msg_NE
("?cannot inline call to & (body not seen yet)", N, Nam);
Set_Is_Inlined_Always (Nam_Alias, False);
-- Nothing to do if there is no body to inline, indicating that
-- the subprogram is not suitable for inlining in GNATprove
-- mode.
elsif No (Body_To_Inline (Decl)) then
null;
-- 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 ("?cannot inline call to &", N, Nam);
Error_Msg_N
("\call appears in potentially unevaluated context", N);
Set_Is_Inlined_Always (Nam_Alias, False);
-- Otherwise, inline the call
else
Expand_Inlined_Call (N, Nam_Alias, Nam);
end if;