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

[multiple changes]

Browse Source 
2014-01-23  Robert Dewar  <dewar@adacore.com>

	* gnatlink.adb (Gnatlink): Fix problem of generating bad name
	msg on VMS.

2014-01-23  Bob Duff  <duff@adacore.com>

	* g-dynhta.ads: Minor comment fix.

2014-01-23  Yannick Moy  <moy@adacore.com>

	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Inherit SPARK_Mode
	from spec on body only when not already inherited on spec. Set
	SPARK_Mode from context on body without previous spec.	*
	* sem_prag.adb (Analyze_Pragma): Check placement of pragma on
	library-level entities.  Correct retrieval of entity from
	declaration, for cases where the declaration is not a unit.
	* sem_ch12.adb (Instantiate_Object): Avoid
	calling Is_Volatile_Object on an empty node.

From-SVN: r206987
This commit is contained in:
Arnaud Charlet 2014-01-23 17:54:50 +01:00
parent 545d3e65ad
commit e949ee225e
6 changed files with 82 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
gcc/ada/ChangeLog
View File

@ -1,3 +1,23 @@
2014-01-23 Robert Dewar <dewar@adacore.com>
* gnatlink.adb (Gnatlink): Fix problem of generating bad name
msg on VMS.
2014-01-23 Bob Duff <duff@adacore.com>
* g-dynhta.ads: Minor comment fix.
2014-01-23 Yannick Moy <moy@adacore.com>
* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Inherit SPARK_Mode
from spec on body only when not already inherited on spec. Set
SPARK_Mode from context on body without previous spec. *
* sem_prag.adb (Analyze_Pragma): Check placement of pragma on
library-level entities. Correct retrieval of entity from
declaration, for cases where the declaration is not a unit.
* sem_ch12.adb (Instantiate_Object): Avoid
calling Is_Volatile_Object on an empty node.
2014-01-23 Robert Dewar <dewar@adacore.com>
* gnatlink.adb (Gnatlink): Check for suspicious executable file

2
gcc/ada/g-dynhta.ads
View File

@ -56,7 +56,7 @@ package GNAT.Dynamic_HTables is
-- A low-level Hash-Table abstraction, not as easy to instantiate as
-- Simple_HTable. This mirrors the interface of GNAT.HTable.Static_HTable,
-- but does require dynamic allocation (since we allow multiple instances
-- of the table. The model is that each Element contains its own Key that
-- of the table). The model is that each Element contains its own Key that
-- can be retrieved by Get_Key. Furthermore, Element provides a link that
-- can be used by the HTable for linking elements with same hash codes:

7
gcc/ada/gnatlink.adb
View File

@ -1101,9 +1101,9 @@ procedure Gnatlink is
-- The following test needs comments, why is it VMS specific.
-- The above comment looks out of date ???
elsif not (OpenVMS_On_Target
and then
Is_Option_Present (Next_Line (Nfirst .. Nlast)))
elsif not
(OpenVMS_On_Target
and then Is_Option_Present (Next_Line (Nfirst .. Nlast)))
then
if Nlast > Nfirst + 2 and then
Next_Line (Nfirst .. Nfirst + 1) = "-L"
@ -1832,6 +1832,7 @@ begin
if FN'Length > 5
and then FN (FN'Last - 3 .. FN'Last) = ".exe"
and then not OpenVMS_On_Target
then
Check_File_Name ("install");
Check_File_Name ("setup");

5
gcc/ada/sem_ch12.adb
View File

@ -9844,7 +9844,10 @@ package body Sem_Ch12 is
-- The following check is only relevant when SPARK_Mode is on as it is
-- not a standard Ada legality rule.
if SPARK_Mode = On and then Is_Volatile_Object (Actual) then
if SPARK_Mode = On
and then Present (Actual)
and then Is_Volatile_Object (Actual)
then
Error_Msg_N
("volatile object cannot act as actual in generic instantiation "
& "(SPARK RM 7.1.3(4))", Actual);

10
gcc/ada/sem_ch6.adb
View File

@ -2997,7 +2997,9 @@ package body Sem_Ch6 is
-- Set SPARK_Mode from spec if spec had a SPARK_Mode pragma
if Present (SPARK_Pragma (Spec_Id)) then
if Present (SPARK_Pragma (Spec_Id))
and then not SPARK_Pragma_Inherited (Spec_Id)
then
SPARK_Mode_Pragma := SPARK_Pragma (Spec_Id);
SPARK_Mode := Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragma);
Set_SPARK_Pragma (Body_Id, SPARK_Pragma (Spec_Id));
@ -3055,6 +3057,12 @@ package body Sem_Ch6 is
Generate_Reference
(Body_Id, Body_Id, 'b', Set_Ref => False, Force => True);
Install_Formals (Body_Id);
-- Set SPARK_Mode from context
Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (Body_Id, True);
Push_Scope (Body_Id);
end if;

49
gcc/ada/sem_prag.adb
View File

@ -18485,6 +18485,9 @@ package body Sem_Prag is
-- anything. But if the old mode is OFF, then the only allowed
-- new mode is also OFF.
procedure Check_Library_Level_Entity (E : Entity_Id);
-- Verify that pragma is applied to library-level entity E
function Get_SPARK_Mode_Name (Id : SPARK_Mode_Type) return Name_Id;
-- Convert a value of type SPARK_Mode_Type to corresponding name
@ -18513,6 +18516,34 @@ package body Sem_Prag is
end if;
end Check_Pragma_Conformance;
--------------------------------
-- Check_Library_Level_Entity --
--------------------------------
procedure Check_Library_Level_Entity (E : Entity_Id) is
MsgF : String := "incorrect placement of pragma%";
begin
if not Is_Library_Level_Entity (E) then
Error_Msg_Name_1 := Pname;
Fix_Error (MsgF);
Error_Msg_N (MsgF, N);
if Ekind_In (E, E_Generic_Package,
E_Package,
E_Package_Body)
then
Error_Msg_NE
("\& is not a library-level package", N, E);
else
Error_Msg_NE
("\& is not a library-level subprogram", N, E);
end if;
raise Pragma_Exit;
end if;
end Check_Library_Level_Entity;
-------------------------
-- Get_SPARK_Mode_Name --
-------------------------
@ -18614,7 +18645,8 @@ package body Sem_Prag is
elsif Nkind_In (Stmt, N_Generic_Package_Declaration,
N_Package_Declaration)
then
Spec_Id := Defining_Unit_Name (Specification (Stmt));
Spec_Id := Defining_Entity (Stmt);
Check_Library_Level_Entity (Spec_Id);
Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
Set_SPARK_Pragma (Spec_Id, N);
@ -18628,7 +18660,8 @@ package body Sem_Prag is
elsif Nkind_In (Stmt, N_Generic_Subprogram_Declaration,
N_Subprogram_Declaration)
then
Spec_Id := Defining_Unit_Name (Specification (Stmt));
Spec_Id := Defining_Entity (Stmt);
Check_Library_Level_Entity (Spec_Id);
Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
Set_SPARK_Pragma (Spec_Id, N);
@ -18679,11 +18712,12 @@ package body Sem_Prag is
-- pragma SPARK_Mode;
if Nkind (Context) = N_Package_Specification then
Spec_Id := Defining_Unit_Name (Context);
Spec_Id := Defining_Entity (Context);
-- Pragma applies to private part
if List_Containing (N) = Private_Declarations (Context) then
Check_Library_Level_Entity (Spec_Id);
Check_Pragma_Conformance (SPARK_Aux_Pragma (Spec_Id));
SPARK_Mode_Pragma := N;
SPARK_Mode := Mode_Id;
@ -18694,6 +18728,7 @@ package body Sem_Prag is
-- Pragma applies to public part
else
Check_Library_Level_Entity (Spec_Id);
Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
SPARK_Mode_Pragma := N;
SPARK_Mode := Mode_Id;
@ -18711,7 +18746,8 @@ package body Sem_Prag is
elsif Nkind_In (Context, N_Function_Specification,
N_Procedure_Specification)
then
Spec_Id := Defining_Unit_Name (Context);
Spec_Id := Defining_Entity (Context);
Check_Library_Level_Entity (Spec_Id);
Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
Set_SPARK_Pragma (Spec_Id, N);
@ -18725,6 +18761,7 @@ package body Sem_Prag is
elsif Nkind (Context) = N_Package_Body then
Spec_Id := Corresponding_Spec (Context);
Body_Id := Defining_Entity (Context);
Check_Library_Level_Entity (Body_Id);
Check_Pragma_Conformance (SPARK_Pragma (Body_Id));
SPARK_Mode_Pragma := N;
SPARK_Mode := Mode_Id;
@ -18743,6 +18780,7 @@ package body Sem_Prag is
Spec_Id := Corresponding_Spec (Context);
Context := Specification (Context);
Body_Id := Defining_Entity (Context);
Check_Library_Level_Entity (Body_Id);
Check_Pragma_Conformance (SPARK_Pragma (Body_Id));
SPARK_Mode_Pragma := N;
SPARK_Mode := Mode_Id;
@ -18761,7 +18799,8 @@ package body Sem_Prag is
then
Context := Parent (Context);
Spec_Id := Corresponding_Spec (Context);
Body_Id := Defining_Unit_Name (Context);
Body_Id := Defining_Entity (Context);
Check_Library_Level_Entity (Body_Id);
Check_Pragma_Conformance (SPARK_Aux_Pragma (Body_Id));
SPARK_Mode_Pragma := N;
SPARK_Mode := Mode_Id;