Make exprt::is_zero() support bitfields

chrisr-diffblue · chrisr-diffblue · commit 9986ea139e6b · 2018-07-25T17:15:27.000+01:00
diff --git a/src/util/expr.cpp b/src/util/expr.cpp
@@ -178,7 +178,8 @@ bool exprt::is_zero() const
     }
     else if(type_id==ID_unsignedbv ||
             type_id==ID_signedbv ||
-            type_id==ID_c_bool)
+            type_id==ID_c_bool ||
+            type_id==ID_c_bit_field)
     {
       return constant.value_is_zero_string();
     }
diff --git a/unit/Makefile b/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 \
diff --git a/unit/util/expr.cpp b/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());
+    }
+  }
+}

Original file line number	Diff line number	Diff line change
`@@ -178,7 +178,8 @@ bool exprt::is_zero() const`
`178`	`178`	`}`
`179`	`179`	`else if(type_id==ID_unsignedbv \|\|`
`180`	`180`	`type_id==ID_signedbv \|\|`
`181`		`- type_id==ID_c_bool)`
	`181`	`+ type_id==ID_c_bool \|\|`
	`182`	`+ type_id==ID_c_bit_field)`
`182`	`183`	`{`
`183`	`184`	`return constant.value_is_zero_string();`
`184`	`185`	`}`