From: Yannick Moy <m...@adacore.com>
Warning on suspicious postcondition is not relevant if contract
Exceptional_Cases is present, or if contract Always_Terminates is
present with a non-statically True value, as in those cases the
postcondition can be used to indicate constraints on those pre-state
for which the subprogram might terminate normally.
gcc/ada/
* sem_util.adb (Check_Result_And_Post_State): Do not warn in cases
where the warning could be spurious.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/sem_util.adb | 32 ++++++++++++++++++++++++++++++++
1 file changed, 32 insertions(+)
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 3a64047d45c..1729a2addd8 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -4566,6 +4566,38 @@ package body Sem_Util is
elsif No (Items) then
return;
+
+ -- If the subprogram has a contract Exceptional_Cases, it is often
+ -- useful to refer only to the pre-state in the postcondition, to
+ -- indicate when the subprogram might terminate normally.
+
+ elsif Present (Get_Pragma (Subp_Id, Pragma_Exceptional_Cases)) then
+ return;
+
+ -- Same if the subprogram has a contract Always_Terminates => Cond,
+ -- where Cond is not syntactically True.
+
+ else
+ declare
+ Prag : constant Node_Id :=
+ Get_Pragma (Subp_Id, Pragma_Always_Terminates);
+ begin
+ if Present (Prag)
+ and then Present (Pragma_Argument_Associations (Prag))
+ then
+ declare
+ Cond : constant Node_Id :=
+ Get_Pragma_Arg
+ (First (Pragma_Argument_Associations (Prag)));
+ begin
+ if not Compile_Time_Known_Value (Cond)
+ or else not Is_True (Expr_Value (Cond))
+ then
+ return;
+ end if;
+ end;
+ end if;
+ end;
end if;
-- Examine all postconditions for attribute 'Result and a post-state
--
2.40.0
