* [Ada] Use of attributes 'Old and 'Result and local entities in another 'Old
@ 2014-02-18 11:57 Arnaud Charlet
0 siblings, 0 replies; only message in thread
From: Arnaud Charlet @ 2014-02-18 11:57 UTC (permalink / raw)
To: gcc-patches; +Cc: Hristian Kirtchev
[-- Attachment #1: Type: text/plain, Size: 2236 bytes --]
This patch implements the following sentence from Ada RM 6.1.1 (27/3):
The prefix of an Old attribute_reference shall not contain a Result
attribute_reference, nor an Old attribute_reference, nor a use of an entity
declared within the postcondition expression but not within prefix itself
(for example, the loop parameter of an enclosing quantified_expression).
------------
-- Source --
------------
-- semantics.ads
package Semantics is
Stuff : array (1 .. 5) of Integer;
procedure Local_Entity_In_Spec
with Post =>
(for all Index in 1 .. 5 =>
Stuff (Index) = Stuff (Index)'Old - 1);
procedure Nested_Old_In_Spec (Param : in out Integer)
with Post =>
Param = Param'Old'Old;
end Semantics
-- semantics.adb
package body Semantics is
procedure Local_Entity_In_Body
with Post =>
(for all Index in 1 .. 5 =>
Stuff (Index) = Stuff (Index)'Old - 1)
is begin null; end Local_Entity_In_Body;
procedure Local_Entity_In_Spec is begin null; end Local_Entity_In_Spec;
procedure Nested_Old_In_Body (Param : in out Integer)
with Post =>
Param = Param'Old'Old
is begin null; end Nested_Old_In_Body;
procedure Nested_Old_In_Spec (Param : in out Integer) is
begin null; end Nested_Old_In_Spec;
end Semantics;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c semantics.adb
semantics.adb:5:34: prefix of attribute "Old" cannot reference local entities
semantics.adb:12:21: attribute "Old" cannot appear in the prefix of attribute
"Old"
semantics.ads:7:34: prefix of attribute "Old" cannot reference local entities
semantics.ads:11:21: attribute "Old" cannot appear in the prefix of attribute
"Old"
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-02-18 Hristian Kirtchev <kirtchev@adacore.com>
* sem_attr.adb (Analyze_Attribute): Comment
and code reformatting. Use separate routines to check the
legality of attribute 'Old in certain pragmas. Verify
the use of 'Old, 'Result and locally declared entities
within the prefix of 'Old.
(Check_References_In_Prefix): New routine.
(Check_Use_In_Contract_Cases): New routine.
(Check_Use_In_Test_Case): New routine.
[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 10789 bytes --]
Index: sem_attr.adb
===================================================================
--- sem_attr.adb (revision 207558)
+++ sem_attr.adb (working copy)
@@ -4373,6 +4373,137 @@
---------
when Attribute_Old => Old : declare
+ procedure Check_References_In_Prefix (Subp_Id : Entity_Id);
+ -- Inspect the contents of the prefix and detect illegal uses of a
+ -- nested 'Old, attribute 'Result or a use of an entity declared in
+ -- the related postcondition expression. Subp_Id is the subprogram to
+ -- which the related postcondition applies.
+
+ procedure Check_Use_In_Contract_Cases (Prag : Node_Id);
+ -- Perform various semantic checks related to the placement of the
+ -- attribute in pragma Contract_Cases.
+
+ procedure Check_Use_In_Test_Case (Prag : Node_Id);
+ -- Perform various semantic checks related to the placement of the
+ -- attribute in pragma Contract_Cases.
+
+ --------------------------------
+ -- Check_References_In_Prefix --
+ --------------------------------
+
+ procedure Check_References_In_Prefix (Subp_Id : Entity_Id) is
+ function Check_Reference (Nod : Node_Id) return Traverse_Result;
+ -- Detect attribute 'Old, attribute 'Result of a use of an entity
+ -- and perform the appropriate semantic check.
+
+ ---------------------
+ -- Check_Reference --
+ ---------------------
+
+ function Check_Reference (Nod : Node_Id) return Traverse_Result is
+ begin
+ -- Attributes 'Old and 'Result cannot appear in the prefix of
+ -- another attribute 'Old.
+
+ if Nkind (Nod) = N_Attribute_Reference
+ and then Nam_In (Attribute_Name (Nod), Name_Old,
+ Name_Result)
+ then
+ Error_Msg_Name_1 := Attribute_Name (Nod);
+ Error_Msg_Name_2 := Name_Old;
+ Error_Msg_N
+ ("attribute % cannot appear in the prefix of attribute %",
+ Nod);
+ return Abandon;
+
+ -- Entities mentioned within the prefix of attribute 'Old must
+ -- be global to the related postcondition. If this is not the
+ -- case, then the scope of the local entity is be nested within
+ -- that of the subprogram.
+
+ elsif Nkind (Nod) = N_Identifier
+ and then Present (Entity (Nod))
+ and then Scope_Within (Scope (Entity (Nod)), Subp_Id)
+ then
+ Error_Attr
+ ("prefix of attribute % cannot reference local entities",
+ Nod);
+ return Abandon;
+ else
+ return OK;
+ end if;
+ end Check_Reference;
+
+ procedure Check_References is new Traverse_Proc (Check_Reference);
+
+ -- Start of processing for Check_References_In_Prefix
+
+ begin
+ Check_References (P);
+ end Check_References_In_Prefix;
+
+ ---------------------------------
+ -- Check_Use_In_Contract_Cases --
+ ---------------------------------
+
+ procedure Check_Use_In_Contract_Cases (Prag : Node_Id) is
+ Cases : constant Node_Id :=
+ Get_Pragma_Arg
+ (First (Pragma_Argument_Associations (Prag)));
+ Expr : Node_Id;
+
+ begin
+ -- Climb the parent chain to reach the top of the expression where
+ -- attribute 'Old resides.
+
+ Expr := N;
+ while Parent (Parent (Expr)) /= Cases loop
+ Expr := Parent (Expr);
+ end loop;
+
+ -- Ensure that the obtained expression is the consequence of a
+ -- contract case as this is the only postcondition-like part of
+ -- the pragma.
+
+ if Expr /= Expression (Parent (Expr)) then
+ Error_Attr
+ ("attribute % cannot appear in the condition of a contract "
+ & "case (SPARK RM 6.1.3(2))", P);
+ end if;
+ end Check_Use_In_Contract_Cases;
+
+ ----------------------------
+ -- Check_Use_In_Test_Case --
+ ----------------------------
+
+ procedure Check_Use_In_Test_Case (Prag : Node_Id) is
+ Ensures : constant Node_Id := Get_Ensures_From_CTC_Pragma (Prag);
+ Expr : Node_Id;
+
+ begin
+ -- Climb the parent chain to reach the top of the Ensures part of
+ -- pragma Test_Case.
+
+ Expr := N;
+ while Expr /= Prag loop
+ if Expr = Ensures then
+ return;
+ end if;
+
+ Expr := Parent (Expr);
+ end loop;
+
+ -- If we get there, then attribute 'Old appears in the requires
+ -- expression of pragma Test_Case which is not a postcondition-
+ -- like context.
+
+ Error_Attr
+ ("attribute % cannot appear in the requires expression of a "
+ & "test case", P);
+ end Check_Use_In_Test_Case;
+
+ -- Local variables
+
CS : Entity_Id;
-- The enclosing scope, excluding loops for quantified expressions.
-- During analysis, it is the postcondition subprogram. During
@@ -4381,6 +4512,8 @@
Prag : Node_Id;
-- During pre-analysis, Prag is the enclosing pragma node if any
+ -- Start of processing for Old
+
begin
Prag := Empty;
@@ -4391,19 +4524,17 @@
CS := Scope (CS);
end loop;
- -- If we are in Spec_Expression mode, this should be the prescan of
- -- the postcondition (or contract case, or test case) pragma.
+ -- A Contract_Cases, Postcondition or Test_Case pragma is in the
+ -- process of being preanalyzed. Perform the semantic checks now
+ -- before the pragma is relocated and/or expanded.
if In_Spec_Expression then
-
- -- Check in postcondition, Test_Case or Contract_Cases
-
Prag := N;
while Present (Prag)
- and then not Nkind_In (Prag, N_Pragma,
+ and then not Nkind_In (Prag, N_Aspect_Specification,
N_Function_Specification,
+ N_Pragma,
N_Procedure_Specification,
- N_Aspect_Specification,
N_Subprogram_Body)
loop
Prag := Parent (Prag);
@@ -4416,64 +4547,25 @@
if Nkind (Prag) = N_Aspect_Specification then
null;
- -- We must have a pragma
+ -- In all other cases the related context must be a pragma
elsif Nkind (Prag) /= N_Pragma then
Error_Attr ("% attribute can only appear in postcondition", P);
- -- Processing depends on which pragma we have
+ -- Verify the placement of the attribute with respect to the
+ -- related pragma.
else
case Get_Pragma_Id (Prag) is
- when Pragma_Test_Case =>
- declare
- Arg_Ens : constant Node_Id :=
- Get_Ensures_From_CTC_Pragma (Prag);
- Arg : Node_Id;
-
- begin
- Arg := N;
- while Arg /= Prag and then Arg /= Arg_Ens loop
- Arg := Parent (Arg);
- end loop;
-
- if Arg /= Arg_Ens then
- Error_Attr
- ("% attribute misplaced inside test case", P);
- end if;
- end;
-
when Pragma_Contract_Cases =>
- declare
- Aggr : constant Node_Id :=
- Expression
- (First (Pragma_Argument_Associations (Prag)));
- Arg : Node_Id;
+ Check_Use_In_Contract_Cases (Prag);
- begin
- Arg := N;
- while Arg /= Prag
- and then Parent (Parent (Arg)) /= Aggr
- loop
- Arg := Parent (Arg);
- end loop;
-
- -- At this point, Parent (Arg) should be a component
- -- association. Attribute Result is only allowed in
- -- the expression part of this association.
-
- if Nkind (Parent (Arg)) /= N_Component_Association
- or else Arg /= Expression (Parent (Arg))
- then
- Error_Attr
- ("% attribute misplaced inside contract cases",
- P);
- end if;
- end;
-
when Pragma_Postcondition | Pragma_Refined_Post =>
null;
+ when Pragma_Test_Case =>
+ Check_Use_In_Test_Case (Prag);
+
when others =>
Error_Attr
("% attribute can only appear in postcondition", P);
@@ -4489,6 +4581,7 @@
elsif not Expander_Active and then In_Refined_Post then
Preanalyze_And_Resolve (P);
+ Check_References_In_Prefix (CS);
P_Type := Etype (P);
Set_Etype (N, P_Type);
@@ -4548,6 +4641,7 @@
-- place during expansion (see below).
Preanalyze_And_Resolve (P);
+ Check_References_In_Prefix (CS);
P_Type := Etype (P);
Set_Etype (N, P_Type);
@@ -4570,8 +4664,9 @@
and then Is_Potentially_Unevaluated (N)
and then not Is_Entity_Name (P)
then
- Error_Attr_P ("prefix of attribute % that is potentially "
- & "unevaluated must denote an entity");
+ Error_Attr_P
+ ("prefix of attribute % that is potentially unevaluated must "
+ & "denote an entity");
end if;
-- The attribute appears within a pre/postcondition, but refers to
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2014-02-18 11:57 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2014-02-18 11:57 [Ada] Use of attributes 'Old and 'Result and local entities in another 'Old Arnaud Charlet
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).