Skip to content

Commit

Permalink
Make exprt::is_zero() support bitfields
Browse files Browse the repository at this point in the history
  • Loading branch information
chrisr-diffblue committed Jul 25, 2018
1 parent f6c34f2 commit 38c9cb4
Show file tree
Hide file tree
Showing 3 changed files with 40 additions and 1 deletion.
3 changes: 2 additions & 1 deletion src/util/expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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();
}
Expand Down
1 change: 1 addition & 0 deletions unit/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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 \
Expand Down
37 changes: 37 additions & 0 deletions unit/util/expr.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
/*******************************************************************\
Module: Unit test for expr.h/expr.cpp
Author: Diffblue Ltd
\*******************************************************************/

#include <testing-utils/catch.hpp>

#include <util/expr.h>
#include <util/std_types.h>
#include <util/std_expr.h>
#include <util/arith_tools.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(!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());
}
}
}

0 comments on commit 38c9cb4

Please sign in to comment.