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

[multiple changes]

Browse source 
2014-07-30  Robert Dewar  <dewar@adacore.com>

	* sem_ch4.adb (Analyze_If_Expression): Resolve condition before
	analyzing branches.
	* sem_eval.adb (Out_Of_Range): Check for statically unevaluated
	expression case.

2014-07-30  Robert Dewar  <dewar@adacore.com>

	* sem_ch13.adb (Analyze_Aspect, predicate cases): Diagnose use
	of predicate aspect on entity other than a type.

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

	* sem_ch6.adb (Body_Has_Contract): New predicate to determine
	when a subprogram body without a previous spec cannot be inlined
	in GNATprove mode, because it includes aspects or pragmas that
	generate a SPARK contract clause.
	* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): A subprogram
	instance cannot be inlined.

From-SVN: r213247
This commit is contained in:
Arnaud Charlet 2014-07-30 12:47:17 +02:00
parent cc6f5d75ed
commit ac072cb2f4
6 changed files with 128 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
gcc/ada/ChangeLog
View file

@ -1,3 +1,24 @@
2014-07-30 Robert Dewar <dewar@adacore.com>
* sem_ch4.adb (Analyze_If_Expression): Resolve condition before
analyzing branches.
* sem_eval.adb (Out_Of_Range): Check for statically unevaluated
expression case.
2014-07-30 Robert Dewar <dewar@adacore.com>
* sem_ch13.adb (Analyze_Aspect, predicate cases): Diagnose use
of predicate aspect on entity other than a type.
2014-07-30 Ed Schonberg <schonberg@adacore.com>
* sem_ch6.adb (Body_Has_Contract): New predicate to determine
when a subprogram body without a previous spec cannot be inlined
in GNATprove mode, because it includes aspects or pragmas that
generate a SPARK contract clause.
* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): A subprogram
instance cannot be inlined.
2014-07-30 Robert Dewar <dewar@adacore.com>
* debug.adb: Document that d7 suppresses compilation time output.

10
gcc/ada/inline.adb
View file

@ -1490,13 +1490,12 @@ package body Inline is
function Has_Some_Contract (Id : Entity_Id) return Boolean is
Items : constant Node_Id := Contract (Id);
begin
return Present (Items)
and then (Present (Pre_Post_Conditions (Items))
or else
Present (Contract_Test_Cases (Items))
or else
Present (Classifications (Items)));
or else Present (Contract_Test_Cases (Items))
or else Present (Classifications (Items)));
end Has_Some_Contract;
--------------------------
@ -1589,6 +1588,9 @@ package body Inline is
then
return False;
elsif Is_Generic_Instance (Spec_Id) then
return False;
-- Only inline subprograms whose body is marked SPARK_Mode On
elsif No (SPARK_Pragma (Body_Id))

9
gcc/ada/sem_ch13.adb
View file

@ -1778,6 +1778,15 @@ package body Sem_Ch13 is
Aspect_Predicate |
Aspect_Static_Predicate =>
-- These aspects apply only to subtypes
if not Is_Type (E) then
Error_Msg_N
("predicate can only be specified for a subtype",
Aspect);
goto Continue;
end if;
-- Construct the pragma (always a pragma Predicate, with
-- flags recording whether it is static/dynamic). We also
-- set flags recording this in the type itself.

11
gcc/ada/sem_ch4.adb
View file

@ -2046,7 +2046,18 @@ package body Sem_Ch4 is
Check_Compiler_Unit ("if expression", N);
end if;
-- Analyze and resolve the condition. We need to resolve this now so
-- that it gets folded to True/False if possible, before we analyze
-- the THEN/ELSE branches, because when analyzing these branches, we
-- may call Is_Statically_Unevaluated, which expects the condition of
-- an enclosing IF to have been analyze/resolved/evaluated.
Analyze_Expression (Condition);
Resolve (Condition, Any_Boolean);
-- Analyze THEN expression and (if present) ELSE expression. For those
-- we delay resolution in the normal manner, because of overloading etc.
Analyze_Expression (Then_Expr);
if Present (Else_Expr) then

69
gcc/ada/sem_ch6.adb
View file

@ -2167,6 +2167,10 @@ package body Sem_Ch6 is
-- Analyze the aspect specifications of a subprogram body [stub]. It is
-- assumed that N has aspects.
function Body_Has_Contract return Boolean;
-- Check whether unanalyzed body has an aspect or pragma that may
-- generate a SPARK contrac.
procedure Check_Anonymous_Return;
-- Ada 2005: if a function returns an access type that denotes a task,
-- or a type that contains tasks, we must create a master entity for
@ -2339,6 +2343,68 @@ package body Sem_Ch6 is
end if;
end Analyze_Aspects_On_Body_Or_Stub;
-----------------------
-- Body_Has_Contract --
-----------------------
function Body_Has_Contract return Boolean is
Decls : constant List_Id := Declarations (N);
A_Spec : Node_Id;
A : Aspect_Id;
Decl : Node_Id;
P_Id : Pragma_Id;
begin
-- Check for unanalyzed aspects in the body that will
-- generate a contract.
if Present (Aspect_Specifications (N)) then
A_Spec := First (Aspect_Specifications (N));
while Present (A_Spec) loop
A := Get_Aspect_Id (Chars (Identifier (A_Spec)));
if A = Aspect_Contract_Cases
or else A = Aspect_Depends
or else A = Aspect_Global
or else A = Aspect_Pre
or else A = Aspect_Precondition
or else A = Aspect_Post
or else A = Aspect_Postcondition
then
return True;
end if;
Next (A_Spec);
end loop;
end if;
-- Check for pragmas that may generate a contract.
if Present (Decls) then
Decl := First (Decls);
while Present (Decl) loop
if Nkind (Decl) = N_Pragma then
P_Id := Get_Pragma_Id (Pragma_Name (Decl));
if P_Id = Pragma_Contract_Cases
or else P_Id = Pragma_Depends
or else P_Id = Pragma_Global
or else P_Id = Pragma_Pre
or else P_Id = Pragma_Precondition
or else P_Id = Pragma_Post
or else P_Id = Pragma_Postcondition
then
return True;
end if;
end if;
Next (Decl);
end loop;
end if;
return False;
end Body_Has_Contract;
----------------------------
-- Check_Anonymous_Return --
----------------------------
@ -2969,6 +3035,7 @@ package body Sem_Ch6 is
and then Full_Analysis
and then Comes_From_Source (Body_Id)
and then Is_List_Member (N)
and then not Body_Has_Contract
then
declare
Body_Spec : constant Node_Id :=
@ -3410,6 +3477,7 @@ package body Sem_Ch6 is
and then
Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Declaration
and then Can_Be_Inlined_In_GNATprove_Mode (Spec_Id, Body_Id)
and then not Body_Has_Contract
then
Build_Body_To_Inline (N, Spec_Id);
end if;
@ -3437,6 +3505,7 @@ package body Sem_Ch6 is
and then Present (Spec_Id)
and then Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Declaration
and then Can_Be_Inlined_In_GNATprove_Mode (Spec_Id, Body_Id)
and then not Body_Has_Contract
then
Check_And_Build_Body_To_Inline (N, Spec_Id, Body_Id);
end if;

15
gcc/ada/sem_eval.adb
View file

@ -5280,15 +5280,22 @@ package body Sem_Eval is
-- If we have the static expression case, then this is an illegality
-- in Ada 95 mode, except that in an instance, we never generate an
-- error (if the error is legitimate, it was already diagnosed in the
-- template). The expression to compute the length of a packed array is
-- attached to the array type itself, and deserves a separate message.
-- template).
if Is_Static_Expression (N)
and then not In_Instance
and then not In_Inlined_Body
and then Ada_Version >= Ada_95
then
if Nkind (Parent (N)) = N_Defining_Identifier
-- No message if we are staticallly unevaluated
if Is_Statically_Unevaluated (N) then
null;
-- The expression to compute the length of a packed array is attached
-- to the array type itself, and deserves a separate message.
elsif Nkind (Parent (N)) = N_Defining_Identifier
and then Is_Array_Type (Parent (N))
and then Present (Packed_Array_Impl_Type (Parent (N)))
and then Present (First_Rep_Item (Parent (N)))
@ -5298,6 +5305,8 @@ package body Sem_Eval is
First_Rep_Item (Parent (N)));
Rewrite (N, Make_Integer_Literal (Sloc (N), Uint_1));
-- All cases except the special array case
else
Apply_Compile_Time_Constraint_Error
(N, "value not in range of}", CE_Range_Check_Failed);