Suppress false warnings about always False precondition

Ref. Componolit/Workarounds#31
AdaCore · Jan 15, 2021 · 0b75e0c · 0b75e0c
1 parent 2bc3465
commit 0b75e0c
Show file tree

Hide file tree

Showing 26 changed files with 116 additions and 10 deletions.
diff --git a/rflx/generator/generator.py b/rflx/generator/generator.py
@@ -1267,6 +1267,8 @@ def __create_successor_function(message: Message) -> UnitPart:
         return UnitPart(
             [],
             [
+                # WORKAROUND: Componolit/Workarounds#31
+                Pragma("Warnings", [Variable("Off"), String("precondition is always False")]),
                 ExpressionFunctionDeclaration(
                     specification,
                     Case(
@@ -1299,7 +1301,8 @@ def __create_successor_function(message: Message) -> UnitPart:
                             )
                         )
                     ],
-                )
+                ),
+                Pragma("Warnings", [Variable("On"), String("precondition is always False")]),
             ],
         )
 

diff --git a/rflx/generator/parser.py b/rflx/generator/parser.py
@@ -30,13 +30,15 @@
     Or,
     Parameter,
     Postcondition,
+    Pragma,
     PragmaStatement,
     Precondition,
     ProcedureSpecification,
     Result,
     ReturnStatement,
     Selected,
     Slice,
+    String,
     Subprogram,
     SubprogramBody,
     SubprogramDeclaration,
@@ -652,15 +654,20 @@ def result(field: Field) -> Expr:
 
         return UnitPart(
             [
-                SubprogramDeclaration(
-                    specification(f, t),
-                    [
-                        Precondition(
-                            Call("Valid", [Variable("Ctx"), Variable(f.affixed_name)]),
-                        )
-                    ],
-                )
-                for f, t in scalar_fields.items()
+                # WORKAROUND: Componolit/Workarounds#31
+                Pragma("Warnings", [Variable("Off"), String("precondition is always False")]),
+                *[
+                    SubprogramDeclaration(
+                        specification(f, t),
+                        [
+                            Precondition(
+                                Call("Valid", [Variable("Ctx"), Variable(f.affixed_name)]),
+                            )
+                        ],
+                    )
+                    for f, t in scalar_fields.items()
+                ],
+                Pragma("Warnings", [Variable("On"), String("precondition is always False")]),
             ],
             [
                 ExpressionFunctionDeclaration(specification(f, t), result(f))

diff --git a/tests/spark/generated/rflx-arrays-generic_array_size_defined_by_message_size.adb b/tests/spark/generated/rflx-arrays-generic_array_size_defined_by_message_size.adb
@@ -99,6 +99,8 @@ is
           when others =>
              Ctx.Cursors (Fld).Predecessor));
 
+   pragma Warnings (Off, "precondition is always False");
+
    function Successor (Ctx : Context; Fld : Field) return Virtual_Field is
      ((case Fld is
           when F_Header =>
@@ -111,6 +113,8 @@ is
        and Structural_Valid (Ctx, Fld)
        and Valid_Predecessor (Ctx, Fld);
 
+   pragma Warnings (On, "precondition is always False");
+
    function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean is
      ((case Fld is
           when F_Initial =>

diff --git a/tests/spark/generated/rflx-arrays-generic_array_size_defined_by_message_size.ads b/tests/spark/generated/rflx-arrays-generic_array_size_defined_by_message_size.ads
@@ -189,10 +189,14 @@ is
 
    function Incomplete_Message (Ctx : Context) return Boolean;
 
+   pragma Warnings (Off, "precondition is always False");
+
    function Get_Header (Ctx : Context) return RFLX.Arrays.Enumeration with
      Pre =>
        Valid (Ctx, F_Header);
 
+   pragma Warnings (On, "precondition is always False");
+
    generic
       with procedure Process_Vector (Vector : Types.Bytes);
    procedure Get_Vector (Ctx : Context) with

diff --git a/tests/spark/generated/rflx-arrays-generic_inner_message.adb b/tests/spark/generated/rflx-arrays-generic_inner_message.adb
@@ -99,6 +99,8 @@ is
           when others =>
              Ctx.Cursors (Fld).Predecessor));
 
+   pragma Warnings (Off, "precondition is always False");
+
    function Successor (Ctx : Context; Fld : Field) return Virtual_Field is
      ((case Fld is
           when F_Length =>
@@ -111,6 +113,8 @@ is
        and Structural_Valid (Ctx, Fld)
        and Valid_Predecessor (Ctx, Fld);
 
+   pragma Warnings (On, "precondition is always False");
+
    function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean is
      ((case Fld is
           when F_Initial =>

diff --git a/tests/spark/generated/rflx-arrays-generic_inner_message.ads b/tests/spark/generated/rflx-arrays-generic_inner_message.ads
@@ -187,10 +187,14 @@ is
 
    function Incomplete_Message (Ctx : Context) return Boolean;
 
+   pragma Warnings (Off, "precondition is always False");
+
    function Get_Length (Ctx : Context) return RFLX.Arrays.Length with
      Pre =>
        Valid (Ctx, F_Length);
 
+   pragma Warnings (On, "precondition is always False");
+
    generic
       with procedure Process_Payload (Payload : Types.Bytes);
    procedure Get_Payload (Ctx : Context) with

diff --git a/tests/spark/generated/rflx-arrays-generic_message.adb b/tests/spark/generated/rflx-arrays-generic_message.adb
@@ -159,6 +159,8 @@ is
           when others =>
              Ctx.Cursors (Fld).Predecessor));
 
+   pragma Warnings (Off, "precondition is always False");
+
    function Successor (Ctx : Context; Fld : Field) return Virtual_Field is
      ((case Fld is
           when F_Length =>
@@ -177,6 +179,8 @@ is
        and Structural_Valid (Ctx, Fld)
        and Valid_Predecessor (Ctx, Fld);
 
+   pragma Warnings (On, "precondition is always False");
+
    function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean is
      ((case Fld is
           when F_Initial =>

diff --git a/tests/spark/generated/rflx-arrays-generic_message.ads b/tests/spark/generated/rflx-arrays-generic_message.ads
@@ -192,10 +192,14 @@ is
 
    function Incomplete_Message (Ctx : Context) return Boolean;
 
+   pragma Warnings (Off, "precondition is always False");
+
    function Get_Length (Ctx : Context) return RFLX.Arrays.Length with
      Pre =>
        Valid (Ctx, F_Length);
 
+   pragma Warnings (On, "precondition is always False");
+
    generic
       with procedure Process_Modular_Vector (Modular_Vector : Types.Bytes);
    procedure Get_Modular_Vector (Ctx : Context) with

diff --git a/tests/spark/generated/rflx-arrays-generic_messages_message.adb b/tests/spark/generated/rflx-arrays-generic_messages_message.adb
@@ -99,6 +99,8 @@ is
           when others =>
              Ctx.Cursors (Fld).Predecessor));
 
+   pragma Warnings (Off, "precondition is always False");
+
    function Successor (Ctx : Context; Fld : Field) return Virtual_Field is
      ((case Fld is
           when F_Length =>
@@ -111,6 +113,8 @@ is
        and Structural_Valid (Ctx, Fld)
        and Valid_Predecessor (Ctx, Fld);
 
+   pragma Warnings (On, "precondition is always False");
+
    function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean is
      ((case Fld is
           when F_Initial =>

diff --git a/tests/spark/generated/rflx-arrays-generic_messages_message.ads b/tests/spark/generated/rflx-arrays-generic_messages_message.ads
@@ -189,10 +189,14 @@ is
 
    function Incomplete_Message (Ctx : Context) return Boolean;
 
+   pragma Warnings (Off, "precondition is always False");
+
    function Get_Length (Ctx : Context) return RFLX.Arrays.Length with
      Pre =>
        Valid (Ctx, F_Length);
 
+   pragma Warnings (On, "precondition is always False");
+
    generic
       with procedure Process_Messages (Messages : Types.Bytes);
    procedure Get_Messages (Ctx : Context) with

diff --git a/tests/spark/generated/rflx-enumeration-generic_message.adb b/tests/spark/generated/rflx-enumeration-generic_message.adb
@@ -75,6 +75,8 @@ is
           when others =>
              Ctx.Cursors (Fld).Predecessor));
 
+   pragma Warnings (Off, "precondition is always False");
+
    function Successor (Ctx : Context; Fld : Field) return Virtual_Field is
      ((case Fld is
           when F_Priority =>
@@ -85,6 +87,8 @@ is
        and Structural_Valid (Ctx, Fld)
        and Valid_Predecessor (Ctx, Fld);
 
+   pragma Warnings (On, "precondition is always False");
+
    function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean is
      ((case Fld is
           when F_Initial =>

diff --git a/tests/spark/generated/rflx-enumeration-generic_message.ads b/tests/spark/generated/rflx-enumeration-generic_message.ads
@@ -182,10 +182,14 @@ is
 
    function Incomplete_Message (Ctx : Context) return Boolean;
 
+   pragma Warnings (Off, "precondition is always False");
+
    function Get_Priority (Ctx : Context) return RFLX.Enumeration.Priority with
      Pre =>
        Valid (Ctx, F_Priority);
 
+   pragma Warnings (On, "precondition is always False");
+
    procedure Set_Priority (Ctx : in out Context; Val : RFLX.Enumeration.Priority_Enum) with
      Pre =>
        not Ctx'Constrained

diff --git a/tests/spark/generated/rflx-ethernet-generic_frame.adb b/tests/spark/generated/rflx-ethernet-generic_frame.adb
@@ -236,6 +236,8 @@ is
           when others =>
              Ctx.Cursors (Fld).Predecessor));
 
+   pragma Warnings (Off, "precondition is always False");
+
    function Successor (Ctx : Context; Fld : Field) return Virtual_Field is
      ((case Fld is
           when F_Destination =>
@@ -282,6 +284,8 @@ is
        and Structural_Valid (Ctx, Fld)
        and Valid_Predecessor (Ctx, Fld);
 
+   pragma Warnings (On, "precondition is always False");
+
    function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean is
      ((case Fld is
           when F_Initial =>

diff --git a/tests/spark/generated/rflx-ethernet-generic_frame.ads b/tests/spark/generated/rflx-ethernet-generic_frame.ads
@@ -197,6 +197,8 @@ is
 
    function Incomplete_Message (Ctx : Context) return Boolean;
 
+   pragma Warnings (Off, "precondition is always False");
+
    function Get_Destination (Ctx : Context) return RFLX.Ethernet.Address with
      Pre =>
        Valid (Ctx, F_Destination);
@@ -221,6 +223,8 @@ is
      Pre =>
        Valid (Ctx, F_Type_Length);
 
+   pragma Warnings (On, "precondition is always False");
+
    generic
       with procedure Process_Payload (Payload : Types.Bytes);
    procedure Get_Payload (Ctx : Context) with

diff --git a/tests/spark/generated/rflx-expression-generic_message.adb b/tests/spark/generated/rflx-expression-generic_message.adb
@@ -77,6 +77,8 @@ is
           when others =>
              Ctx.Cursors (Fld).Predecessor));
 
+   pragma Warnings (Off, "precondition is always False");
+
    function Successor (Ctx : Context; Fld : Field) return Virtual_Field is
      ((case Fld is
           when F_Payload =>
@@ -92,6 +94,8 @@ is
        and Structural_Valid (Ctx, Fld)
        and Valid_Predecessor (Ctx, Fld);
 
+   pragma Warnings (On, "precondition is always False");
+
    function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean is
      ((case Fld is
           when F_Initial =>

diff --git a/tests/spark/generated/rflx-expression-generic_message.ads b/tests/spark/generated/rflx-expression-generic_message.ads
@@ -185,6 +185,10 @@ is
 
    function Incomplete_Message (Ctx : Context) return Boolean;
 
+   pragma Warnings (Off, "precondition is always False");
+
+   pragma Warnings (On, "precondition is always False");
+
    generic
       with procedure Process_Payload (Payload : Types.Bytes);
    procedure Get_Payload (Ctx : Context) with

diff --git a/tests/spark/generated/rflx-icmp-generic_message.adb b/tests/spark/generated/rflx-icmp-generic_message.adb
@@ -466,6 +466,8 @@ is
           when others =>
              Ctx.Cursors (Fld).Predecessor));
 
+   pragma Warnings (Off, "precondition is always False");
+
    function Successor (Ctx : Context; Fld : Field) return Virtual_Field is
      ((case Fld is
           when F_Tag =>
@@ -564,6 +566,8 @@ is
        and Structural_Valid (Ctx, Fld)
        and Valid_Predecessor (Ctx, Fld);
 
+   pragma Warnings (On, "precondition is always False");
+
    function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean is
      ((case Fld is
           when F_Initial =>

diff --git a/tests/spark/generated/rflx-icmp-generic_message.ads b/tests/spark/generated/rflx-icmp-generic_message.ads
@@ -215,6 +215,8 @@ is
 
    function Incomplete_Message (Ctx : Context) return Boolean;
 
+   pragma Warnings (Off, "precondition is always False");
+
    function Get_Tag (Ctx : Context) return RFLX.ICMP.Tag with
      Pre =>
        Valid (Ctx, F_Tag);
@@ -275,6 +277,8 @@ is
      Pre =>
        Valid (Ctx, F_Transmit_Timestamp);
 
+   pragma Warnings (On, "precondition is always False");
+
    generic
       with procedure Process_Data (Data : Types.Bytes);
    procedure Get_Data (Ctx : Context) with

diff --git a/tests/spark/generated/rflx-ipv4-generic_option.adb b/tests/spark/generated/rflx-ipv4-generic_option.adb
@@ -202,6 +202,8 @@ is
           when others =>
              Ctx.Cursors (Fld).Predecessor));
 
+   pragma Warnings (Off, "precondition is always False");
+
    function Successor (Ctx : Context; Fld : Field) return Virtual_Field is
      ((case Fld is
           when F_Copied =>
@@ -246,6 +248,8 @@ is
        and Structural_Valid (Ctx, Fld)
        and Valid_Predecessor (Ctx, Fld);
 
+   pragma Warnings (On, "precondition is always False");
+
    function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean is
      ((case Fld is
           when F_Initial =>

diff --git a/tests/spark/generated/rflx-ipv4-generic_option.ads b/tests/spark/generated/rflx-ipv4-generic_option.ads
@@ -196,6 +196,8 @@ is
 
    function Incomplete_Message (Ctx : Context) return Boolean;
 
+   pragma Warnings (Off, "precondition is always False");
+
    function Get_Copied (Ctx : Context) return Boolean with
      Pre =>
        Valid (Ctx, F_Copied);
@@ -212,6 +214,8 @@ is
      Pre =>
        Valid (Ctx, F_Option_Length);
 
+   pragma Warnings (On, "precondition is always False");
+
    generic
       with procedure Process_Option_Data (Option_Data : Types.Bytes);
    procedure Get_Option_Data (Ctx : Context) with

diff --git a/tests/spark/generated/rflx-ipv4-generic_packet.adb b/tests/spark/generated/rflx-ipv4-generic_packet.adb
@@ -409,6 +409,8 @@ is
           when others =>
              Ctx.Cursors (Fld).Predecessor));
 
+   pragma Warnings (Off, "precondition is always False");
+
    function Successor (Ctx : Context; Fld : Field) return Virtual_Field is
      ((case Fld is
           when F_Version =>
@@ -461,6 +463,8 @@ is
        and Structural_Valid (Ctx, Fld)
        and Valid_Predecessor (Ctx, Fld);
 
+   pragma Warnings (On, "precondition is always False");
+
    function Valid_Predecessor (Ctx : Context; Fld : Virtual_Field) return Boolean is
      ((case Fld is
           when F_Initial =>