+2014-01-20 Hristian Kirtchev <kirtchev@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.
+
+2014-01-20 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * exp_ch7.adb (Is_Subprogram_Call): New routine.
+ (Process_Transient_Objects): Make variable Must_Hook global with
+ respect to all locally declared subprograms. Search the context
+ for at least one subprogram call.
+ (Requires_Hooking): Removed.
+
+2014-01-20 Claire Dross <dross@adacore.com>
+
+ * a-cfdlli.ads a-cfhama.ads a-cfhase.ads a-cforma.ads
+ * a-cforse.ads a-cofove.ads: Add pragma Annotate (GNATprove,
+ External_Axiomatization);
+
2014-01-20 Robert Dewar <dewar@adacore.com>
* sem_attr.adb (Analyze_Attribute, case Loop_Entry): Allow
return Boolean is <>;
package Ada.Containers.Formal_Doubly_Linked_Lists is
+ pragma Annotate (GNATprove, External_Axiomatization);
pragma Pure;
type List (Capacity : Count_Type) is private;
with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Formal_Hashed_Maps is
+ pragma Annotate (GNATprove, External_Axiomatization);
pragma Pure;
type Map (Capacity : Count_Type; Modulus : Hash_Type) is private;
with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Formal_Hashed_Sets is
+ pragma Annotate (GNATprove, External_Axiomatization);
pragma Pure;
type Set (Capacity : Count_Type; Modulus : Hash_Type) is private;
with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Formal_Ordered_Maps is
+ pragma Annotate (GNATprove, External_Axiomatization);
pragma Pure;
function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Formal_Ordered_Sets is
+ pragma Annotate (GNATprove, External_Axiomatization);
pragma Pure;
function Equivalent_Elements (Left, Right : Element_Type) return Boolean;
with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Formal_Vectors is
+ pragma Annotate (GNATprove, External_Axiomatization);
pragma Pure;
subtype Extended_Index is Index_Type'Base
Last_Object : Node_Id;
Related_Node : Node_Id)
is
- function Requires_Hooking return Boolean;
- -- Determine whether the context requires transient variable export
- -- to the outer finalizer. This scenario arises when the context may
- -- raise an exception.
+ Must_Hook : Boolean := False;
+ -- Flag denoting whether the context requires transient variable
+ -- export to the outer finalizer.
- ----------------------
- -- Requires_Hooking --
- ----------------------
+ function Is_Subprogram_Call (N : Node_Id) return Traverse_Result;
+ -- Determine whether an arbitrary node denotes a subprogram call
- function Requires_Hooking return Boolean is
+ ------------------------
+ -- Is_Subprogram_Call --
+ ------------------------
+
+ function Is_Subprogram_Call (N : Node_Id) return Traverse_Result is
begin
- -- The context is either a procedure or function call or an object
- -- declaration initialized by a function call. Note that in the
- -- latter case, a function call that returns on the secondary
- -- stack is usually rewritten into something else. Its proper
- -- detection requires examination of the original initialization
- -- expression.
-
- return Nkind (N) in N_Subprogram_Call
- or else (Nkind (N) = N_Object_Declaration
- and then Nkind (Original_Node (Expression (N))) =
- N_Function_Call);
- end Requires_Hooking;
+ -- A regular procedure or function call
+
+ if Nkind (N) in N_Subprogram_Call then
+ Must_Hook := True;
+ return Abandon;
+
+ -- Detect a call to a function that returns on the secondary stack
+
+ elsif Nkind (N) = N_Object_Declaration
+ and then Nkind (Original_Node (Expression (N))) = N_Function_Call
+ then
+ Must_Hook := True;
+ return Abandon;
+
+ -- Keep searching
+
+ else
+ return OK;
+ end if;
+ end Is_Subprogram_Call;
+
+ procedure Detect_Subprogram_Call is
+ new Traverse_Proc (Is_Subprogram_Call);
-- Local variables
- Must_Hook : constant Boolean := Requires_Hooking;
Built : Boolean := False;
Desig_Typ : Entity_Id;
Fin_Block : Node_Id;
-- Start of processing for Process_Transient_Objects
begin
+ -- Search the context for at least one subprogram call. If found, the
+ -- machinery exports all transient objects to the enclosing finalizer
+ -- due to the possibility of abnormal call termination.
+
+ Detect_Subprogram_Call (N);
+
-- Examine all objects in the list First_Object .. Last_Object
Stmt := First_Object;
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;
+
+ if Arg /= Arg_Ens then
+ Error_Attr
+ ("% attribute misplaced inside test case", P);
+ end if;
+ end;
- elsif Get_Pragma_Id (Prag) = Pragma_Contract_Cases then
- declare
- Aggr : constant Node_Id :=
- Expression (First (Pragma_Argument_Associations (Prag)));
- Arg : Node_Id;
+ when Pragma_Contract_Cases =>
+ declare
+ Aggr : constant Node_Id :=
+ Expression
+ (First (Pragma_Argument_Associations (Prag)));
+ Arg : Node_Id;
- begin
- Arg := N;
- while Arg /= Prag and then Parent (Parent (Arg)) /= Aggr loop
- Arg := Parent (Arg);
- end loop;
+ 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;
- -- At this point, Parent (Arg) should be a component
- -- association. Attribute Result is only allowed in
- -- the expression part of this association.
+ when Pragma_Postcondition | Pragma_Refined_Post =>
+ null;
- if Nkind (Parent (Arg)) /= N_Component_Association
- or else Arg /= Expression (Parent (Arg))
- then
+ 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
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;
+
+ 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;
+
+ -- 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;
- 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;
- elsif Get_Pragma_Id (Prag) /= Pragma_Postcondition then
- Error_Attr
- ("% attribute can only appear in postcondition of function",
- P);
+ 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,
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);
---------------------------------
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).
-
- 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
+ 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;
begin
if Present (Items) then
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);
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
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;
-- 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);
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;
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 --
------------------------------
-- 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);
projects / thirdparty / gcc.git / commitdiff
