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

[multiple changes] 

2016-04-18  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_res.adb (Is_Protected_Operation_Call):
	Add guards to account for a non-decorated selected component.

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

	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Improve
	implementation of Body_Has_SPARK_Mode_On.
	* sem_prag.adb, sem_prag.ads (Get_SPARK_Mode_From_Annotation):
	New function replacing previous Get_SPARK_Mode_From_Pragma, that
	deals also with aspects.
	(Get_SPARK_Mode_Type): Make function internal again.
	* inline.adb, sem_ch7.adb, sem_util.adb: Use new
	Get_SPARK_Mode_From_Annotation.

From-SVN: r235116
This commit is contained in:
Arnaud Charlet 2016-04-18 12:24:03 +02:00
parent 4179af278f
commit 933aa0ac81
8 changed files with 84 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
gcc/ada/ChangeLog
View File

@ -1,3 +1,19 @@
2016-04-18 Hristian Kirtchev <kirtchev@adacore.com>
* sem_res.adb (Is_Protected_Operation_Call):
Add guards to account for a non-decorated selected component.
2016-04-18 Yannick Moy <moy@adacore.com>
* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Improve
implementation of Body_Has_SPARK_Mode_On.
* sem_prag.adb, sem_prag.ads (Get_SPARK_Mode_From_Annotation):
New function replacing previous Get_SPARK_Mode_From_Pragma, that
deals also with aspects.
(Get_SPARK_Mode_Type): Make function internal again.
* inline.adb, sem_ch7.adb, sem_util.adb: Use new
Get_SPARK_Mode_From_Annotation.
2016-04-18 Hristian Kirtchev <kirtchev@adacore.com>
* contracts.adb (Analyze_Object_Contract): Update references to

3
gcc/ada/inline.adb
View File

@ -1553,7 +1553,8 @@ package body Inline is
elsif Present (Spec_Id)
and then
(No (SPARK_Pragma (Spec_Id))
or else Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) /= On)
or else
Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Spec_Id)) /= On)
then
return False;

32
gcc/ada/sem_ch6.adb
View File

@ -2292,11 +2292,7 @@ package body Sem_Ch6 is
Item := First (Aspect_Specifications (N));
while Present (Item) loop
if Get_Aspect_Id (Item) = Aspect_SPARK_Mode then
return No (Expression (Item))
or else
(Nkind (Expression (Item)) = N_Identifier
and then
Get_SPARK_Mode_Type (Chars (Expression (Item))) = On);
return Get_SPARK_Mode_From_Annotation (Item) = On;
end if;
Next (Item);
@ -2308,18 +2304,28 @@ package body Sem_Ch6 is
if Present (Decls) then
Item := First (Decls);
while Present (Item) loop
if Nkind (Item) = N_Pragma
and then Get_Pragma_Id (Item) = Pragma_SPARK_Mode
then
return Get_SPARK_Mode_From_Pragma (Item) = On;
-- Pragmas that apply to a subprogram body are usually grouped
-- together. Look for a potential pragma SPARK_Mode among them.
if Nkind (Item) = N_Pragma then
if Get_Pragma_Id (Item) = Pragma_SPARK_Mode then
return Get_SPARK_Mode_From_Annotation (Item) = On;
end if;
-- Otherwise the first non-pragma declarative item terminates
-- the region where pragma SPARK_Mode may appear.
else
exit;
end if;
Next (Item);
end loop;
end if;
-- Applicable SPARK_Mode is inherited from the enclosing subprogram
-- or package.
-- Otherwise, the applicable SPARK_Mode is inherited from the
-- enclosing subprogram or package.
return SPARK_Mode = On;
end Body_Has_SPARK_Mode_On;
@ -3849,9 +3855,9 @@ package body Sem_Ch6 is
if Present (Spec_Id) and then Present (SPARK_Pragma (Body_Id)) then
if Present (SPARK_Pragma (Spec_Id)) then
if Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) = Off
if Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Spec_Id)) = Off
and then
Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) = On
Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Body_Id)) = On
then
Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
Error_Msg_N ("incorrect application of SPARK_Mode#", N);

7
gcc/ada/sem_ch7.adb
View File

@ -777,9 +777,10 @@ package body Sem_Ch7 is
if Present (SPARK_Pragma (Body_Id)) then
if Present (SPARK_Aux_Pragma (Spec_Id)) then
if Get_SPARK_Mode_From_Pragma (SPARK_Aux_Pragma (Spec_Id)) = Off
and then
Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) = On
if Get_SPARK_Mode_From_Annotation (SPARK_Aux_Pragma (Spec_Id)) =
Off
and then
Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Body_Id)) = On
then
Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
Error_Msg_N ("incorrect application of SPARK_Mode#", N);

54
gcc/ada/sem_prag.adb
View File

@ -235,6 +235,11 @@ package body Sem_Prag is
-- original one, following the renaming chain) is returned. Otherwise the
-- entity is returned unchanged. Should be in Einfo???
function Get_SPARK_Mode_Type (N : Name_Id) return SPARK_Mode_Type;
-- Subsidiary to the analysis of pragma SPARK_Mode as well as subprogram
-- Get_SPARK_Mode_From_Annotation. Convert a name into a corresponding
-- value of type SPARK_Mode_Type.
function Has_Extra_Parentheses (Clause : Node_Id) return Boolean;
-- Subsidiary to the analysis of pragmas Depends and Refined_Depends.
-- Determine whether dependency clause Clause is surrounded by extra
@ -20338,8 +20343,8 @@ package body Sem_Prag is
-- Issue an error if the new mode is less restrictive than
-- that of the context.
if Get_SPARK_Mode_From_Pragma (Context_Pragma) = Off
and then Get_SPARK_Mode_From_Pragma (N) = On
if Get_SPARK_Mode_From_Annotation (Context_Pragma) = Off
and then Get_SPARK_Mode_From_Annotation (N) = On
then
Error_Msg_N
("cannot change SPARK_Mode from Off to On", Err_N);
@ -20376,8 +20381,8 @@ package body Sem_Prag is
-- Issue an error if the new mode is less restrictive
-- than that of the initial declaration.
if Get_SPARK_Mode_From_Pragma (Entity_Pragma) = Off
and then Get_SPARK_Mode_From_Pragma (N) = On
if Get_SPARK_Mode_From_Annotation (Entity_Pragma) = Off
and then Get_SPARK_Mode_From_Annotation (N) = On
then
Error_Msg_N ("incorrect use of SPARK_Mode", Err_N);
Error_Msg_Sloc := Sloc (Entity_Pragma);
@ -27553,30 +27558,45 @@ package body Sem_Prag is
end if;
end Get_SPARK_Mode_Type;
--------------------------------
-- Get_SPARK_Mode_From_Pragma --
--------------------------------
------------------------------------
-- Get_SPARK_Mode_From_Annotation --
------------------------------------
function Get_SPARK_Mode_From_Pragma (N : Node_Id) return SPARK_Mode_Type is
Args : List_Id;
function Get_SPARK_Mode_From_Annotation
(N : Node_Id) return SPARK_Mode_Type
is
Mode : Node_Id;
begin
pragma Assert (Nkind (N) = N_Pragma);
Args := Pragma_Argument_Associations (N);
if Nkind (N) = N_Aspect_Specification then
Mode := Expression (N);
-- Extract the mode from the argument list
if Present (Args) then
else pragma Assert (Nkind (N) = N_Pragma);
Mode := First (Pragma_Argument_Associations (N));
return Get_SPARK_Mode_Type (Chars (Get_Pragma_Arg (Mode)));
-- If SPARK_Mode pragma has no argument, default is ON
if Present (Mode) then
Mode := Get_Pragma_Arg (Mode);
end if;
end if;
-- Aspect or pragma SPARK_Mode specifies an explicit mode
if Present (Mode) then
if Nkind (Mode) = N_Identifier then
return Get_SPARK_Mode_Type (Chars (Mode));
-- In case of a malformed aspect or pragma, return the default None
else
return None;
end if;
-- Otherwise the lack of an expression defaults SPARK_Mode to On
else
return On;
end if;
end Get_SPARK_Mode_From_Pragma;
end Get_SPARK_Mode_From_Annotation;
---------------------------
-- Has_Extra_Parentheses --

10
gcc/ada/sem_prag.ads
View File

@ -397,13 +397,9 @@ package Sem_Prag is
-- Context denotes the entity of the function, package or procedure where
-- Prag resides.
function Get_SPARK_Mode_From_Pragma (N : Node_Id) return SPARK_Mode_Type;
-- Given a pragma SPARK_Mode node, return corresponding mode id
function Get_SPARK_Mode_Type (N : Name_Id) return SPARK_Mode_Type;
-- Subsidiary to the analysis of pragma SPARK_Mode as well as subprogram
-- Get_SPARK_Mode_From_Pragma. Convert a name into a corresponding value
-- of type SPARK_Mode_Type.
function Get_SPARK_Mode_From_Annotation
(N : Node_Id) return SPARK_Mode_Type;
-- Given an aspect or pragma SPARK_Mode node, return corresponding mode id
procedure Initialize;
-- Initializes data structures used for pragma processing. Must be called

2
gcc/ada/sem_res.adb
View File

@ -6895,8 +6895,10 @@ package body Sem_Res is
return
Pref = Obj_Ref
and then Present (Etype (Pref))
and then Is_Protected_Type (Etype (Pref))
and then Is_Entity_Name (Subp)
and then Present (Entity (Subp))
and then Ekind_In (Entity (Subp), E_Entry,
E_Entry_Family,
E_Function,

2
gcc/ada/sem_util.adb
View File

@ -18645,7 +18645,7 @@ package body Sem_Util is
null;
elsif Present (SPARK_Pragma (Context)) then
SPARK_Mode := Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Context));
SPARK_Mode := Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Context));
end if;
end Save_SPARK_Mode_And_Set;