From dff98f76fb246e0a0d02ce13f2160c69168c3dc7 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Fri, 11 Feb 2022 09:02:42 +0100 Subject: [PATCH] [Ada] Remove useless pragma Warnings Off from runtime units GNAT does not issue a warning anymore on a postcondition of True (used here to prevent inining inside GNATprove for proof). gcc/ada/ * libgnat/s-valuei.ads: Remove pragma Warnings Off. * libgnat/s-valueu.ads: Same. * libgnat/s-valuti.ads: Same. --- gcc/ada/libgnat/s-valuei.ads | 2 -- gcc/ada/libgnat/s-valueu.ads | 2 -- gcc/ada/libgnat/s-valuti.ads | 2 -- 3 files changed, 6 deletions(-) diff --git a/gcc/ada/libgnat/s-valuei.ads b/gcc/ada/libgnat/s-valuei.ads index d2e857a..c5b4b8e 100644 --- a/gcc/ada/libgnat/s-valuei.ads +++ b/gcc/ada/libgnat/s-valuei.ads @@ -37,8 +37,6 @@ pragma Assertion_Policy (Pre => Ignore, Contract_Cases => Ignore, Ghost => Ignore, Subprogram_Variant => Ignore); -pragma Warnings (Off, "postcondition does not mention function result"); --- True postconditions are used to avoid inlining for GNATprove with System.Val_Util; use System.Val_Util; diff --git a/gcc/ada/libgnat/s-valueu.ads b/gcc/ada/libgnat/s-valueu.ads index 6245c47..1508b6e 100644 --- a/gcc/ada/libgnat/s-valueu.ads +++ b/gcc/ada/libgnat/s-valueu.ads @@ -43,8 +43,6 @@ pragma Assertion_Policy (Pre => Ignore, Contract_Cases => Ignore, Ghost => Ignore, Subprogram_Variant => Ignore); -pragma Warnings (Off, "postcondition does not mention function result"); --- True postconditions are used to avoid inlining for GNATprove with System.Val_Util; use System.Val_Util; diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads index db1051b..45a0b66 100644 --- a/gcc/ada/libgnat/s-valuti.ads +++ b/gcc/ada/libgnat/s-valuti.ads @@ -41,8 +41,6 @@ pragma Assertion_Policy (Pre => Ignore, Post => Ignore, Contract_Cases => Ignore, Ghost => Ignore); -pragma Warnings (Off, "postcondition does not mention function result"); --- True postconditions are used to avoid inlining for GNATprove with System.Case_Util; -- 2.7.4