Skip to content

Commit 2422f5c

Browse files
committed
Use irep_idt() instead of ""
Constructing a dstringt from a C string requires a string table lookup, while the default constructor for a dstringt just zero-initialises an unsigned.
1 parent 9f6eb84 commit 2422f5c

22 files changed

+72
-64
lines changed

jbmc/src/java_bytecode/java_object_factory.cpp

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -290,9 +290,9 @@ void java_object_factoryt::gen_pointer_target_init(
290290
gen_nondet_init(
291291
assignments,
292292
init_expr,
293-
false, // is_sub
294-
"", // class_identifier
295-
false, // skip_classid
293+
false, // is_sub
294+
irep_idt(), // class_identifier
295+
false, // skip_classid
296296
lifetime,
297297
{}, // no override type
298298
depth + 1,
@@ -757,9 +757,9 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
757757
gen_nondet_init(
758758
assignments,
759759
new_symbol.symbol_expr(),
760-
false, // is_sub
761-
"", // class_identifier
762-
false, // skip_classid
760+
false, // is_sub
761+
irep_idt(), // class_identifier
762+
false, // skip_classid
763763
lifetime,
764764
{}, // no override_type
765765
depth,
@@ -1546,9 +1546,9 @@ exprt object_factory(
15461546
state.gen_nondet_init(
15471547
assignments,
15481548
object,
1549-
false, // is_sub
1550-
"", // class_identifier
1551-
false, // skip_classid
1549+
false, // is_sub
1550+
irep_idt(), // class_identifier
1551+
false, // skip_classid
15521552
lifetime,
15531553
{}, // no override_type
15541554
1, // initial depth
@@ -1617,8 +1617,8 @@ void gen_nondet_init(
16171617
state.gen_nondet_init(
16181618
assignments,
16191619
expr,
1620-
false, // is_sub
1621-
"", // class_identifier
1620+
false, // is_sub
1621+
irep_idt(), // class_identifier
16221622
skip_classid,
16231623
lifetime,
16241624
{}, // no override_type

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,7 @@ static irep_idt get_tag(const typet &type)
4242
else if(type.id() == ID_struct)
4343
return irep_idt("java::" + id2string(to_struct_type(type).get_tag()));
4444
else
45-
return "";
45+
return irep_idt();
4646
}
4747

4848
/// \param type: a type

src/analyses/ai.h

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -157,7 +157,7 @@ class ai_baset
157157
const goto_functionst::goto_functiont &goto_function,
158158
std::ostream &out) const
159159
{
160-
output(ns, "", goto_function.body, out);
160+
output(ns, irep_idt(), goto_function.body, out);
161161
}
162162

163163
/// Output the abstract states for the whole program as JSON
@@ -178,15 +178,15 @@ class ai_baset
178178
const namespacet &ns,
179179
const goto_programt &goto_program) const
180180
{
181-
return output_json(ns, "", goto_program);
181+
return output_json(ns, irep_idt(), goto_program);
182182
}
183183

184184
/// Output the abstract states for a single function as JSON
185185
jsont output_json(
186186
const namespacet &ns,
187187
const goto_functionst::goto_functiont &goto_function) const
188188
{
189-
return output_json(ns, "", goto_function.body);
189+
return output_json(ns, irep_idt(), goto_function.body);
190190
}
191191

192192
/// Output the abstract states for the whole program as XML
@@ -207,15 +207,15 @@ class ai_baset
207207
const namespacet &ns,
208208
const goto_programt &goto_program) const
209209
{
210-
return output_xml(ns, "", goto_program);
210+
return output_xml(ns, irep_idt(), goto_program);
211211
}
212212

213213
/// Output the abstract states for a single function as XML
214214
xmlt output_xml(
215215
const namespacet &ns,
216216
const goto_functionst::goto_functiont &goto_function) const
217217
{
218-
return output_xml(ns, "", goto_function.body);
218+
return output_xml(ns, irep_idt(), goto_function.body);
219219
}
220220

221221
protected:

src/analyses/goto_rw.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -665,7 +665,7 @@ void guarded_range_domaint::output(
665665
out << itr->first << ":" << itr->second.first;
666666
// we don't know what mode (language) we are in, so we rely on the default
667667
// language to be reasonable for from_expr
668-
out << " if " << from_expr(ns, "", itr->second.second);
668+
out << " if " << from_expr(ns, irep_idt(), itr->second.second);
669669
}
670670
out << "]";
671671
}

src/analyses/invariant_set.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -137,7 +137,7 @@ std::string inv_object_storet::build_string(const exprt &expr) const
137137
// we don't know what mode (language) we are in, so we rely on the default
138138
// language to be reasonable for from_expr
139139
if(is_constant_address(expr))
140-
return from_expr(ns, "", expr);
140+
return from_expr(ns, irep_idt(), expr);
141141

142142
if(expr.id()==ID_member)
143143
{
@@ -399,8 +399,8 @@ void invariant_sett::strengthen_rec(const exprt &expr)
399399
throw "non-Boolean argument to strengthen()";
400400

401401
#if 0
402-
std::cout << "S: " << from_expr(*ns, "", expr) << '\n';
403-
#endif
402+
std::cout << "S: " << from_expr(*ns, irep_idt(), expr) << '\n';
403+
#endif
404404

405405
if(is_false)
406406
{
@@ -602,8 +602,8 @@ tvt invariant_sett::implies_rec(const exprt &expr) const
602602
throw "implies: non-Boolean expression";
603603

604604
#if 0
605-
std::cout << "I: " << from_expr(*ns, "", expr) << '\n';
606-
#endif
605+
std::cout << "I: " << from_expr(*ns, irep_idt(), expr) << '\n';
606+
#endif
607607

608608
if(is_false) // can't get any stronger
609609
return tvt(true);

src/analyses/local_bitvector_analysis.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -349,7 +349,7 @@ void local_bitvector_analysist::output(
349349
}
350350

351351
out << "\n";
352-
goto_function.body.output_instruction(ns, "", out, *i_it);
352+
goto_function.body.output_instruction(ns, irep_idt(), out, *i_it);
353353
out << "\n";
354354

355355
l++;

src/analyses/local_may_alias.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -470,7 +470,7 @@ void local_may_aliast::output(
470470
}
471471

472472
out << "\n";
473-
goto_function.body.output_instruction(ns, "", out, *i_it);
473+
goto_function.body.output_instruction(ns, irep_idt(), out, *i_it);
474474
out << "\n";
475475

476476
l++;

src/analyses/local_safe_pointers.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -205,7 +205,7 @@ void local_safe_pointerst::output(
205205
}
206206

207207
out << '\n';
208-
goto_program.output_instruction(ns, "", out, *i_it);
208+
goto_program.output_instruction(ns, irep_idt(), out, *i_it);
209209
out << '\n';
210210
}
211211
}
@@ -252,7 +252,7 @@ void local_safe_pointerst::output_safe_dereferences(
252252
}
253253

254254
out << '\n';
255-
goto_program.output_instruction(ns, "", out, *i_it);
255+
goto_program.output_instruction(ns, irep_idt(), out, *i_it);
256256
out << '\n';
257257
}
258258
}

src/analyses/static_analysis.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -155,7 +155,7 @@ class static_analysis_baset
155155
const goto_programt &goto_program,
156156
std::ostream &out) const
157157
{
158-
output(goto_program, "", out);
158+
output(goto_program, irep_idt(), out);
159159
}
160160

161161
virtual bool has_location(locationt l) const=0;

src/ansi-c/c_preprocess.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -199,9 +199,9 @@ static void error_parse_line(
199199
if(state==2)
200200
{
201201
saved_error_location.set_file(file);
202-
saved_error_location.set_function("");
202+
saved_error_location.set_function(irep_idt());
203203
saved_error_location.set_line(line_no);
204-
saved_error_location.set_column("");
204+
saved_error_location.set_column(irep_idt());
205205
}
206206
}
207207

0 commit comments

Comments
 (0)