Skip to content

Commit 9986ea1

Browse files
Make exprt::is_zero() support bitfields
1 parent f6c34f2 commit 9986ea1

File tree

3 files changed

+42
-1
lines changed

3 files changed

+42
-1
lines changed

src/util/expr.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -178,7 +178,8 @@ bool exprt::is_zero() const
178178
}
179179
else if(type_id==ID_unsignedbv ||
180180
type_id==ID_signedbv ||
181-
type_id==ID_c_bool)
181+
type_id==ID_c_bool ||
182+
type_id==ID_c_bit_field)
182183
{
183184
return constant.value_is_zero_string();
184185
}

unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ SRC += unit_tests.cpp \
2424
solvers/refinement/string_refinement/substitute_array_list.cpp \
2525
solvers/refinement/string_refinement/sparse_array.cpp \
2626
solvers/refinement/string_refinement/union_find_replace.cpp \
27+
util/expr.cpp \
2728
util/expr_cast/expr_cast.cpp \
2829
util/graph.cpp \
2930
util/irep.cpp \

unit/util/expr.cpp

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
/*******************************************************************\
2+
3+
Module: Unit test for expr.h/expr.cpp
4+
5+
Author: Diffblue Ltd
6+
7+
\*******************************************************************/
8+
9+
#include <testing-utils/catch.hpp>
10+
11+
#include <util/arith_tools.h>
12+
#include <util/expr.h>
13+
#include <util/std_expr.h>
14+
#include <util/std_types.h>
15+
16+
17+
SCENARIO("bitfield-expr-is-zero", "[core][util][expr]")
18+
{
19+
GIVEN("An exprt representing a bitfield constant of 3")
20+
{
21+
const exprt bitfield3 =
22+
from_integer(mp_integer(3), c_bit_field_typet(signedbv_typet(32), 4));
23+
24+
THEN("is_zero() should be false")
25+
{
26+
REQUIRE_FALSE(bitfield3.is_zero());
27+
}
28+
}
29+
GIVEN("An exprt representing a bitfield constant of 0")
30+
{
31+
const exprt bitfield0 =
32+
from_integer(mp_integer(0), c_bit_field_typet(signedbv_typet(32), 4));
33+
34+
THEN("is_zero() should be true")
35+
{
36+
REQUIRE(bitfield0.is_zero());
37+
}
38+
}
39+
}

0 commit comments

Comments
 (0)