Skip to content

R
riscv-gcc-1
Commit 4179af27 by Hristian Kirtchev Committed by Arnaud Charlet
Options

contracts.adb (Analyze_Object_Contract): Update references to SPARK RM. 

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

	* contracts.adb (Analyze_Object_Contract): Update references to
	SPARK RM.
	* freeze.adb (Freeze_Entity): Update references to SPARK RM.
	* ghost.adb Add with and use clauses for Sem_Disp.
	(Check_Ghost_Derivation): Removed.
	(Check_Ghost_Overriding):
	Reimplemented.	(Check_Ghost_Policy): Update references to SPARK RM.
	(Check_Ghost_Primitive): New routine.
	(Check_Ghost_Refinement): New routine.	(Is_OK_Ghost_Context):
	Update references to SPARK RM.	(Is_OK_Pragma): Update references
	to SPARK RM. Predicates are now a valid context for references
	to Ghost entities.
	* ghost.ads (Check_Ghost_Derivation): Removed.
	(Check_Ghost_Overriding): Update the comment on usage.
	(Check_Ghost_Primitive): New routine.
	(Check_Ghost_Refinement): New routine.
	(Remove_Ignored_Ghost_Code): Update references to SPARK RM.
	* sem_ch3.adb (Process_Full_View): Remove the now obsolete check
	related to Ghost derivations
	* sem_ch6.adb (Check_Conformance): Remove now obsolete check
	related to the convention-like behavior of pragma Ghost.
	(Check_For_Primitive_Subprogram): Verify that the Ghost policy
	of a tagged type and its primitive agree.
	* sem_prag.adb (Analyze_Pragma): Update references to SPARK
	RM. Move the verification of pragma Assertion_Policy Ghost
	to the proper place. Remove the now obsolete check related
	to Ghost derivations.
	(Collect_Constituent): Add a call to Check_Ghost_Refinement.
	* sem_res.adb (Resolve_Actuals): Update references to SPARK RM.

From-SVN: r235115
parent 0d6014fa
Showing with 110 additions and 118 deletions
gcc/ada/ChangeLog
2016-04-18 Hristian Kirtchev <kirtchev@adacore.com>
* contracts.adb (Analyze_Object_Contract): Update references to
SPARK RM.
* freeze.adb (Freeze_Entity): Update references to SPARK RM.
* ghost.adb Add with and use clauses for Sem_Disp.
(Check_Ghost_Derivation): Removed.
(Check_Ghost_Overriding):
Reimplemented. (Check_Ghost_Policy): Update references to SPARK RM.
(Check_Ghost_Primitive): New routine.
(Check_Ghost_Refinement): New routine. (Is_OK_Ghost_Context):
Update references to SPARK RM. (Is_OK_Pragma): Update references
to SPARK RM. Predicates are now a valid context for references
to Ghost entities.
* ghost.ads (Check_Ghost_Derivation): Removed.
(Check_Ghost_Overriding): Update the comment on usage.
(Check_Ghost_Primitive): New routine.
(Check_Ghost_Refinement): New routine.
(Remove_Ignored_Ghost_Code): Update references to SPARK RM.
* sem_ch3.adb (Process_Full_View): Remove the now obsolete check
related to Ghost derivations
* sem_ch6.adb (Check_Conformance): Remove now obsolete check
related to the convention-like behavior of pragma Ghost.
(Check_For_Primitive_Subprogram): Verify that the Ghost policy
of a tagged type and its primitive agree.
* sem_prag.adb (Analyze_Pragma): Update references to SPARK
RM. Move the verification of pragma Assertion_Policy Ghost
to the proper place. Remove the now obsolete check related
to Ghost derivations.
(Collect_Constituent): Add a call to Check_Ghost_Refinement.
* sem_res.adb (Resolve_Actuals): Update references to SPARK RM.
2016-04-18 Eric Botcazou <ebotcazou@adacore.com>
* layout.adb: Fix more minor typos in comments.
......
gcc/ada/contracts.adb
......@@ -907,13 +907,13 @@ package body Contracts is
if Yields_Synchronized_Object (Obj_Typ) then
Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id);
-- A Ghost object cannot be effectively volatile (SPARK RM 6.9(8) and
-- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and
-- SPARK RM 6.9(19)).
elsif Is_Effectively_Volatile (Obj_Id) then
Error_Msg_N ("ghost object & 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(7)).
-- One exception to this is the object that represents the dispatch
-- table of a Ghost tagged type, as the symbol needs to be exported.
......
gcc/ada/freeze.adb
......@@ -3466,8 +3466,8 @@ package body Freeze is
and then Convention (E) /= Convention_Intrinsic
-- Assume that ASM interface knows what it is doing. This deals
-- with unsigned.ads in the AAMP back end.
-- Assume that ASM interface knows what it is doing. This deals
-- with unsigned.ads in the AAMP back end.
and then Convention (E) /= Convention_Assembler
then
......@@ -5213,7 +5213,7 @@ package body Freeze is
if Is_Concurrent_Type (E) then
Error_Msg_N ("ghost type & cannot be concurrent", E);
-- A Ghost type cannot be effectively volatile (SPARK RM 6.9(8))
-- A Ghost type cannot be effectively volatile (SPARK RM 6.9(7))
elsif Is_Effectively_Volatile (E) then
Error_Msg_N ("ghost type & cannot be volatile", E);
......
gcc/ada/ghost.ads
......@@ -45,16 +45,25 @@ package Ghost is
-- Determine whether node Ghost_Ref appears within a Ghost-friendly context
-- where Ghost entity Ghost_Id can safely reside.
procedure Check_Ghost_Derivation (Typ : Entity_Id);
-- Verify that the parent type and all progenitors of derived type or type
-- extension Typ are Ghost. If this is not the case, issue an error.
procedure Check_Ghost_Overriding
(Subp : Entity_Id;
Overridden_Subp : Entity_Id);
-- Verify that the Ghost policy of parent subprogram Overridden_Subp is the
-- same as the Ghost policy of overriding subprogram Subp. Emit an error if
-- this is not the case.
-- Verify that the Ghost policy of parent subprogram Overridden_Subp is
-- compatible with the Ghost policy of overriding subprogram Subp. Emit
-- an error if this is not the case.
procedure Check_Ghost_Primitive (Prim : Entity_Id; Typ : Entity_Id);
-- Verify that the Ghost policy of primitive operation Prim is the same as
-- the Ghost policy of tagged type Typ. Emit an error if this is not the
-- case.
procedure Check_Ghost_Refinement
(State : Node_Id;
State_Id : Entity_Id;
Constit : Node_Id;
Constit_Id : Entity_Id);
-- Verify that the Ghost policy of constituent Constit_Id is compatible
-- with the Ghost policy of abstract state State_I.
function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
-- Determine whether type Typ implements at least one Ghost interface
......@@ -85,7 +94,7 @@ package Ghost is
procedure Remove_Ignored_Ghost_Code;
-- Remove all code marked as ignored Ghost from the trees of all qualifying
-- units.
-- units (SPARK RM 6.9(4)).
--
-- WARNING: this is a separate front end pass, care should be taken to keep
-- it optimized.
......
gcc/ada/sem_ch3.adb
......@@ -14649,8 +14649,8 @@ package body Sem_Ch3 is
then
Set_Derived_Name;
-- Otherwise, the type is inheriting a private operation, so enter
-- it with a special name so it can't be overridden.
-- Otherwise, the type is inheriting a private operation, so enter it
-- with a special name so it can't be overridden.
else
Set_Chars (New_Subp, New_External_Name (Chars (Parent_Subp), 'P'));
......@@ -19956,14 +19956,6 @@ package body Sem_Ch3 is
Check_Ghost_Completion (Priv_T, Full_T);
-- In the case where the private view of a tagged type lacks a parent
-- type and is subject to pragma Ghost, ensure that the parent type
-- specified by the full view is also Ghost (SPARK RM 6.9(9)).
if Is_Derived_Type (Full_T) then
Check_Ghost_Derivation (Full_T);
end if;
-- Propagate the attributes related to pragma Ghost from the private
-- to the full view.
......
gcc/ada/sem_ch6.adb
......@@ -4701,18 +4701,6 @@ package body Sem_Ch6 is
then
Conformance_Error ("\formal subprograms not allowed!");
return;
-- Pragma Ghost behaves as a convention in the context of subtype
-- conformance (SPARK RM 6.9(5)). Do not check internally generated
-- subprograms as their spec may reside in a Ghost region and their
-- body not, or vice versa.
elsif Comes_From_Source (Old_Id)
and then Comes_From_Source (New_Id)
and then Is_Ghost_Entity (Old_Id) /= Is_Ghost_Entity (New_Id)
then
Conformance_Error ("\ghost modes do not match!");
return;
end if;
end if;
......@@ -9014,6 +9002,12 @@ package body Sem_Ch6 is
Set_Has_Primitive_Operations (B_Typ);
Set_Is_Primitive (S);
Check_Private_Overriding (B_Typ);
-- The Ghost policy in effect at the point of declaration of
-- a tagged type and a primitive operation must match
-- (SPARK RM 6.9(16)).
Check_Ghost_Primitive (S, B_Typ);
end if;
end if;
......@@ -9041,6 +9035,12 @@ package body Sem_Ch6 is
Set_Is_Primitive (S);
Set_Has_Primitive_Operations (B_Typ);
Check_Private_Overriding (B_Typ);
-- The Ghost policy in effect at the point of declaration of
-- a tagged type and a primitive operation must match
-- (SPARK RM 6.9(16)).
Check_Ghost_Primitive (S, B_Typ);
end if;
Next_Formal (Formal);
......@@ -9068,6 +9068,12 @@ package body Sem_Ch6 is
Set_Is_Primitive (S);
Set_Has_Primitive_Operations (B_Typ);
Check_Private_Overriding (B_Typ);
-- The Ghost policy in effect at the point of declaration of a
-- tagged type and a primitive operation must match
-- (SPARK RM 6.9(16)).
Check_Ghost_Primitive (S, B_Typ);
end if;
end if;
end Check_For_Primitive_Subprogram;
......
gcc/ada/sem_prag.adb
......@@ -11585,7 +11585,8 @@ package body Sem_Prag is
-- Check Kind and Policy have allowed forms
Kind := Chars (Arg);
Kind := Chars (Arg);
Policy := Get_Pragma_Arg (Arg);
if not Is_Valid_Assertion_Kind (Kind) then
Error_Pragma_Arg
......@@ -11595,6 +11596,30 @@ package body Sem_Prag is
Check_Arg_Is_One_Of
(Arg, Name_Check, Name_Disable, Name_Ignore);
if Kind = Name_Ghost then
-- The Ghost policy must be either Check or Ignore
-- (SPARK RM 6.9(6)).
if not Nam_In (Chars (Policy), Name_Check,
Name_Ignore)
then
Error_Pragma_Arg
("argument of pragma % Ghost must be Check or "
& "Ignore", Policy);
end if;
-- Pragma Assertion_Policy specifying a Ghost policy
-- cannot occur within a Ghost subprogram or package
-- (SPARK RM 6.9(14)).
if Ghost_Mode > None then
Error_Pragma
("pragma % cannot appear within ghost subprogram or "
& "package");
end if;
end if;
-- Rewrite the Assertion_Policy pragma as a series of
-- Check_Policy pragmas of the form:
......@@ -11612,7 +11637,7 @@ package body Sem_Prag is
Make_Pragma_Argument_Association (LocP,
Expression => Make_Identifier (LocP, Kind)),
Make_Pragma_Argument_Association (LocP,
Expression => Get_Pragma_Arg (Arg)))));
Expression => Policy))));
Arg := Next (Arg);
end loop;
......@@ -12371,8 +12396,7 @@ package body Sem_Prag is
-- new form syntax.
when Pragma_Check_Policy => Check_Policy : declare
Ident : Node_Id;
Kind : Node_Id;
Kind : Node_Id;
begin
GNAT_Pragma;
......@@ -12416,29 +12440,6 @@ package body Sem_Prag is
Check_Arg_Is_One_Of
(Arg2,
Name_On, Name_Off, Name_Check, Name_Disable, Name_Ignore);
Ident := Get_Pragma_Arg (Arg2);
if Chars (Kind) = Name_Ghost then
-- Pragma Check_Policy specifying a Ghost policy cannot
-- occur within a ghost subprogram or package.
if Ghost_Mode > None then
Error_Pragma
("pragma % cannot appear within ghost subprogram or "
& "package");
-- The policy identifier of pragma Ghost must be either
-- Check or Ignore (SPARK RM 6.9(7)).
elsif not Nam_In (Chars (Ident), Name_Check,
Name_Ignore)
then
Error_Pragma_Arg
("argument of pragma % Ghost must be Check or Ignore",
Arg2);
end if;
end if;
-- And chain pragma on the Check_Policy_List for search
......@@ -15021,14 +15022,6 @@ package body Sem_Prag is
return;
end if;
-- A derived type or type extension cannot be subject to pragma
-- Ghost if either the parent type or one of the progenitor types
-- is not Ghost (SPARK RM 6.9(9)).
if Is_Derived_Type (Id) then
Check_Ghost_Derivation (Id);
end if;
-- Handle completions of types and constants that are subject to
-- pragma Ghost.
......@@ -15040,7 +15033,7 @@ package body Sem_Prag is
-- The full declaration of a deferred constant cannot be
-- subject to pragma Ghost unless the deferred declaration
-- is also Ghost (SPARK RM 6.9(10)).
-- is also Ghost (SPARK RM 6.9(9)).
if Ekind (Prev_Id) = E_Constant then
Error_Msg_Name_1 := Pname;
......@@ -15058,7 +15051,7 @@ package body Sem_Prag is
-- The full declaration of a type cannot be subject to
-- pragma Ghost unless the partial view is also Ghost
-- (SPARK RM 6.9(10)).
-- (SPARK RM 6.9(9)).
else
Error_Msg_NE (Fix_Error
......@@ -15092,7 +15085,7 @@ package body Sem_Prag is
if Is_OK_Static_Expression (Expr) then
-- "Ghostness" cannot be turned off once enabled within a
-- region (SPARK RM 6.9(7)).
-- region (SPARK RM 6.9(6)).
if Is_False (Expr_Value (Expr))
and then Ghost_Mode > None
......@@ -25230,51 +25223,11 @@ package body Sem_Prag is
procedure Collect_Constituent is
begin
if Is_Ghost_Entity (State_Id) then
if Is_Ghost_Entity (Constit_Id) then
-- The Ghost policy in effect at the point of abstract
-- state declaration and constituent must match
-- (SPARK RM 6.9(16)).
if Is_Checked_Ghost_Entity (State_Id)
and then Is_Ignored_Ghost_Entity (Constit_Id)
then
Error_Msg_Sloc := Sloc (Constit);
SPARK_Msg_N
("incompatible ghost policies in effect", State);
SPARK_Msg_NE
("\abstract state & declared with ghost policy "
& "Check", State, State_Id);
SPARK_Msg_NE
("\constituent & declared # with ghost policy "
& "Ignore", State, Constit_Id);
elsif Is_Ignored_Ghost_Entity (State_Id)
and then Is_Checked_Ghost_Entity (Constit_Id)
then
Error_Msg_Sloc := Sloc (Constit);
SPARK_Msg_N
("incompatible ghost policies in effect", State);
SPARK_Msg_NE
("\abstract state & declared with ghost policy "
& "Ignore", State, State_Id);
SPARK_Msg_NE
("\constituent & declared # with ghost policy "
& "Check", State, Constit_Id);
end if;
-- The Ghost policy in effect at the point of abstract state
-- declaration and constituent must match (SPARK RM 6.9(15))
-- A constituent of a Ghost abstract state must be a
-- Ghost entity (SPARK RM 7.2.2(12)).
else
SPARK_Msg_NE
("constituent of ghost state & must be ghost",
Constit, State_Id);
end if;
end if;
Check_Ghost_Refinement
(State, State_Id, Constit, Constit_Id);
-- A synchronized state must be refined by a synchronized
-- object or another synchronized state (SPARK RM 9.6).
......
gcc/ada/sem_res.adb
......@@ -4528,7 +4528,7 @@ package body Sem_Res is
end if;
-- The actual parameter of a Ghost subprogram whose formal is of
-- mode IN OUT or OUT must be a Ghost variable (SPARK RM 6.9(13)).
-- mode IN OUT or OUT must be a Ghost variable (SPARK RM 6.9(12)).
if Comes_From_Source (Nam)
and then Is_Ghost_Entity (Nam)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment