Commit 10274386 by Arnaud Charlet

[multiple changes]

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

	* einfo.adb (Set_Is_Checked_Ghost_Entity,
	Set_Is_Ignored_Ghost_Entity): Add exceptions to the assertion
	check.
	* sem_ch6.adb (Check_Conformance): Consider only
	source subprograms when checking for Ghost conformance.
	* sem_prag.adb (Analyze_Pragma): Handle the case
	where pragma Ghost applies to a stand alone subprogram body that
	acts as a compilation unit.
	* sem_res.adb: Minor reformatting (merge if statements).

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

	* exp_strm.adb (Build_Record_Or_Elementary_Input_Function):
	Check whether underlying type is constrained before generating
	the object declaration for the result object of the function.

From-SVN: r217226
parent 8ad1c2df
2014-11-07 Hristian Kirtchev <kirtchev@adacore.com>
* einfo.adb (Set_Is_Checked_Ghost_Entity,
Set_Is_Ignored_Ghost_Entity): Add exceptions to the assertion
check.
* sem_ch6.adb (Check_Conformance): Consider only
source subprograms when checking for Ghost conformance.
* sem_prag.adb (Analyze_Pragma): Handle the case
where pragma Ghost applies to a stand alone subprogram body that
acts as a compilation unit.
* sem_res.adb: Minor reformatting (merge if statements).
2014-11-07 Ed Schonberg <schonberg@adacore.com>
* exp_strm.adb (Build_Record_Or_Elementary_Input_Function):
Check whether underlying type is constrained before generating
the object declaration for the result object of the function.
2014-11-07 Robert Dewar <dewar@adacore.com> 2014-11-07 Robert Dewar <dewar@adacore.com>
* freeze.adb: Code clean up. * freeze.adb: Code clean up.
......
...@@ -4748,6 +4748,7 @@ package body Einfo is ...@@ -4748,6 +4748,7 @@ package body Einfo is
or else Ekind (Id) = E_Abstract_State or else Ekind (Id) = E_Abstract_State
or else Ekind (Id) = E_Component or else Ekind (Id) = E_Component
or else Ekind (Id) = E_Discriminant or else Ekind (Id) = E_Discriminant
or else Ekind (Id) = E_Exception
or else Ekind (Id) = E_Package_Body or else Ekind (Id) = E_Package_Body
or else Ekind (Id) = E_Subprogram_Body); or else Ekind (Id) = E_Subprogram_Body);
Set_Flag277 (Id, V); Set_Flag277 (Id, V);
...@@ -4942,6 +4943,7 @@ package body Einfo is ...@@ -4942,6 +4943,7 @@ package body Einfo is
or else Ekind (Id) = E_Abstract_State or else Ekind (Id) = E_Abstract_State
or else Ekind (Id) = E_Component or else Ekind (Id) = E_Component
or else Ekind (Id) = E_Discriminant or else Ekind (Id) = E_Discriminant
or else Ekind (Id) = E_Exception
or else Ekind (Id) = E_Package_Body or else Ekind (Id) = E_Package_Body
or else Ekind (Id) = E_Subprogram_Body); or else Ekind (Id) = E_Subprogram_Body);
Set_Flag278 (Id, V); Set_Flag278 (Id, V);
......
...@@ -1123,9 +1123,15 @@ package body Exp_Strm is ...@@ -1123,9 +1123,15 @@ package body Exp_Strm is
J := 1; J := 1;
-- In the presence of multiple instantiations (as in uses of the Booch
-- components) the base type may be private, and the underlying type
-- already constrained, in which case there's no discriminant constraint
-- to construct.
if Has_Discriminants (Typ) if Has_Discriminants (Typ)
and then and then
No (Discriminant_Default_Value (First_Discriminant (Typ))) No (Discriminant_Default_Value (First_Discriminant (Typ)))
and then not Is_Constrained (Underlying_Type (B_Typ))
then then
Discr := First_Discriminant (B_Typ); Discr := First_Discriminant (B_Typ);
......
...@@ -4766,9 +4766,14 @@ package body Sem_Ch6 is ...@@ -4766,9 +4766,14 @@ package body Sem_Ch6 is
return; return;
-- Pragma Ghost behaves as a convention in the context of subtype -- Pragma Ghost behaves as a convention in the context of subtype
-- conformance (SPARK RM 6.9(5)). -- 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 Is_Ghost_Entity (Old_Id) /= Is_Ghost_Entity (New_Id) then 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!"); Conformance_Error ("\ghost modes do not match!");
return; return;
end if; end if;
......
...@@ -14216,7 +14216,7 @@ package body Sem_Prag is ...@@ -14216,7 +14216,7 @@ package body Sem_Prag is
-- pragma Ghost [ (boolean_EXPRESSION) ]; -- pragma Ghost [ (boolean_EXPRESSION) ];
when Pragma_Ghost => Ghost : declare when Pragma_Ghost => Ghost : declare
Context : constant Node_Id := Parent (N); Context : Node_Id;
Expr : Node_Id; Expr : Node_Id;
Id : Entity_Id; Id : Entity_Id;
Orig_Stmt : Node_Id; Orig_Stmt : Node_Id;
...@@ -14228,6 +14228,14 @@ package body Sem_Prag is ...@@ -14228,6 +14228,14 @@ package body Sem_Prag is
Check_No_Identifiers; Check_No_Identifiers;
Check_At_Most_N_Arguments (1); Check_At_Most_N_Arguments (1);
Context := Parent (N);
-- Handle compilation units
if Nkind (Context) = N_Compilation_Unit_Aux then
Context := Unit (Parent (Context));
end if;
Id := Empty; Id := Empty;
Stmt := Prev (N); Stmt := Prev (N);
while Present (Stmt) loop while Present (Stmt) loop
......
...@@ -7053,42 +7053,37 @@ package body Sem_Res is ...@@ -7053,42 +7053,37 @@ package body Sem_Res is
end if; end if;
-- The following checks are only relevant when SPARK_Mode is on as they -- The following checks are only relevant when SPARK_Mode is on as they
-- are not standard Ada legality rules. -- are not standard Ada legality rules. An effectively volatile object
-- subject to enabled properties Async_Writers or Effective_Reads must
-- appear in a specific context.
if SPARK_Mode = On then if SPARK_Mode = On
and then Is_Object (E)
-- An effectively volatile object subject to enabled properties and then Is_Effectively_Volatile (E)
-- Async_Writers or Effective_Reads must appear in a specific and then
-- context. (Async_Writers_Enabled (E) or else Effective_Reads_Enabled (E))
and then Comes_From_Source (N)
if Is_Object (E) then
and then Is_Effectively_Volatile (E) -- The effectively volatile objects appears in a "non-interfering
and then -- context" as defined in SPARK RM 7.1.3(13).
(Async_Writers_Enabled (E) or else Effective_Reads_Enabled (E))
and then Comes_From_Source (N)
then
-- The effectively volatile objects appears in a "non-interfering
-- context" as defined in SPARK RM 7.1.3(13).
if Is_OK_Volatile_Context (Par, N) then if Is_OK_Volatile_Context (Par, N) then
null; null;
-- Assume that references to effectively volatile objects that -- Assume that references to effectively volatile objects that appear
-- appear as actual parameters in a procedure call are always -- as actual parameters in a procedure call are always legal. A full
-- legal. A full legality check is done when the actuals are -- legality check is done when the actuals are resolved.
-- resolved.
elsif Nkind (Par) = N_Procedure_Call_Statement then elsif Nkind (Par) = N_Procedure_Call_Statement then
null; null;
-- Otherwise the context causes a side effect with respect to the -- Otherwise the context causes a side effect with respect to the
-- effectively volatile object. -- effectively volatile object.
else else
SPARK_Msg_N SPARK_Msg_N
("volatile object cannot appear in this context " ("volatile object cannot appear in this context "
& "(SPARK RM 7.1.3(13))", N); & "(SPARK RM 7.1.3(13))", N);
end if;
end if; end if;
end if; end if;
......
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