This patch adds logic to verify that the expression of aspect/pragma
Refined_Post mentions 'Result and introduces a post-state when applied to a
function.
------------
-- Source --
------------
-- result_and_post.ads
package Result_And_Post is
function OK (Formal : Integer) return Integer;
function Error (Formal : Integer) return Integer;
end Result_And_Post;
-- result_and_post.adb
package body Result_And_Post is
function OK (Formal : Integer) return Integer
with Refined_Post => OK'Result = Formal + 1
is
begin
return Formal + 1;
end OK;
function Error (Formal : Integer) return Integer
with Refined_Post => True
is
begin
return Formal + 1;
end Error;
end Result_And_Post;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c -gnatw.t result_and_post.adb
result_and_post.adb:10:11: warning: aspect "Refined_Post" does not mention
function result
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-01-20 Hristian Kirtchev <kirtc...@adacore.com>
* sem_attr.adb (Analyze_Attribute): Attributes 'Old and 'Result
can now apply to a refined postcondition.
* sem_ch6.adb (Analyze_Subprogram_Contract): Remove local
variable Result_Seen. Add variables Case_Prag, Post_Prag,
Seen_In_Case and Seen_In_Post. Update the mechanism that detects
whether postconditions and/or constract-cases mention attribute
'Result and introduce a post-state when applied to functions.
(Check_Result_And_Post_State): Removed.
* sem_prag.adb (Analyze_Pragma): Add local variable
Result_Seen. Verify that the expression of pragma Refined_Post
mentions attribute 'Result and introduces a post-state.
* sem_util.ads, sem_util.adb (Check_Result_And_Post_State): New routine.
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 206818)
+++ sem_prag.adb (working copy)
@@ -17331,9 +17331,10 @@
-- pragma Refined_Post (boolean_EXPRESSION);
when Pragma_Refined_Post => Refined_Post : declare
- Body_Id : Entity_Id;
- Legal : Boolean;
- Spec_Id : Entity_Id;
+ Body_Id : Entity_Id;
+ Legal : Boolean;
+ Result_Seen : Boolean := False;
+ Spec_Id : Entity_Id;
begin
Analyze_Refined_Pragma (Spec_Id, Body_Id, Legal);
@@ -17342,6 +17343,20 @@
if Legal then
Analyze_Pre_Post_Condition_In_Decl_Part (N, Spec_Id);
+
+ -- Verify that the refined postcondition mentions attribute
+ -- 'Result and its expression introduces a post-state.
+
+ if Warn_On_Suspicious_Contract
+ and then Ekind_In (Spec_Id, E_Function, E_Generic_Function)
+ then
+ Check_Result_And_Post_State (N, Result_Seen);
+
+ if not Result_Seen then
+ Error_Pragma
+ ("pragma % does not mention function result?T?");
+ end if;
+ end if;
end if;
end Refined_Post;
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 206805)
+++ sem_util.adb (working copy)
@@ -2396,6 +2396,168 @@
end loop;
end Check_Potentially_Blocking_Operation;
+ ---------------------------------
+ -- Check_Result_And_Post_State --
+ ---------------------------------
+
+ procedure Check_Result_And_Post_State
+ (Prag : Node_Id;
+ Result_Seen : in out Boolean)
+ is
+ procedure Check_Expression (Expr : Node_Id);
+ -- Perform the 'Result and post-state checks on a given expression
+
+ function Is_Function_Result (N : Node_Id) return Traverse_Result;
+ -- Attempt to find attribute 'Result in a subtree denoted by N
+
+ function Is_Trivial_Boolean (N : Node_Id) return Boolean;
+ -- Determine whether source node N denotes "True" or "False"
+
+ function Mentions_Post_State (N : Node_Id) return Boolean;
+ -- Determine whether a subtree denoted by N mentions any construct that
+ -- denotes a post-state.
+
+ procedure Check_Function_Result is
+ new Traverse_Proc (Is_Function_Result);
+
+ ----------------------
+ -- Check_Expression --
+ ----------------------
+
+ procedure Check_Expression (Expr : Node_Id) is
+ begin
+ if not Is_Trivial_Boolean (Expr) then
+ Check_Function_Result (Expr);
+
+ if not Mentions_Post_State (Expr) then
+ if Pragma_Name (Prag) = Name_Contract_Cases then
+ Error_Msg_N
+ ("contract case refers only to pre-state?T?", Expr);
+
+ elsif Pragma_Name (Prag) = Name_Refined_Post then
+ Error_Msg_N
+ ("refined postcondition refers only to pre-state?T?",
+ Prag);
+
+ else
+ Error_Msg_N
+ ("postcondition refers only to pre-state?T?", Prag);
+ end if;
+ end if;
+ end if;
+ end Check_Expression;
+
+ ------------------------
+ -- Is_Function_Result --
+ ------------------------
+
+ function Is_Function_Result (N : Node_Id) return Traverse_Result is
+ begin
+ if Is_Attribute_Result (N) then
+ Result_Seen := True;
+ return Abandon;
+
+ -- Continue the traversal
+
+ else
+ return OK;
+ end if;
+ end Is_Function_Result;
+
+ ------------------------
+ -- Is_Trivial_Boolean --
+ ------------------------
+
+ function Is_Trivial_Boolean (N : Node_Id) return Boolean is
+ begin
+ return
+ Comes_From_Source (N)
+ and then Is_Entity_Name (N)
+ and then (Entity (N) = Standard_True
+ or else Entity (N) = Standard_False);
+ end Is_Trivial_Boolean;
+
+ -------------------------
+ -- Mentions_Post_State --
+ -------------------------
+
+ function Mentions_Post_State (N : Node_Id) return Boolean is
+ Post_State_Seen : Boolean := False;
+
+ function Is_Post_State (N : Node_Id) return Traverse_Result;
+ -- Attempt to find a construct that denotes a post-state. If this is
+ -- the case, set flag Post_State_Seen.
+
+ -------------------
+ -- Is_Post_State --
+ -------------------
+
+ function Is_Post_State (N : Node_Id) return Traverse_Result is
+ Ent : Entity_Id;
+
+ begin
+ if Nkind_In (N, N_Explicit_Dereference, N_Function_Call) then
+ Post_State_Seen := True;
+ return Abandon;
+
+ elsif Nkind_In (N, N_Expanded_Name, N_Identifier) then
+ Ent := Entity (N);
+
+ if No (Ent) or else Ekind (Ent) in Assignable_Kind then
+ Post_State_Seen := True;
+ return Abandon;
+ end if;
+
+ elsif Nkind (N) = N_Attribute_Reference then
+ if Attribute_Name (N) = Name_Old then
+ return Skip;
+
+ elsif Attribute_Name (N) = Name_Result then
+ Post_State_Seen := True;
+ return Abandon;
+ end if;
+ end if;
+
+ return OK;
+ end Is_Post_State;
+
+ procedure Find_Post_State is new Traverse_Proc (Is_Post_State);
+
+ -- Start of processing for Mentions_Post_State
+
+ begin
+ Find_Post_State (N);
+
+ return Post_State_Seen;
+ end Mentions_Post_State;
+
+ -- Local variables
+
+ Expr : constant Node_Id :=
+ Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag)));
+ Nam : constant Name_Id := Pragma_Name (Prag);
+ CCase : Node_Id;
+
+ -- Start of processing for Check_Result_And_Post_State
+
+ begin
+ -- Examine all consequences
+
+ if Nam = Name_Contract_Cases then
+ CCase := First (Component_Associations (Expr));
+ while Present (CCase) loop
+ Check_Expression (Expression (CCase));
+
+ Next (CCase);
+ end loop;
+
+ -- Examine the expression of a postcondition
+
+ else pragma Assert (Nam_In (Nam, Name_Postcondition, Name_Refined_Post));
+ Check_Expression (Expr);
+ end if;
+ end Check_Result_And_Post_State;
+
------------------------------
-- Check_Unprotected_Access --
------------------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 206804)
+++ sem_util.ads (working copy)
@@ -260,6 +260,14 @@
-- N is one of the statement forms that is a potentially blocking
-- operation. If it appears within a protected action, emit warning.
+ procedure Check_Result_And_Post_State
+ (Prag : Node_Id;
+ Result_Seen : in out Boolean);
+ -- Determine whether pragma Prag mentions attribute 'Result and whether
+ -- the pragma contains an expression that evaluates differently in pre-
+ -- and post-state. Prag is a [refined] postcondition or a contract-cases
+ -- pragma. Result_Seen is set when the pragma mentions attribute 'Result.
+
procedure Check_Unprotected_Access
(Context : Node_Id;
Expr : Node_Id);
Index: sem_attr.adb
===================================================================
--- sem_attr.adb (revision 206818)
+++ sem_attr.adb (working copy)
@@ -4357,52 +4357,68 @@
if Nkind (Prag) = N_Aspect_Specification then
null;
+ -- We must have a pragma
+
elsif Nkind (Prag) /= N_Pragma then
Error_Attr ("% attribute can only appear in postcondition", P);
- elsif Get_Pragma_Id (Prag) = Pragma_Test_Case then
- declare
- Arg_Ens : constant Node_Id :=
- Get_Ensures_From_CTC_Pragma (Prag);
- Arg : Node_Id;
+ -- Processing depends on which pragma we have
- begin
- Arg := N;
- while Arg /= Prag and then Arg /= Arg_Ens loop
- Arg := Parent (Arg);
- end loop;
+ 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;
- if Arg /= Arg_Ens then
- Error_Attr ("% attribute misplaced inside test case", P);
- end if;
- end;
+ begin
+ Arg := N;
+ while Arg /= Prag and then Arg /= Arg_Ens loop
+ Arg := Parent (Arg);
+ end loop;
- elsif Get_Pragma_Id (Prag) = Pragma_Contract_Cases then
- declare
- Aggr : constant Node_Id :=
- Expression (First (Pragma_Argument_Associations (Prag)));
- Arg : Node_Id;
+ if Arg /= Arg_Ens then
+ Error_Attr
+ ("% attribute misplaced inside test case", P);
+ end if;
+ end;
- begin
- Arg := N;
- while Arg /= Prag and then Parent (Parent (Arg)) /= Aggr loop
- Arg := Parent (Arg);
- end loop;
+ when Pragma_Contract_Cases =>
+ declare
+ Aggr : constant Node_Id :=
+ Expression
+ (First (Pragma_Argument_Associations (Prag)));
+ Arg : Node_Id;
- -- At this point, Parent (Arg) should be a component
- -- association. Attribute Result is only allowed in
- -- the expression part of this association.
+ begin
+ Arg := N;
+ while Arg /= Prag
+ and then Parent (Parent (Arg)) /= Aggr
+ loop
+ Arg := Parent (Arg);
+ end loop;
- if Nkind (Parent (Arg)) /= N_Component_Association
- or else Arg /= Expression (Parent (Arg))
- then
+ -- 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 others =>
Error_Attr
- ("% attribute misplaced inside contract cases", P);
- end if;
- end;
-
- elsif Get_Pragma_Id (Prag) /= Pragma_Postcondition then
- Error_Attr ("% attribute can only appear in postcondition", P);
+ ("% attribute can only appear in postcondition", P);
+ end case;
end if;
-- Check the legality of attribute 'Old when it appears inside pragma
@@ -4796,56 +4812,72 @@
if Nkind (Prag) = N_Aspect_Specification then
null;
+ -- Must have a pragma
+
elsif Nkind (Prag) /= N_Pragma then
Error_Attr
("% attribute can only appear in postcondition of function",
P);
- elsif Get_Pragma_Id (Prag) = Pragma_Test_Case then
- declare
- Arg_Ens : constant Node_Id :=
- Get_Ensures_From_CTC_Pragma (Prag);
- Arg : Node_Id;
+ -- Processing depends on which pragma we have
- begin
- Arg := N;
- while Arg /= Prag and then Arg /= Arg_Ens loop
- Arg := Parent (Arg);
- end loop;
+ else
+ case Get_Pragma_Id (Prag) is
- if Arg /= Arg_Ens then
- Error_Attr ("% attribute misplaced inside test case", P);
- end if;
- end;
+ when Pragma_Test_Case =>
+ declare
+ Arg_Ens : constant Node_Id :=
+ Get_Ensures_From_CTC_Pragma (Prag);
+ Arg : Node_Id;
- elsif Get_Pragma_Id (Prag) = Pragma_Contract_Cases then
- declare
- Aggr : constant Node_Id :=
- Expression (First (Pragma_Argument_Associations (Prag)));
- Arg : Node_Id;
+ begin
+ Arg := N;
+ while Arg /= Prag and then Arg /= Arg_Ens loop
+ Arg := Parent (Arg);
+ end loop;
- begin
- Arg := N;
- while Arg /= Prag and then Parent (Parent (Arg)) /= Aggr loop
- Arg := Parent (Arg);
- end loop;
+ if Arg /= Arg_Ens then
+ Error_Attr
+ ("% attribute misplaced inside test case", P);
+ end if;
+ end;
- -- At this point, Parent (Arg) should be a component
- -- association. Attribute Result is only allowed in
- -- the expression part of this association.
+ when Pragma_Contract_Cases =>
+ declare
+ Aggr : constant Node_Id :=
+ Expression (First
+ (Pragma_Argument_Associations (Prag)));
+ Arg : Node_Id;
- 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;
+ begin
+ Arg := N;
+ while Arg /= Prag
+ and then Parent (Parent (Arg)) /= Aggr
+ loop
+ Arg := Parent (Arg);
+ end loop;
- elsif Get_Pragma_Id (Prag) /= Pragma_Postcondition then
- Error_Attr
- ("% attribute can only appear in postcondition of function",
- P);
+ -- 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 others =>
+ Error_Attr
+ ("% attribute can only appear in postcondition "
+ & "of function", P);
+ end case;
end if;
-- The attribute reference is a primary. If expressions follow,
@@ -4866,8 +4898,8 @@
Set_Etype (N, Etype (CS));
- -- If several functions with that name are visible,
- -- the intended one is the current scope.
+ -- If several functions with that name are visible, the intended
+ -- one is the current scope.
if Is_Overloaded (P) then
Set_Entity (P, CS);
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 206813)
+++ sem_ch6.adb (working copy)
@@ -3420,191 +3420,16 @@
---------------------------------
procedure Analyze_Subprogram_Contract (Subp : Entity_Id) is
- Result_Seen : Boolean := False;
- -- A flag which keeps track of whether at least one postcondition or
- -- contract-case mentions attribute 'Result (set True if so).
+ Items : constant Node_Id := Contract (Subp);
+ Case_Prag : Node_Id := Empty;
+ Depends : Node_Id := Empty;
+ Global : Node_Id := Empty;
+ Nam : Name_Id;
+ Post_Prag : Node_Id := Empty;
+ Prag : Node_Id;
+ Seen_In_Case : Boolean := False;
+ Seen_In_Post : Boolean := False;
- procedure Check_Result_And_Post_State
- (Prag : Node_Id;
- Error_Nod : in out Node_Id);
- -- Determine whether pragma Prag mentions attribute 'Result and whether
- -- the pragma contains an expression that evaluates differently in pre-
- -- and post-state. Prag is a postcondition or a contract-cases pragma.
- -- Error_Nod denotes the proper error node.
-
- ---------------------------------
- -- Check_Result_And_Post_State --
- ---------------------------------
-
- procedure Check_Result_And_Post_State
- (Prag : Node_Id;
- Error_Nod : in out Node_Id)
- is
- procedure Check_Expression (Expr : Node_Id);
- -- Perform the 'Result and post-state checks on a given expression
-
- function Is_Function_Result (N : Node_Id) return Traverse_Result;
- -- Attempt to find attribute 'Result in a subtree denoted by N
-
- function Is_Trivial_Boolean (N : Node_Id) return Boolean;
- -- Determine whether source node N denotes "True" or "False"
-
- function Mentions_Post_State (N : Node_Id) return Boolean;
- -- Determine whether a subtree denoted by N mentions any construct
- -- that denotes a post-state.
-
- procedure Check_Function_Result is
- new Traverse_Proc (Is_Function_Result);
-
- ----------------------
- -- Check_Expression --
- ----------------------
-
- procedure Check_Expression (Expr : Node_Id) is
- begin
- if not Is_Trivial_Boolean (Expr) then
- Check_Function_Result (Expr);
-
- if not Mentions_Post_State (Expr) then
- if Pragma_Name (Prag) = Name_Contract_Cases then
- Error_Msg_N
- ("contract case refers only to pre-state?T?", Expr);
- else
- Error_Msg_N
- ("postcondition refers only to pre-state?T?", Prag);
- end if;
- end if;
- end if;
- end Check_Expression;
-
- ------------------------
- -- Is_Function_Result --
- ------------------------
-
- function Is_Function_Result (N : Node_Id) return Traverse_Result is
- begin
- if Nkind (N) = N_Attribute_Reference
- and then Attribute_Name (N) = Name_Result
- then
- Result_Seen := True;
- return Abandon;
-
- -- Continue the traversal
-
- else
- return OK;
- end if;
- end Is_Function_Result;
-
- ------------------------
- -- Is_Trivial_Boolean --
- ------------------------
-
- function Is_Trivial_Boolean (N : Node_Id) return Boolean is
- begin
- return
- Comes_From_Source (N)
- and then Is_Entity_Name (N)
- and then (Entity (N) = Standard_True
- or else Entity (N) = Standard_False);
- end Is_Trivial_Boolean;
-
- -------------------------
- -- Mentions_Post_State --
- -------------------------
-
- function Mentions_Post_State (N : Node_Id) return Boolean is
- Post_State_Seen : Boolean := False;
-
- function Is_Post_State (N : Node_Id) return Traverse_Result;
- -- Attempt to find a construct that denotes a post-state. If this
- -- is the case, set flag Post_State_Seen.
-
- -------------------
- -- Is_Post_State --
- -------------------
-
- function Is_Post_State (N : Node_Id) return Traverse_Result is
- Ent : Entity_Id;
-
- begin
- if Nkind_In (N, N_Explicit_Dereference, N_Function_Call) then
- Post_State_Seen := True;
- return Abandon;
-
- elsif Nkind_In (N, N_Expanded_Name, N_Identifier) then
- Ent := Entity (N);
-
- if No (Ent) or else Ekind (Ent) in Assignable_Kind then
- Post_State_Seen := True;
- return Abandon;
- end if;
-
- elsif Nkind (N) = N_Attribute_Reference then
- if Attribute_Name (N) = Name_Old then
- return Skip;
- elsif Attribute_Name (N) = Name_Result then
- Post_State_Seen := True;
- return Abandon;
- end if;
- end if;
-
- return OK;
- end Is_Post_State;
-
- procedure Find_Post_State is new Traverse_Proc (Is_Post_State);
-
- -- Start of processing for Mentions_Post_State
-
- begin
- Find_Post_State (N);
- return Post_State_Seen;
- end Mentions_Post_State;
-
- -- Local variables
-
- Expr : constant Node_Id :=
- Expression (First (Pragma_Argument_Associations (Prag)));
- Nam : constant Name_Id := Pragma_Name (Prag);
- CCase : Node_Id;
-
- -- Start of processing for Check_Result_And_Post_State
-
- begin
- if No (Error_Nod) then
- Error_Nod := Prag;
- end if;
-
- -- Examine all consequences
-
- if Nam = Name_Contract_Cases then
- CCase := First (Component_Associations (Expr));
- while Present (CCase) loop
- Check_Expression (Expression (CCase));
-
- Next (CCase);
- end loop;
-
- -- Examine the expression of a postcondition
-
- else
- pragma Assert (Nam = Name_Postcondition);
- Check_Expression (Expr);
- end if;
- end Check_Result_And_Post_State;
-
- -- Local variables
-
- Items : constant Node_Id := Contract (Subp);
- Depends : Node_Id := Empty;
- Error_CCase : Node_Id := Empty;
- Error_Post : Node_Id := Empty;
- Global : Node_Id := Empty;
- Nam : Name_Id;
- Prag : Node_Id;
-
- -- Start of processing for Analyze_Subprogram_Contract
-
begin
if Present (Items) then
@@ -3620,7 +3445,8 @@
if Warn_On_Suspicious_Contract
and then Pragma_Name (Prag) = Name_Postcondition
then
- Check_Result_And_Post_State (Prag, Error_Post);
+ Post_Prag := Prag;
+ Check_Result_And_Post_State (Prag, Seen_In_Post);
end if;
Prag := Next_Pragma (Prag);
@@ -3642,7 +3468,8 @@
if Warn_On_Suspicious_Contract
and then not Error_Posted (Prag)
then
- Check_Result_And_Post_State (Prag, Error_CCase);
+ Case_Prag := Prag;
+ Check_Result_And_Post_State (Prag, Seen_In_Case);
end if;
else
@@ -3683,26 +3510,28 @@
end if;
end if;
- -- Emit an error when none of the postconditions or contract-cases
+ -- Emit an error when neither the postconditions nor the contract-cases
-- mention attribute 'Result in the context of a function.
if Warn_On_Suspicious_Contract
and then Ekind_In (Subp, E_Function, E_Generic_Function)
- and then not Result_Seen
then
- if Present (Error_Post) and then Present (Error_CCase) then
+ if Present (Case_Prag)
+ and then not Seen_In_Case
+ and then Present (Post_Prag)
+ and then not Seen_In_Post
+ then
Error_Msg_N
("neither function postcondition nor contract cases mention "
- & "result?T?", Error_Post);
+ & "result?T?", Post_Prag);
- elsif Present (Error_Post) then
+ elsif Present (Case_Prag) and then not Seen_In_Case then
Error_Msg_N
- ("function postcondition does not mention result?T?",
- Error_Post);
+ ("contract cases do not mention result?T?", Case_Prag);
- elsif Present (Error_CCase) then
+ elsif Present (Post_Prag) and then not Seen_In_Post then
Error_Msg_N
- ("contract cases do not mention result?T?", Error_CCase);
+ ("function postcondition does not mention result?T?", Post_Prag);
end if;
end if;
end Analyze_Subprogram_Contract;
