Merge pull request #2614 from chrisr-diffblue/is_zero_bitfield_support

Make exprt::is_zero() support bitfields

Author: Daniel Kroening

src/util/expr.cpp

@@ -176,9 +176,9 @@ bool exprt::is_zero() const
         CHECK_RETURN(false);
       return rat_value.is_zero();
     }
-    else if(type_id==ID_unsignedbv ||
-            type_id==ID_signedbv ||
-            type_id==ID_c_bool)
+    else if(
+      type_id == ID_unsignedbv || type_id == ID_signedbv ||
+      type_id == ID_c_bool || type_id == ID_c_bit_field)
     {
       return constant.value_is_zero_string();
     }

unit/Makefile

@@ -24,6 +24,7 @@ SRC += unit_tests.cpp \
        solvers/refinement/string_refinement/substitute_array_list.cpp \
        solvers/refinement/string_refinement/sparse_array.cpp \
        solvers/refinement/string_refinement/union_find_replace.cpp \
+       util/expr.cpp \
        util/expr_cast/expr_cast.cpp \
        util/graph.cpp \
        util/irep.cpp \

unit/util/expr.cpp

@@ -0,0 +1,39 @@
+/*******************************************************************\
+
+Module: Unit test for expr.h/expr.cpp
+
+Author: Diffblue Ltd
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+
+#include <util/arith_tools.h>
+#include <util/expr.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
+
+
+SCENARIO("bitfield-expr-is-zero", "[core][util][expr]")
+{
+  GIVEN("An exprt representing a bitfield constant of 3")
+  {
+    const exprt bitfield3 =
+      from_integer(mp_integer(3), c_bit_field_typet(signedbv_typet(32), 4));
+
+    THEN("is_zero() should be false")
+    {
+      REQUIRE_FALSE(bitfield3.is_zero());
+    }
+  }
+  GIVEN("An exprt representing a bitfield constant of 0")
+  {
+    const exprt bitfield0 =
+      from_integer(mp_integer(0), c_bit_field_typet(signedbv_typet(32), 4));
+
+    THEN("is_zero() should be true")
+    {
+      REQUIRE(bitfield0.is_zero());
+    }
+  }
+}