Skip to content

Commit 497b7e3

Browse files
committed
Mark constant_exprt::value_is_zero_string protected
The value representation is an implementation detail. Callers should use methods at a higher level of abstraction.
1 parent 2212cd6 commit 497b7e3

File tree

4 files changed

+6
-6
lines changed

4 files changed

+6
-6
lines changed

src/goto-programs/json_expr.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ static exprt simplify_json_expr(const exprt &src)
5353
}
5454
else if(
5555
object.id() == ID_index && to_index_expr(object).index().is_constant() &&
56-
to_constant_expr(to_index_expr(object).index()).value_is_zero_string())
56+
to_constant_expr(to_index_expr(object).index()).is_zero())
5757
{
5858
// simplify expressions of the form &array[0]
5959
return simplify_json_expr(to_index_expr(object).array());

src/util/simplify_expr_int.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -777,7 +777,7 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr)
777777
}
778778
else if(
779779
it->is_constant() && it->type().id() == ID_bv &&
780-
to_constant_expr(*it).value_is_zero_string() &&
780+
*it == to_bv_type(it->type()).all_zeros_expr() &&
781781
new_expr.operands().size() > 1)
782782
{
783783
it = new_expr.operands().erase(it);

src/util/std_expr.h

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3005,8 +3005,6 @@ class constant_exprt : public nullary_exprt
30053005
set(ID_value, value);
30063006
}
30073007

3008-
bool value_is_zero_string() const;
3009-
30103008
/// Returns true if \p expr has a pointer type and a value NULL; it also
30113009
/// returns true when \p expr has value zero and NULL_is_zero is true; returns
30123010
/// false in all other cases.
@@ -3023,6 +3021,9 @@ class constant_exprt : public nullary_exprt
30233021
{
30243022
check(expr, vm);
30253023
}
3024+
3025+
protected:
3026+
bool value_is_zero_string() const;
30263027
};
30273028

30283029
template <>

unit/goto-symex/goto_symex_state.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -172,8 +172,7 @@ SCENARIO(
172172
const symbol_exprt object_symbol =
173173
to_symbol_expr(object_descriptor->object());
174174
REQUIRE(object_symbol.get_identifier() == "int_value!0");
175-
REQUIRE(to_constant_expr(object_descriptor->offset())
176-
.value_is_zero_string());
175+
REQUIRE(to_constant_expr(object_descriptor->offset()).is_zero());
177176
}
178177
THEN("The target equations are unchanged")
179178
{

0 commit comments

Comments
 (0)