Skip to content

Commit c2813b7

Browse files
kroeningkroening
authored
Merge pull request #6542 from tautschnig/is_constant
Consistently use exprt::is_constant()
2 parents b3c456f + 5eddb4c commit c2813b7

File tree

75 files changed

+163
-192
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

75 files changed

+163
-192
lines changed

‎jbmc/src/java_bytecode/expr2java.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -427,7 +427,7 @@ std::string expr2javat::convert_with_precedence(
427427
{
428428
return '"' + MetaString(id2string(literal->value())) + '"';
429429
}
430-
else if(src.id()==ID_constant)
430+
else if(src.is_constant())
431431
return convert_constant(to_constant_expr(src), precedence=16);
432432
else
433433
return expr2ct::convert_with_precedence(src, precedence);

‎jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -1447,8 +1447,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
14471447
{
14481448
CHECK_RETURN(results.size() == 1);
14491449
DATA_INVARIANT(
1450-
arg0.id()==ID_constant,
1451-
"ipush argument expected to be constant");
1450+
arg0.is_constant(), "ipush argument expected to be constant");
14521451
results[0] = typecast_exprt::conditional_cast(arg0, java_int_type());
14531452
}
14541453
else if(bytecode == patternt("if_?cmp??"))

‎jbmc/src/java_bytecode/java_bytecode_language.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -581,7 +581,7 @@ static exprt get_ldc_result(
581581
else
582582
{
583583
INVARIANT(
584-
ldc_arg0.id() == ID_constant,
584+
ldc_arg0.is_constant(),
585585
"ldc argument should be constant, string literal or class literal");
586586
return ldc_arg0;
587587
}

‎jbmc/src/java_bytecode/java_trace_validation.cpp

+9-13
Original file line numberDiff line numberDiff line change
@@ -104,19 +104,15 @@ bool check_struct_structure(const struct_exprt &expr)
104104
{
105105
return false;
106106
}
107-
if(
108-
expr.operands().size() > 1 && std::any_of(
109-
++expr.operands().begin(),
110-
expr.operands().end(),
111-
[&](const exprt &operand) {
112-
return operand.id() != ID_constant &&
113-
operand.id() !=
114-
ID_annotated_pointer_constant;
115-
}))
116-
{
117-
return false;
118-
}
119-
return true;
107+
108+
return expr.operands().size() == 1 ||
109+
std::all_of(
110+
std::next(expr.operands().begin()),
111+
expr.operands().end(),
112+
[&](const exprt &operand) {
113+
return can_cast_expr<constant_exprt>(operand) ||
114+
can_cast_expr<annotated_pointer_constant_exprt>(operand);
115+
});
120116
}
121117

122118
bool check_address_structure(const address_of_exprt &address)

‎jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp

+2-4
Original file line numberDiff line numberDiff line change
@@ -33,9 +33,7 @@ exprt resolve_classid_test(
3333

3434
const auto &expr_binary = to_binary_expr(expr);
3535

36-
if(
37-
expr_binary.op0().id() == ID_constant &&
38-
expr_binary.op1().id() != ID_constant)
36+
if(expr_binary.op0().is_constant() && !expr_binary.op1().is_constant())
3937
{
4038
binary_exprt swapped = expr_binary;
4139
std::swap(swapped.op0(), swapped.op1());
@@ -46,7 +44,7 @@ exprt resolve_classid_test(
4644
expr_binary.op0().id() == ID_member &&
4745
to_member_expr(expr_binary.op0()).get_component_name() ==
4846
"@class_identifier" &&
49-
expr_binary.op1().id() == ID_constant &&
47+
expr_binary.op1().is_constant() &&
5048
expr_binary.op1().type().id() == ID_string)
5149
{
5250
binary_exprt resolved = expr_binary;

‎jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp

+4-3
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ void check_function_call(
2222
const irep_idt &function_name,
2323
const goto_programt::targetst &targets)
2424
{
25-
REQUIRE(eq_expr.op0().id() == ID_constant);
25+
REQUIRE(eq_expr.op0().is_constant());
2626
REQUIRE(eq_expr.op0().type().id() == ID_string);
2727
REQUIRE(to_constant_expr(eq_expr.op0()).get_value() == class_name);
2828

@@ -99,8 +99,9 @@ SCENARIO(
9999
equal_exprt eq_expr1 =
100100
to_equal_expr(disjunction.op1());
101101

102-
if(eq_expr0.op0().id() == ID_constant &&
103-
to_constant_expr(eq_expr0.op0()).get_value() == "java::O")
102+
if(
103+
eq_expr0.op0().is_constant() &&
104+
to_constant_expr(eq_expr0.op0()).get_value() == "java::O")
104105
{
105106
// Allow either order of the D and O comparisons:
106107
std::swap(eq_expr0, eq_expr1);

‎src/analyses/constant_propagator.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -777,7 +777,7 @@ void constant_propagator_ait::replace(
777777

778778
if(!constant_propagator_domaint::partial_evaluate(d.values, rhs, ns))
779779
{
780-
if(rhs.id() == ID_constant)
780+
if(rhs.is_constant())
781781
rhs.add_source_location() = it->assign_lhs().source_location();
782782
}
783783
}

‎src/analyses/interval_domain.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -272,7 +272,7 @@ void interval_domaint::assume_rec(
272272
<< from_expr(rhs) << "\n";
273273
#endif
274274

275-
if(lhs.id()==ID_symbol && rhs.id()==ID_constant)
275+
if(lhs.id() == ID_symbol && rhs.is_constant())
276276
{
277277
irep_idt lhs_identifier=to_symbol_expr(lhs).get_identifier();
278278

@@ -297,7 +297,7 @@ void interval_domaint::assume_rec(
297297
make_bottom();
298298
}
299299
}
300-
else if(lhs.id()==ID_constant && rhs.id()==ID_symbol)
300+
else if(lhs.is_constant() && rhs.id() == ID_symbol)
301301
{
302302
irep_idt rhs_identifier=to_symbol_expr(rhs).get_identifier();
303303

‎src/analyses/local_bitvector_analysis.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -113,7 +113,7 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
113113
const exprt &rhs,
114114
points_tot &loc_info_src)
115115
{
116-
if(rhs.id()==ID_constant)
116+
if(rhs.is_constant())
117117
{
118118
if(rhs.is_zero())
119119
return flagst::mk_null();

‎src/analyses/local_may_alias.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -169,7 +169,7 @@ void local_may_aliast::get_rec(
169169
const exprt &rhs,
170170
const loc_infot &loc_info_src) const
171171
{
172-
if(rhs.id()==ID_constant)
172+
if(rhs.is_constant())
173173
{
174174
if(rhs.is_zero())
175175
dest.insert(objects.number(exprt(ID_null_object)));

‎src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -181,7 +181,7 @@ void constant_pointer_abstract_objectt::output(
181181
{
182182
auto const &array_symbol = to_symbol_expr(array);
183183
out << array_symbol.get_identifier() << "[";
184-
if(array_index.index().id() == ID_constant)
184+
if(array_index.index().is_constant())
185185
out << to_constant_expr(array_index.index()).get_value();
186186
else
187187
out << "?";

‎src/analyses/variable-sensitivity/interval_abstract_value.cpp

+6-8
Original file line numberDiff line numberDiff line change
@@ -148,7 +148,7 @@ interval_from_x_gt_value(const exprt &value)
148148
static inline bool represents_interval(const exprt &expr)
149149
{
150150
const exprt &e = skip_typecast(expr);
151-
return (e.id() == ID_constant_interval || e.id() == ID_constant);
151+
return (e.id() == ID_constant_interval || e.is_constant());
152152
}
153153

154154
static inline constant_interval_exprt make_interval_expr(const exprt &expr)
@@ -159,7 +159,7 @@ static inline constant_interval_exprt make_interval_expr(const exprt &expr)
159159
{
160160
return to_constant_interval_expr(e);
161161
}
162-
else if(e.id() == ID_constant)
162+
else if(e.is_constant())
163163
{
164164
return constant_interval_exprt(e, e);
165165
}
@@ -201,8 +201,8 @@ static inline constant_interval_exprt interval_from_relation(const exprt &e)
201201
PRECONDITION(
202202
relation == ID_le || relation == ID_lt || relation == ID_ge ||
203203
relation == ID_gt || relation == ID_equal);
204-
PRECONDITION(lhs.id() == ID_constant || lhs.id() == ID_symbol);
205-
PRECONDITION(rhs.id() == ID_constant || rhs.id() == ID_symbol);
204+
PRECONDITION(lhs.is_constant() || lhs.id() == ID_symbol);
205+
PRECONDITION(rhs.is_constant() || rhs.id() == ID_symbol);
206206
PRECONDITION(lhs.id() != rhs.id());
207207

208208
const auto the_constant_part_of_the_relation =
@@ -334,8 +334,7 @@ void interval_abstract_valuet::output(
334334
else
335335
{
336336
INVARIANT(
337-
interval.get_lower().id() == ID_constant,
338-
"We only support constant limits");
337+
interval.get_lower().is_constant(), "We only support constant limits");
339338
lower_string =
340339
id2string(to_constant_expr(interval.get_lower()).get_value());
341340
}
@@ -347,8 +346,7 @@ void interval_abstract_valuet::output(
347346
else
348347
{
349348
INVARIANT(
350-
interval.get_upper().id() == ID_constant,
351-
"We only support constant limits");
349+
interval.get_upper().is_constant(), "We only support constant limits");
352350
upper_string =
353351
id2string(to_constant_expr(interval.get_upper()).get_value());
354352
}

‎src/ansi-c/c_nondet_symbol_factory.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -172,7 +172,7 @@ void symbol_factoryt::gen_nondet_array_init(
172172
{
173173
auto const &array_type = to_array_type(expr.type());
174174
const auto &size = array_type.size();
175-
PRECONDITION(size.id() == ID_constant);
175+
PRECONDITION(size.is_constant());
176176
auto const array_size = numeric_cast<mp_integer>(to_constant_expr(size));
177177
DATA_INVARIANT(
178178
array_size.has_value() && *array_size >= 0,

‎src/ansi-c/c_typecheck_expr.cpp

+2-3
Original file line numberDiff line numberDiff line change
@@ -176,7 +176,7 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
176176
{
177177
if(expr.id()==ID_side_effect)
178178
typecheck_expr_side_effect(to_side_effect_expr(expr));
179-
else if(expr.id()==ID_constant)
179+
else if(expr.is_constant())
180180
typecheck_expr_constant(expr);
181181
else if(expr.id()==ID_infinity)
182182
{
@@ -860,8 +860,7 @@ void c_typecheck_baset::typecheck_expr_symbol(exprt &expr)
860860
follow_macros(expr);
861861

862862
#if 0
863-
if(expr.id()==ID_constant &&
864-
!base_name.empty())
863+
if(expr.is_constant() && !base_name.empty())
865864
expr.set(ID_C_cformat, base_name);
866865
else
867866
#endif

‎src/ansi-c/c_typecheck_type.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -1294,8 +1294,7 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
12941294
else if(tmp_v.is_false())
12951295
value=0;
12961296
else if(
1297-
tmp_v.id() == ID_constant &&
1298-
!to_integer(to_constant_expr(tmp_v), value))
1297+
tmp_v.is_constant() && !to_integer(to_constant_expr(tmp_v), value))
12991298
{
13001299
}
13011300
else

‎src/ansi-c/expr2c.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -1273,7 +1273,7 @@ std::string expr2ct::convert_complex(
12731273
{
12741274
if(
12751275
src.operands().size() == 2 && to_binary_expr(src).op0().is_zero() &&
1276-
to_binary_expr(src).op1().id() == ID_constant)
1276+
to_binary_expr(src).op1().is_constant())
12771277
{
12781278
// This is believed to be gcc only; check if this is sensible
12791279
// in MSC mode.
@@ -3871,7 +3871,7 @@ std::string expr2ct::convert_with_precedence(
38713871
else if(src.id()==ID_code)
38723872
return convert_code(to_code(src));
38733873

3874-
else if(src.id()==ID_constant)
3874+
else if(src.is_constant())
38753875
return convert_constant(to_constant_expr(src), precedence);
38763876

38773877
else if(src.id() == ID_annotated_pointer_constant)

‎src/cpp/cpp_declarator_converter.cpp

+3-4
Original file line numberDiff line numberDiff line change
@@ -478,10 +478,9 @@ symbolt &cpp_declarator_convertert::convert_new_symbol(
478478
}
479479
else
480480
{
481-
symbol.is_lvalue =
482-
!is_reference(symbol.type) &&
483-
!(symbol.type.get_bool(ID_C_constant) && is_number(symbol.type) &&
484-
symbol.value.id() == ID_constant);
481+
symbol.is_lvalue = !is_reference(symbol.type) &&
482+
!(symbol.type.get_bool(ID_C_constant) &&
483+
is_number(symbol.type) && symbol.value.is_constant());
485484

486485
symbol.is_static_lifetime =
487486
!symbol.is_macro && !symbol.is_type &&

‎src/cpp/cpp_typecheck_compound_type.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -546,7 +546,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
546546
component.type().set(ID_C_virtual_name, virtual_name);
547547

548548
// Check if it is a pure virtual method
549-
if(value.is_not_nil() && value.id() == ID_constant)
549+
if(value.is_not_nil() && value.is_constant())
550550
{
551551
mp_integer i;
552552
to_integer(to_constant_expr(value), i);

‎src/cpp/cpp_typecheck_conversions.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -602,7 +602,7 @@ bool cpp_typecheckt::standard_conversion_pointer_to_member(
602602
if(expr.get_bool(ID_C_lvalue))
603603
return false;
604604

605-
if(expr.id() == ID_constant && is_null_pointer(to_constant_expr(expr)))
605+
if(expr.is_constant() && is_null_pointer(to_constant_expr(expr)))
606606
{
607607
new_expr = typecast_exprt::conditional_cast(expr, type);
608608
return true;

‎src/cpp/cpp_typecheck_expr.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -1150,7 +1150,7 @@ void cpp_typecheckt::typecheck_expr_member(
11501150

11511151
DATA_INVARIANT(
11521152
symbol_expr.id() == ID_symbol || symbol_expr.id() == ID_member ||
1153-
symbol_expr.id() == ID_constant,
1153+
symbol_expr.is_constant(),
11541154
"expression kind unexpected");
11551155

11561156
// If it is a symbol or a constant, just return it!
@@ -1188,7 +1188,7 @@ void cpp_typecheckt::typecheck_expr_member(
11881188
expr=symbol_expr;
11891189
return;
11901190
}
1191-
else if(symbol_expr.id()==ID_constant)
1191+
else if(symbol_expr.is_constant())
11921192
{
11931193
expr=symbol_expr;
11941194
return;

‎src/cpp/cpp_typecheck_resolve.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -360,7 +360,7 @@ exprt cpp_typecheck_resolvet::convert_identifier(
360360

361361
if(
362362
constant && symbol.value.is_not_nil() && is_number(symbol.type) &&
363-
symbol.value.id() == ID_constant)
363+
symbol.value.is_constant())
364364
{
365365
e=symbol.value;
366366
}

‎src/cprover/bv_pointers_wide.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -268,7 +268,7 @@ optionalt<bvt> bv_pointers_widet::convert_address_of_rec(const exprt &expr)
268268
return std::move(bv);
269269
}
270270
else if(
271-
expr.id() == ID_constant || expr.id() == ID_string_constant ||
271+
expr.is_constant() || expr.id() == ID_string_constant ||
272272
expr.id() == ID_array)
273273
{ // constant
274274
return add_addr(expr);
@@ -382,7 +382,7 @@ bvt bv_pointers_widet::convert_pointer_type(const exprt &expr)
382382
const auto &object_address_expr = to_object_address_expr(expr);
383383
return add_addr(object_address_expr.object_expr());
384384
}
385-
else if(expr.id() == ID_constant)
385+
else if(expr.is_constant())
386386
{
387387
const constant_exprt &c = to_constant_expr(expr);
388388

‎src/cprover/simplify_state_expr.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -628,7 +628,7 @@ static bool is_one(const exprt &src)
628628
{
629629
if(src.id() == ID_typecast)
630630
return is_one(to_typecast_expr(src).op());
631-
else if(src.id() == ID_constant)
631+
else if(src.is_constant())
632632
{
633633
auto value_opt = numeric_cast<mp_integer>(src);
634634
return value_opt.has_value() && *value_opt == 1;

‎src/goto-cc/linker_script_merge.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -164,8 +164,8 @@ linker_script_merget::linker_script_merget(
164164
.id() == ID_array &&
165165

166166
to_index_expr(to_address_of_expr(expr).object())
167-
.index()
168-
.id() == ID_constant &&
167+
.index()
168+
.is_constant() &&
169169
to_index_expr(to_address_of_expr(expr).object())
170170
.index()
171171
.type()

‎src/goto-instrument/accelerate/overflow_instrumenter.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -100,7 +100,7 @@ void overflow_instrumentert::overflow_expr(
100100
{
101101
const auto &typecast_expr = to_typecast_expr(expr);
102102

103-
if(typecast_expr.op().id() == ID_constant)
103+
if(typecast_expr.op().is_constant())
104104
return;
105105

106106
const typet &old_type = typecast_expr.op().type();

‎src/goto-instrument/accelerate/polynomial.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -136,7 +136,7 @@ void polynomialt::from_expr(const exprt &expr)
136136
mult(poly2);
137137
}
138138
}
139-
else if(expr.id()==ID_constant)
139+
else if(expr.is_constant())
140140
{
141141
monomialt monomial;
142142
monomial.coeff = numeric_cast_v<int>(to_constant_expr(expr));

‎src/goto-instrument/dump_c.cpp

+3-4
Original file line numberDiff line numberDiff line change
@@ -1389,7 +1389,7 @@ void dump_ct::cleanup_expr(exprt &expr)
13891389
}
13901390
// add a typecast for NULL
13911391
else if(
1392-
u.op().id() == ID_constant && is_null_pointer(to_constant_expr(u.op())) &&
1392+
u.op().is_constant() && is_null_pointer(to_constant_expr(u.op())) &&
13931393
to_pointer_type(u.op().type()).base_type().id() == ID_empty)
13941394
{
13951395
const struct_union_typet::componentt &comp=
@@ -1445,7 +1445,7 @@ void dump_ct::cleanup_expr(exprt &expr)
14451445

14461446
// add a typecast for NULL or 0
14471447
if(
1448-
argument.id() == ID_constant &&
1448+
argument.is_constant() &&
14491449
is_null_pointer(to_constant_expr(argument)))
14501450
{
14511451
const typet &comp_type=
@@ -1461,8 +1461,7 @@ void dump_ct::cleanup_expr(exprt &expr)
14611461
}
14621462
}
14631463
}
1464-
else if(expr.id()==ID_constant &&
1465-
expr.type().id()==ID_signedbv)
1464+
else if(expr.is_constant() && expr.type().id() == ID_signedbv)
14661465
{
14671466
#if 0
14681467
const irep_idt &cformat=expr.get(ID_C_cformat);

0 commit comments

Comments
 (0)