Suppress inevitable proof warnings

Ref. #1131
AdaCore · Aug 19, 2022 · 4b542d8 · 4b542d8
1 parent 97775c3
commit 4b542d8
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 0 deletions.
diff --git a/rflx/templates/rflx_generic_types.ads b/rflx/templates/rflx_generic_types.ads
@@ -185,12 +185,16 @@ is
 
    procedure Free is new Ada.Unchecked_Deallocation (Object => Bytes, Name => Bytes_Ptr);
 
+   pragma Warnings (Off, "precondition is always False");
+
    function Unreachable return Boolean is (False) with Pre => False;
 
    function Unreachable return Bit_Length is (0) with Pre => False;
 
    function Unreachable return Length is (0) with Pre => False;
 
+   pragma Warnings (On, "precondition is always False");
+
    procedure Lemma_Size (Val : Base_Integer; Size : Positive) renames {prefix}RFLX_Arithmetic.Lemma_Size;
 
 end {prefix}RFLX_Generic_Types;
diff --git a/tests/integration/shared/generated/rflx-rflx_generic_types.ads b/tests/integration/shared/generated/rflx-rflx_generic_types.ads
@@ -185,12 +185,16 @@ is
 
    procedure Free is new Ada.Unchecked_Deallocation (Object => Bytes, Name => Bytes_Ptr);
 
+   pragma Warnings (Off, "precondition is always False");
+
    function Unreachable return Boolean is (False) with Pre => False;
 
    function Unreachable return Bit_Length is (0) with Pre => False;
 
    function Unreachable return Length is (0) with Pre => False;
 
+   pragma Warnings (On, "precondition is always False");
+
    procedure Lemma_Size (Val : Base_Integer; Size : Positive) renames RFLX.RFLX_Arithmetic.Lemma_Size;
 
 end RFLX.RFLX_Generic_Types;
diff --git a/tests/spark/generated/rflx-rflx_generic_types.ads b/tests/spark/generated/rflx-rflx_generic_types.ads
@@ -185,12 +185,16 @@ is
 
    procedure Free is new Ada.Unchecked_Deallocation (Object => Bytes, Name => Bytes_Ptr);
 
+   pragma Warnings (Off, "precondition is always False");
+
    function Unreachable return Boolean is (False) with Pre => False;
 
    function Unreachable return Bit_Length is (0) with Pre => False;
 
    function Unreachable return Length is (0) with Pre => False;
 
+   pragma Warnings (On, "precondition is always False");
+
    procedure Lemma_Size (Val : Base_Integer; Size : Positive) renames RFLX.RFLX_Arithmetic.Lemma_Size;
 
 end RFLX.RFLX_Generic_Types;