Prevent warning on conditionals in SPARK code

Ref. #312
AdaCore · Jul 1, 2020 · 836a259 · 836a259
1 parent 3fbddda
commit 836a259
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 4 deletions.
diff --git a/generated/rflx-ethernet.ads b/generated/rflx-ethernet.ads
@@ -85,8 +85,7 @@ is
    pragma Warnings (On, "precondition is * false");
 
    function Valid (Val : RFLX.Ethernet.TPID_Base) return Boolean is
-     (Val >= 16#8100#
-      and Val <= 16#8100#);
+     (Val = 16#8100#);
 
    function To_Base (Val : RFLX.Ethernet.TPID) return RFLX.Ethernet.TPID_Base is
      (RFLX.Ethernet.TPID_Base (Val));

diff --git a/generated/rflx-ipv4.ads b/generated/rflx-ipv4.ads
@@ -23,8 +23,7 @@ is
    pragma Warnings (On, "precondition is * false");
 
    function Valid (Val : RFLX.IPv4.Version_Base) return Boolean is
-     (Val >= 4
-      and Val <= 4);
+     (Val = 4);
 
    function To_Base (Val : RFLX.IPv4.Version) return RFLX.IPv4.Version_Base is
      (RFLX.IPv4.Version_Base (Val));

diff --git a/rflx/model.py b/rflx/model.py
@@ -261,6 +261,9 @@ def constraints(self, name: str, proof: bool = False) -> Sequence[Expr]:
                 Equal(Length(name), self.size, location=self.location),
             ]
 
+        if self.first.simplified() == self.last.simplified():
+            return [Equal(Variable(name), self.first)]
+
         c: Expr = TRUE
         if self.first.simplified() != self.base_first.simplified():
             c = GreaterEqual(Variable(name), self.first)