Skip to content

Commit 970cc26

Browse files
authored
Merge pull request #6857 from diffblue/_code
instructiont::get_code -> code
2 parents ee860d4 + 66a5a42 commit 970cc26

32 files changed

+148
-145
lines changed

jbmc/src/java_bytecode/remove_exceptions.cpp

+4-4
Original file line numberDiff line numberDiff line change
@@ -234,7 +234,7 @@ void remove_exceptionst::instrument_exception_handler(
234234
{
235235
// retrieve the exception variable
236236
const exprt &thrown_exception_local =
237-
to_code_landingpad(instr_it->get_code()).catch_expr();
237+
to_code_landingpad(instr_it->code()).catch_expr();
238238

239239
const symbol_exprt thrown_global_symbol=
240240
get_inflight_exception_global();
@@ -407,7 +407,7 @@ bool remove_exceptionst::instrument_throw(
407407
PRECONDITION(instr_it->type() == THROW);
408408

409409
const exprt &exc_expr =
410-
uncaught_exceptions_domaint::get_exception_symbol(instr_it->get_code());
410+
uncaught_exceptions_domaint::get_exception_symbol(instr_it->code());
411411

412412
add_exception_dispatch_sequence(
413413
function_identifier, goto_program, instr_it, stack_catch, locals);
@@ -512,7 +512,7 @@ void remove_exceptionst::instrument_exceptions(
512512
// Is it a handler push/pop or catch landing-pad?
513513
else if(instr_it->type() == CATCH)
514514
{
515-
const irep_idt &statement = instr_it->get_code().get_statement();
515+
const irep_idt &statement = instr_it->code().get_statement();
516516
// Is it an exception landing pad (start of a catch block)?
517517
if(statement==ID_exception_landingpad)
518518
{
@@ -553,7 +553,7 @@ void remove_exceptionst::instrument_exceptions(
553553

554554
// copy targets
555555
const code_push_catcht::exception_listt &exception_list =
556-
to_code_push_catch(instr_it->get_code()).exception_list();
556+
to_code_push_catch(instr_it->code()).exception_list();
557557

558558
// The target list can be empty if `finish_catch_push_targets` found that
559559
// the targets were unreachable (in which case no exception can truly

jbmc/src/java_bytecode/remove_instanceof.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -242,8 +242,8 @@ bool remove_instanceoft::lower_instanceof(
242242
goto_programt::targett target)
243243
{
244244
if(
245-
target->is_target() && (contains_instanceof(target->get_code()) ||
246-
contains_instanceof(target->guard)))
245+
target->is_target() &&
246+
(contains_instanceof(target->code()) || contains_instanceof(target->guard)))
247247
{
248248
// If this is a branch target, add a skip beforehand so we can splice new
249249
// GOTO programs before the target instruction without inserting into the

jbmc/src/java_bytecode/replace_java_nondet.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -89,11 +89,11 @@ is_nondet_returning_object(const code_function_callt &function_call)
8989
static nondet_instruction_infot
9090
get_nondet_instruction_info(const goto_programt::const_targett &instr)
9191
{
92-
if(!(instr->is_function_call() && instr->get_code().id() == ID_code))
92+
if(!(instr->is_function_call() && instr->code().id() == ID_code))
9393
{
9494
return nondet_instruction_infot();
9595
}
96-
const auto &code = instr->get_code();
96+
const auto &code = instr->code();
9797
INVARIANT(
9898
code.get_statement() == ID_function_call,
9999
"function_call should have ID_function_call");

jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -79,8 +79,8 @@ SCENARIO(
7979
instrend = main_function.body.instructions.end();
8080
instrit != instrend; ++instrit)
8181
{
82-
for(auto it = instrit->get_code().depth_begin(),
83-
itend = instrit->get_code().depth_end();
82+
for(auto it = instrit->code().depth_begin(),
83+
itend = instrit->code().depth_end();
8484
it != itend;
8585
++it)
8686
{

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -93,7 +93,7 @@ void validate_nondets_converted(
9393
exprt target_expression =
9494
(inst.is_assign()
9595
? inst.assign_rhs()
96-
: inst.is_set_return_value() ? inst.return_value() : inst.get_code());
96+
: inst.is_set_return_value() ? inst.return_value() : inst.code());
9797

9898
if(
9999
const auto side_effect =

src/analyses/cfg_dominators.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -267,7 +267,7 @@ inline void dominators_pretty_print_node(
267267
const goto_programt::targett& target,
268268
std::ostream& out)
269269
{
270-
out << target->get_code().pretty();
270+
out << target->code().pretty();
271271
}
272272

273273
/// Print the result of the dominator computation

src/analyses/invariant_set_domain.cpp

+3-3
Original file line numberDiff line numberDiff line change
@@ -60,15 +60,15 @@ void invariant_set_domaint::transform(
6060

6161
case OTHER:
6262
if(from_l->get_other().is_not_nil())
63-
invariant_set.apply_code(from_l->get_code());
63+
invariant_set.apply_code(from_l->code());
6464
break;
6565

6666
case DECL:
67-
invariant_set.apply_code(from_l->get_code());
67+
invariant_set.apply_code(from_l->code());
6868
break;
6969

7070
case FUNCTION_CALL:
71-
invariant_set.apply_code(from_l->get_code());
71+
invariant_set.apply_code(from_l->code());
7272
break;
7373

7474
case START_THREAD:

src/analyses/uncaught_exceptions_analysis.cpp

+3-3
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,7 @@ void uncaught_exceptions_domaint::transform(
7171
{
7272
case THROW:
7373
{
74-
const exprt &exc_symbol = get_exception_symbol(instruction.get_code());
74+
const exprt &exc_symbol = get_exception_symbol(instruction.code());
7575
// retrieve the static type of the thrown exception
7676
const irep_idt &type_id =
7777
get_exception_type(to_pointer_type(exc_symbol.type()));
@@ -85,15 +85,15 @@ void uncaught_exceptions_domaint::transform(
8585
}
8686
case CATCH:
8787
{
88-
if(!instruction.get_code().has_operands())
88+
if(!instruction.code().has_operands())
8989
{
9090
if(!instruction.targets.empty()) // push
9191
{
9292
std::set<irep_idt> caught;
9393
stack_caught.push_back(caught);
9494
std::set<irep_idt> &last_caught=stack_caught.back();
9595
const irept::subt &exception_list =
96-
instruction.get_code().find(ID_exception_list).get_sub();
96+
instruction.code().find(ID_exception_list).get_sub();
9797

9898
for(const auto &exc : exception_list)
9999
{

src/goto-instrument/contracts/instrument_spec_assigns.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -1021,8 +1021,7 @@ void instrument_spec_assignst::instrument_call_statement(
10211021

10221022
if(callee_name == "malloc")
10231023
{
1024-
const auto &function_call =
1025-
to_code_function_call(instruction_it->get_code());
1024+
const auto &function_call = to_code_function_call(instruction_it->code());
10261025
if(function_call.lhs().is_not_nil())
10271026
{
10281027
// grab the returned pointer from malloc

src/goto-instrument/dot.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -160,7 +160,7 @@ void dott::write_dot_subgraph(
160160
it->is_assign() || it->is_decl() || it->is_set_return_value() ||
161161
it->is_other())
162162
{
163-
std::string t = from_expr(ns, function_id, it->get_code());
163+
std::string t = from_expr(ns, function_id, it->code());
164164
while(t[ t.size()-1 ]=='\n')
165165
t = t.substr(0, t.size()-1);
166166
tmp.str(escape(t));

src/goto-instrument/goto_instrument_parse_options.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -658,8 +658,8 @@ int goto_instrument_parse_optionst::doit()
658658
for(auto const &pair : goto_model.goto_functions.function_map)
659659
for(auto const &ins : pair.second.body.instructions)
660660
{
661-
if(ins.get_code().is_not_nil())
662-
log.status() << ins.get_code().pretty() << messaget::eom;
661+
if(ins.code().is_not_nil())
662+
log.status() << ins.code().pretty() << messaget::eom;
663663
if(ins.has_condition())
664664
{
665665
log.status() << "[guard] " << ins.condition().pretty()

src/goto-instrument/wmm/fence.cpp

+9-9
Original file line numberDiff line numberDiff line change
@@ -25,11 +25,11 @@ bool is_fence(
2525
"fence")
2626
/* if assembly-sensitive algorithms are not available */
2727
|| (instruction.is_other() &&
28-
instruction.get_code().get_statement() == ID_fence &&
29-
instruction.get_code().get_bool(ID_WWfence) &&
30-
instruction.get_code().get_bool(ID_WRfence) &&
31-
instruction.get_code().get_bool(ID_RWfence) &&
32-
instruction.get_code().get_bool(ID_RRfence));
28+
instruction.code().get_statement() == ID_fence &&
29+
instruction.code().get_bool(ID_WWfence) &&
30+
instruction.code().get_bool(ID_WRfence) &&
31+
instruction.code().get_bool(ID_RWfence) &&
32+
instruction.code().get_bool(ID_RRfence));
3333
}
3434

3535
bool is_lwfence(
@@ -41,8 +41,8 @@ bool is_lwfence(
4141
"lwfence")
4242
/* if assembly-sensitive algorithms are not available */
4343
|| (instruction.is_other() &&
44-
instruction.get_code().get_statement() == ID_fence &&
45-
instruction.get_code().get_bool(ID_WWfence) &&
46-
instruction.get_code().get_bool(ID_RWfence) &&
47-
instruction.get_code().get_bool(ID_RRfence));
44+
instruction.code().get_statement() == ID_fence &&
45+
instruction.code().get_bool(ID_WWfence) &&
46+
instruction.code().get_bool(ID_RWfence) &&
47+
instruction.code().get_bool(ID_RRfence));
4848
}

src/goto-instrument/wmm/goto2graph.cpp

+8-9
Original file line numberDiff line numberDiff line change
@@ -235,8 +235,7 @@ void instrumentert::cfg_visitort::visit_cfg_function(
235235
visit_cfg_skip(i_it);
236236
}
237237
else if(
238-
instruction.is_other() &&
239-
instruction.get_code().get_statement() == ID_fence)
238+
instruction.is_other() && instruction.code().get_statement() == ID_fence)
240239
{
241240
visit_cfg_asm_fence(i_it, function_id);
242241
}
@@ -792,13 +791,13 @@ void instrumentert::cfg_visitort::visit_cfg_asm_fence(
792791
const irep_idt &function_id)
793792
{
794793
const goto_programt::instructiont &instruction=*i_it;
795-
bool WRfence = instruction.get_code().get_bool(ID_WRfence);
796-
bool WWfence = instruction.get_code().get_bool(ID_WWfence);
797-
bool RRfence = instruction.get_code().get_bool(ID_RRfence);
798-
bool RWfence = instruction.get_code().get_bool(ID_RWfence);
799-
bool WWcumul = instruction.get_code().get_bool(ID_WWcumul);
800-
bool RRcumul = instruction.get_code().get_bool(ID_RRcumul);
801-
bool RWcumul = instruction.get_code().get_bool(ID_RWcumul);
794+
bool WRfence = instruction.code().get_bool(ID_WRfence);
795+
bool WWfence = instruction.code().get_bool(ID_WWfence);
796+
bool RRfence = instruction.code().get_bool(ID_RRfence);
797+
bool RWfence = instruction.code().get_bool(ID_RWfence);
798+
bool WWcumul = instruction.code().get_bool(ID_WWcumul);
799+
bool RRcumul = instruction.code().get_bool(ID_RRcumul);
800+
bool RWcumul = instruction.code().get_bool(ID_RWcumul);
802801
const abstract_eventt new_fence_event(
803802
abstract_eventt::operationt::ASMfence,
804803
thread,

src/goto-instrument/wmm/shared_buffers.cpp

+8-8
Original file line numberDiff line numberDiff line change
@@ -282,7 +282,7 @@ void shared_bufferst::write(
282282
target,
283283
source_location,
284284
vars.w_buff0,
285-
original_instruction.get_code().op1());
285+
original_instruction.code().op1());
286286

287287
// We update the used flags
288288
assignment(
@@ -1219,7 +1219,7 @@ void shared_bufferst::cfg_visitort::weak_memory(
12191219
choice1_expr,
12201220
dereference_exprt{new_read_expr},
12211221
to_replace_expr),
1222-
to_replace_expr); // original_instruction.get_code().op1());
1222+
to_replace_expr); // original_instruction.code().op1());
12231223

12241224
shared_buffers.assignment(
12251225
goto_program,
@@ -1237,7 +1237,7 @@ void shared_bufferst::cfg_visitort::weak_memory(
12371237
i_it,
12381238
source_location,
12391239
w_entry.second.object,
1240-
original_instruction.get_code().op1());
1240+
original_instruction.code().op1());
12411241
}
12421242
}
12431243

@@ -1286,11 +1286,11 @@ void shared_bufferst::cfg_visitort::weak_memory(
12861286
else if(
12871287
is_fence(instruction, ns) ||
12881288
(instruction.is_other() &&
1289-
instruction.get_code().get_statement() == ID_fence &&
1290-
(instruction.get_code().get_bool("WRfence") ||
1291-
instruction.get_code().get_bool("WWfence") ||
1292-
instruction.get_code().get_bool("RWfence") ||
1293-
instruction.get_code().get_bool("RRfence"))))
1289+
instruction.code().get_statement() == ID_fence &&
1290+
(instruction.code().get_bool("WRfence") ||
1291+
instruction.code().get_bool("WWfence") ||
1292+
instruction.code().get_bool("RWfence") ||
1293+
instruction.code().get_bool("RRfence"))))
12941294
{
12951295
goto_programt::instructiont original_instruction;
12961296
original_instruction.swap(instruction);

src/goto-programs/goto_convert.cpp

+7-7
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,7 @@ static void finish_catch_push_targets(goto_programt &dest)
6060
{
6161
if(
6262
instruction.is_catch() &&
63-
instruction.get_code().get_statement() == ID_push_catch)
63+
instruction.code().get_statement() == ID_push_catch)
6464
{
6565
// Populate `targets` with a GOTO instruction target per
6666
// exception handler if it isn't already populated.
@@ -71,7 +71,7 @@ static void finish_catch_push_targets(goto_programt &dest)
7171
{
7272
bool handler_added=true;
7373
const code_push_catcht::exception_listt &handler_list =
74-
to_code_push_catch(instruction.get_code()).exception_list();
74+
to_code_push_catch(instruction.code()).exception_list();
7575

7676
for(const auto &handler : handler_list)
7777
{
@@ -114,7 +114,7 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
114114

115115
if(i.is_start_thread())
116116
{
117-
const irep_idt &goto_label = i.get_code().get(ID_destination);
117+
const irep_idt &goto_label = i.code().get(ID_destination);
118118

119119
labelst::const_iterator l_it=
120120
targets.labels.find(goto_label);
@@ -123,22 +123,22 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
123123
{
124124
throw incorrect_goto_program_exceptiont(
125125
"goto label \'" + id2string(goto_label) + "\' not found",
126-
i.get_code().find_source_location());
126+
i.code().find_source_location());
127127
}
128128

129129
i.targets.push_back(l_it->second.first);
130130
}
131131
else if(i.is_incomplete_goto())
132132
{
133-
const irep_idt &goto_label = i.get_code().get(ID_destination);
133+
const irep_idt &goto_label = i.code().get(ID_destination);
134134

135135
labelst::const_iterator l_it=targets.labels.find(goto_label);
136136

137137
if(l_it == targets.labels.end())
138138
{
139139
throw incorrect_goto_program_exceptiont(
140140
"goto label \'" + id2string(goto_label) + "\' not found",
141-
i.get_code().find_source_location());
141+
i.code().find_source_location());
142142
}
143143

144144
i.complete_goto(l_it->second.first);
@@ -204,7 +204,7 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program)
204204
for(auto &g_it : targets.computed_gotos)
205205
{
206206
goto_programt::instructiont &i=*g_it;
207-
dereference_exprt destination = to_dereference_expr(i.get_code().op0());
207+
dereference_exprt destination = to_dereference_expr(i.code().op0());
208208
const exprt pointer = destination.pointer();
209209

210210
// remember the expression for later checks

0 commit comments

Comments
 (0)