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

[multiple changes] 

2014-11-07  Hristian Kirtchev  <kirtchev@adacore.com>

	* freeze.adb (Freeze_Entity): Issue an error regardless of the
	SPARK_Mode when a ghost type is effectively volatile.
	* sem_ch3.adb (Analyze_Object_Contract): Decouple the checks
	related to Ghost from SPARK_Mode.
	* sem_res.adb (Check_Ghost_Policy): Issue an error regardless
	of the SPARK_Mode when the Ghost policies do not match.
	* sem_util.adb (Check_Ghost_Completion): Issue an error regardless
	of the SPARK_Mode when the Ghost policies do not match.

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

	* sem_ch5.adb (Analyze_Iterator_Specification): return if name
	in iterator does not have any usable aspect for iteration.

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

	* sem_ch6.adb (Analyze_Null_Procedure): Reject a null procedure
	that there is a previous null procedure in scope with a matching
	profile.

2014-11-07  Hristian Kirtchev  <kirtchev@adacore.com>

	* atree.adb (Copy_Separate_Tree): Copy the aspect specifications.
	* inline.adb (Has_Some_Contract): Do the check only when the
	related entity has been analyzed.

From-SVN: r217224
This commit is contained in:
Arnaud Charlet 2014-11-07 14:47:31 +01:00
parent e8de1a820f
commit a98480ddbb
9 changed files with 117 additions and 77 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
gcc/ada/ChangeLog
View File

@ -1,3 +1,31 @@
2014-11-07 Hristian Kirtchev <kirtchev@adacore.com>
* freeze.adb (Freeze_Entity): Issue an error regardless of the
SPARK_Mode when a ghost type is effectively volatile.
* sem_ch3.adb (Analyze_Object_Contract): Decouple the checks
related to Ghost from SPARK_Mode.
* sem_res.adb (Check_Ghost_Policy): Issue an error regardless
of the SPARK_Mode when the Ghost policies do not match.
* sem_util.adb (Check_Ghost_Completion): Issue an error regardless
of the SPARK_Mode when the Ghost policies do not match.
2014-11-07 Ed Schonberg <schonberg@adacore.com>
* sem_ch5.adb (Analyze_Iterator_Specification): return if name
in iterator does not have any usable aspect for iteration.
2014-11-07 Ed Schonberg <schonberg@adacore.com>
* sem_ch6.adb (Analyze_Null_Procedure): Reject a null procedure
that there is a previous null procedure in scope with a matching
profile.
2014-11-07 Hristian Kirtchev <kirtchev@adacore.com>
* atree.adb (Copy_Separate_Tree): Copy the aspect specifications.
* inline.adb (Has_Some_Contract): Do the check only when the
related entity has been analyzed.
2014-11-07 Ed Schonberg <schonberg@adacore.com>
* exp_fixd.adb (Expand_Multiply_Fixed_By_Fixed_Giving_Integer):

10
gcc/ada/atree.adb
View File

@ -892,6 +892,16 @@ package body Atree is
Set_Field4 (New_Id, Possible_Copy (Field4 (New_Id)));
Set_Field5 (New_Id, Possible_Copy (Field5 (New_Id)));
-- Explicitly copy the aspect specifications as those do not reside
-- in a node field.
if Permits_Aspect_Specifications (Source)
and then Has_Aspects (Source)
then
Set_Aspect_Specifications
(New_Id, Copy_List (Aspect_Specifications (Source)));
end if;
-- Set Entity field to Empty to ensure that no entity references
-- are shared between the two, if the source is already analyzed.

53
gcc/ada/freeze.adb
View File

@ -2398,6 +2398,24 @@ package body Freeze is
Set_Has_Non_Standard_Rep (Base_Type (Arr), True);
Set_Is_Bit_Packed_Array (Base_Type (Arr), True);
Set_Is_Packed (Base_Type (Arr), True);
-- Make sure that we have the necessary routines to
-- implement the packing, and complain now if not.
declare
CS : constant Int := UI_To_Int (Csiz);
RE : constant RE_Id := Get_Id (CS);
begin
if RE /= RE_Null
and then not RTE_Available (RE)
then
Error_Msg_CRT
("packing of " & UI_Image (Csiz)
& "-bit components",
First_Subtype (Etype (Arr)));
end if;
end;
end if;
end;
end if;
@ -2650,37 +2668,6 @@ package body Freeze is
Create_Packed_Array_Impl_Type (Arr);
Freeze_And_Append (Packed_Array_Impl_Type (Arr), N, Result);
-- Make sure that we have the necessary routines to implement the
-- packing, and complain now if not. Note that we only test this
-- for constrained array types.
if Is_Constrained (Arr)
and then Is_Bit_Packed_Array (Arr)
and then Present (Packed_Array_Impl_Type (Arr))
and then Is_Array_Type (Packed_Array_Impl_Type (Arr))
then
declare
CS : constant Uint := Component_Size (Arr);
RE : constant RE_Id := Get_Id (UI_To_Int (CS));
begin
if RE /= RE_Null
and then not RTE_Available (RE)
then
Error_Msg_CRT
("packing of " & UI_Image (CS) & "-bit components",
First_Subtype (Etype (Arr)));
-- Cancel the packing
Set_Is_Packed (Base_Type (Arr), False);
Set_Is_Bit_Packed_Array (Base_Type (Arr), False);
Set_Packed_Array_Impl_Type (Arr, Empty);
goto Skip_Packed;
end if;
end;
end if;
-- Size information of packed array type is copied to the array
-- type, since this is really the representation. But do not
-- override explicit existing size values. If the ancestor subtype
@ -2702,8 +2689,6 @@ package body Freeze is
end if;
end if;
<<Skip_Packed>>
-- For non-packed arrays set the alignment of the array to the
-- alignment of the component type if it is unknown. Skip this
-- in atomic case (atomic arrays may need larger alignments).
@ -4835,7 +4820,7 @@ package body Freeze is
if Is_Ghost_Entity (E)
and then Is_Effectively_Volatile (E)
then
SPARK_Msg_N ("ghost type & cannot be volatile", E);
Error_Msg_N ("ghost type & cannot be volatile", E);
end if;
-- Deal with special cases of freezing for subtype

21
gcc/ada/inline.adb
View File

@ -1316,12 +1316,23 @@ package body Inline is
-----------------------
function Has_Some_Contract (Id : Entity_Id) return Boolean is
Items : constant Node_Id := Contract (Id);
Items : Node_Id;
begin
return Present (Items)
and then (Present (Pre_Post_Conditions (Items)) or else
Present (Contract_Test_Cases (Items)) or else
Present (Classifications (Items)));
-- A call to an expression function may precede the actual body which
-- is inserted at the end of the enclosing declarations. Ensure that
-- the related entity is analyzed before inspecting the contract.
if Analyzed (Id) then
Items := Contract (Id);
return Present (Items)
and then (Present (Pre_Post_Conditions (Items)) or else
Present (Contract_Test_Cases (Items)) or else
Present (Classifications (Items)));
end if;
return False;
end Has_Some_Contract;
-----------------------------

28
gcc/ada/sem_ch3.adb
View File

@ -3185,24 +3185,22 @@ package body Sem_Ch3 is
Obj_Id);
end if;
end if;
end if;
if Is_Ghost_Entity (Obj_Id) then
if Is_Ghost_Entity (Obj_Id) then
-- A Ghost object cannot be effectively volatile
-- (SPARK RM 6.9(8)).
-- A Ghost object cannot be effectively volatile (SPARK RM 6.9(8))
if Is_Effectively_Volatile (Obj_Id) then
SPARK_Msg_N ("ghost variable & cannot be volatile", Obj_Id);
if Is_Effectively_Volatile (Obj_Id) then
Error_Msg_N ("ghost variable & cannot be volatile", Obj_Id);
-- A Ghost object cannot be imported or exported
-- (SPARK RM 6.9(8)).
-- A Ghost object cannot be imported or exported (SPARK RM 6.9(8))
elsif Is_Imported (Obj_Id) then
SPARK_Msg_N ("ghost object & cannot be imported", Obj_Id);
elsif Is_Imported (Obj_Id) then
Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
elsif Is_Exported (Obj_Id) then
SPARK_Msg_N ("ghost object & cannot be exported", Obj_Id);
end if;
elsif Is_Exported (Obj_Id) then
Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
end if;
end if;
@ -3256,10 +3254,10 @@ package body Sem_Ch3 is
if Is_Ghost_Entity (Obj_Id) then
if Is_Exported (Obj_Id) then
SPARK_Msg_N ("ghost object & cannot be exported", Obj_Id);
Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
elsif Is_Imported (Obj_Id) then
SPARK_Msg_N ("ghost object & cannot be imported", Obj_Id);
Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
end if;
end if;
end Analyze_Object_Contract;
@ -4788,8 +4786,6 @@ package body Sem_Ch3 is
when Class_Wide_Kind =>
Set_Ekind (Id, E_Class_Wide_Subtype);
Set_First_Entity (Id, First_Entity (T));
Set_Last_Entity (Id, Last_Entity (T));
Set_Class_Wide_Type (Id, Class_Wide_Type (T));
Set_Cloned_Subtype (Id, T);
Set_Is_Tagged_Type (Id, True);

4
gcc/ada/sem_ch5.adb
View File

@ -2063,6 +2063,10 @@ package body Sem_Ch5 is
Error_Msg_NE
("\to iterate directly over the elements of a container, "
& "write `of &`", Name (N), Original_Node (Name (N)));
-- No point in continuing analysis of iterator spec.
return;
end if;
end if;

5
gcc/ada/sem_ch6.adb
View File

@ -1453,6 +1453,11 @@ package body Sem_Ch6 is
-- there are various error checks that are applied on this body
-- when it is analyzed (e.g. correct aspect placement).
if Has_Completion (Prev) then
Error_Msg_Sloc := Sloc (Prev);
Error_Msg_NE ("duplicate body for & declared#", N, Prev);
end if;
Is_Completion := True;
Rewrite (N, Null_Body);
Analyze (N);

25
gcc/ada/sem_res.adb
View File

@ -846,16 +846,16 @@ package body Sem_Res is
if Is_Checked_Ghost_Entity (Id) and then Policy = Name_Ignore then
Error_Msg_Sloc := Sloc (Err_N);
SPARK_Msg_N ("incompatible ghost policies in effect", Err_N);
SPARK_Msg_NE ("\& declared with ghost policy Check", Err_N, Id);
SPARK_Msg_NE ("\& used # with ghost policy Ignore", Err_N, Id);
Error_Msg_N ("incompatible ghost policies in effect", Err_N);
Error_Msg_NE ("\& declared with ghost policy Check", Err_N, Id);
Error_Msg_NE ("\& used # with ghost policy Ignore", Err_N, Id);
elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then
Error_Msg_Sloc := Sloc (Err_N);
SPARK_Msg_N ("incompatible ghost policies in effect", Err_N);
SPARK_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id);
SPARK_Msg_NE ("\& used # with ghost policy Check", Err_N, Id);
Error_Msg_N ("incompatible ghost policies in effect", Err_N);
Error_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id);
Error_Msg_NE ("\& used # with ghost policy Check", Err_N, Id);
end if;
end Check_Ghost_Policy;
@ -873,7 +873,7 @@ package body Sem_Res is
-- its behavior or value.
else
SPARK_Msg_N
Error_Msg_N
("ghost entity cannot appear in this context (SPARK RM 6.9(12))",
Ghost_Ref);
end if;
@ -7089,13 +7089,14 @@ package body Sem_Res is
("volatile object cannot appear in this context "
& "(SPARK RM 7.1.3(13))", N);
end if;
-- A Ghost entity must appear in a specific context
elsif Is_Ghost_Entity (E) and then Comes_From_Source (N) then
Check_Ghost_Context (E, N);
end if;
end if;
-- A Ghost entity must appear in a specific context
if Is_Ghost_Entity (E) and then Comes_From_Source (N) then
Check_Ghost_Context (E, N);
end if;
end Resolve_Entity_Name;
-------------------

20
gcc/ada/sem_util.adb
View File

@ -2688,18 +2688,18 @@ package body Sem_Util is
then
Error_Msg_Sloc := Sloc (Full_View);
SPARK_Msg_N ("incompatible ghost policies in effect", Partial_View);
SPARK_Msg_N ("\& declared with ghost policy Check", Partial_View);
SPARK_Msg_N ("\& completed # with ghost policy Ignore", Partial_View);
Error_Msg_N ("incompatible ghost policies in effect", Partial_View);
Error_Msg_N ("\& declared with ghost policy Check", Partial_View);
Error_Msg_N ("\& completed # with ghost policy Ignore", Partial_View);
elsif Is_Ignored_Ghost_Entity (Partial_View)
and then Policy = Name_Check
then
Error_Msg_Sloc := Sloc (Full_View);
SPARK_Msg_N ("incompatible ghost policies in effect", Partial_View);
SPARK_Msg_N ("\& declared with ghost policy Ignore", Partial_View);
SPARK_Msg_N ("\& completed # with ghost policy Check", Partial_View);
Error_Msg_N ("incompatible ghost policies in effect", Partial_View);
Error_Msg_N ("\& declared with ghost policy Ignore", Partial_View);
Error_Msg_N ("\& completed # with ghost policy Check", Partial_View);
end if;
end Check_Ghost_Completion;
@ -2722,8 +2722,8 @@ package body Sem_Util is
-- The parent type of a Ghost type extension must be Ghost
elsif not Is_Ghost_Entity (Parent_Typ) then
SPARK_Msg_N ("type extension & cannot be ghost", Typ);
SPARK_Msg_NE ("\parent type & is not ghost", Typ, Parent_Typ);
Error_Msg_N ("type extension & cannot be ghost", Typ);
Error_Msg_NE ("\parent type & is not ghost", Typ, Parent_Typ);
return;
end if;
@ -2735,8 +2735,8 @@ package body Sem_Util is
Iface := Node (Iface_Elmt);
if not Is_Ghost_Entity (Iface) then
SPARK_Msg_N ("type extension & cannot be ghost", Typ);
SPARK_Msg_NE ("\interface type & is not ghost", Typ, Iface);
Error_Msg_N ("type extension & cannot be ghost", Typ);
Error_Msg_NE ("\interface type & is not ghost", Typ, Iface);
return;
end if;