From 836a25968eb79ca7f78ebde0ebdcf57bb19a654a Mon Sep 17 00:00:00 2001
From: Tobias Reiher <reiher@componolit.com>
Date: Wed, 1 Jul 2020 11:32:08 +0200
Subject: [PATCH] Prevent warning on conditionals in SPARK code

Ref. #312
---
 generated/rflx-ethernet.ads | 3 +--
 generated/rflx-ipv4.ads     | 3 +--
 rflx/model.py               | 3 +++
 3 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/generated/rflx-ethernet.ads b/generated/rflx-ethernet.ads
index 57b8d51b3..eae00b895 100644
--- 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
index e5f6291f4..a652cf5b7 100644
--- 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
index 2753c1d2d..49ab2f38d 100644
--- 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)