replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

remove goto_programt::instructiont::function member

This commit is contained in:
Daniel Kroening 2018-10-09 08:51:17 +01:00 committed by Michael Tautschnig
parent 22373c1135
commit c9c872e267
50 changed files with 14 additions and 264 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
jbmc/src/java_bytecode/remove_exceptions.cpp
View File

@ -237,7 +237,6 @@ void remove_exceptionst::instrument_exception_handler(
t_null->code=code_assignt(
thrown_global_symbol,
null_voidptr);
t_null->function=instr_it->function;
// add the assignment exc = @inflight_exception (before the null assignment)
goto_programt::targett t_exc=goto_program.insert_after(instr_it);
@ -246,7 +245,6 @@ void remove_exceptionst::instrument_exception_handler(
t_exc->code=code_assignt(
thrown_exception_local,
typecast_exprt(thrown_global_symbol, thrown_exception_local.type()));
t_exc->function=instr_it->function;
}
instr_it->make_skip();
}
@ -352,7 +350,6 @@ void remove_exceptionst::add_exception_dispatch_sequence(
goto_programt::targett t_exc=goto_program.insert_after(instr_it);
t_exc->make_goto(new_state_pc);
t_exc->source_location=instr_it->source_location;
t_exc->function=instr_it->function;
// use instanceof to check that this is the correct handler
struct_tag_typet type(stack_catch[i][j].first);
@ -377,7 +374,6 @@ void remove_exceptionst::add_exception_dispatch_sequence(
default_dispatch->make_goto(default_target);
default_dispatch->source_location=instr_it->source_location;
default_dispatch->function=instr_it->function;
// add dead instructions
for(const auto &local : locals)
@ -386,7 +382,6 @@ void remove_exceptionst::add_exception_dispatch_sequence(
t_dead->make_dead();
t_dead->code=code_deadt(local);
t_dead->source_location=instr_it->source_location;
t_dead->function=instr_it->function;
}
}
@ -466,7 +461,6 @@ bool remove_exceptionst::instrument_function_call(
goto_programt::targett t_null=goto_program.insert_after(instr_it);
t_null->make_goto(next_it);
t_null->source_location=instr_it->source_location;
t_null->function=instr_it->function;
t_null->guard=no_exception_currently_in_flight;
}

3
jbmc/src/jbmc/jbmc_parse_options.cpp
View File

@ -840,9 +840,6 @@ void jbmc_parse_optionst::process_goto_function(
function.compute_location_numbers();
goto_function.body.compute_loop_numbers();
}
// update the function member in each instruction
function.update_instructions_function();
}
}

15
jbmc/src/jdiff/java_syntactic_diff.cpp
View File

@ -75,21 +75,6 @@ bool java_syntactic_difft::operator()()
modified_functions.insert(it->first);
continue;
}
goto_programt::instructionst::const_iterator i_it1 =
it->second.body.instructions.begin();
for(goto_programt::instructionst::const_iterator
i_it2 = f_it->second.body.instructions.begin();
i_it1 != it->second.body.instructions.end() &&
i_it2 != f_it->second.body.instructions.end();
++i_it1, ++i_it2)
{
if(i_it1->function != i_it2->function)
{
modified_functions.insert(it->first);
break;
}
}
}
forall_goto_functions(it, goto_model2.goto_functions)
{

6
src/analyses/flow_insensitive_analysis.cpp
View File

@ -212,12 +212,9 @@ bool flow_insensitive_analysis_baset::do_function_call(
goto_programt::targett r = temp.add(goto_programt::make_return(code_returnt(
side_effect_expr_nondett(code.lhs().type(), l_call->source_location))));
r->function=f_it->first;
r->location_number=0;
goto_programt::targett t = temp.add(goto_programt::make_end_function());
t->function=f_it->first;
t->location_number=1;
locationt l_next=l_call; l_next++;
@ -242,9 +239,6 @@ bool flow_insensitive_analysis_baset::do_function_call(
// get the state at the beginning of the function
locationt l_begin=goto_function.body.instructions.begin();
DATA_INVARIANT(
l_begin->function == f_it->first, "function names have to match");
// do the edge from the call site to the beginning of the function
new_data =
state.transform(ns, calling_function, l_call, f_it->first, l_begin);

3
src/analyses/goto_check.cpp
View File

@ -1900,9 +1900,6 @@ void goto_checkt::goto_check(
i_it->source_location.set_java_bytecode_index(
it->source_location.get_java_bytecode_index());
}
if(i_it->function.empty())
i_it->function=it->function;
}
// insert new instructions -- make sure targets are not moved

1
src/analyses/interval_analysis.cpp
View File

@ -82,7 +82,6 @@ void instrument_intervals(
t->make_assumption(conjunction(assertion));
i_it++; // goes to original instruction
t->source_location=i_it->source_location;
t->function=i_it->function;
}
}
}

3
src/assembler/remove_asm.cpp
View File

@ -493,9 +493,6 @@ void remove_asmt::process_function(
it->make_skip();
did_something = true;
for(auto &instruction : tmp_dest.instructions)
instruction.function = it->function;
goto_programt::targett next = it;
next++;

15
src/goto-diff/syntactic_diff.cpp
View File

@ -74,21 +74,6 @@ bool syntactic_difft::operator()()
modified_functions.insert(it->first);
continue;
}
goto_programt::instructionst::const_iterator
i_it1=it->second.body.instructions.begin();
for(goto_programt::instructionst::const_iterator
i_it2=f_it->second.body.instructions.begin();
i_it1!=it->second.body.instructions.end() &&
i_it2!=f_it->second.body.instructions.end();
++i_it1, ++i_it2)
{
if(i_it1->function != i_it2->function)
{
modified_functions.insert(it->first);
break;
}
}
}
forall_goto_functions(it, goto_model2.goto_functions)
{

2
src/goto-diff/unified_diff.cpp
View File

@ -392,7 +392,7 @@ bool unified_difft::instructions_equal(
const goto_programt::instructiont &ins1,
const goto_programt::instructiont &ins2)
{
return ins1.equals(ins2) && ins1.function == ins2.function &&
return ins1.equals(ins2) &&
(ins1.targets.empty() ||
instructions_equal(*ins1.get_target(), *ins2.get_target()));
}

2
src/goto-instrument/branch.cpp
View File

@ -54,7 +54,6 @@ void branch(
goto_programt::targett t1=body.insert_after(i_it);
t1->make_function_call(
function_to_call(goto_model.symbol_table, id, "taken"));
t1->function=f_it->first;
goto_programt::targett t2=body.insert_after(t1);
t2->make_goto(i_it->get_target());
@ -62,7 +61,6 @@ void branch(
goto_programt::targett t3=body.insert_after(t2);
t3->make_function_call(
function_to_call(goto_model.symbol_table, id, "not-taken"));
t3->function=f_it->first;
i_it->targets.clear();
i_it->targets.push_back(t3);
}

13
src/goto-instrument/code_contracts.cpp
View File

@ -112,7 +112,6 @@ static void check_apply_invariants(
{
goto_programt::targett a=havoc_code.add_instruction(ASSERT);
a->guard=invariant;
a->function=loop_head->function;
a->source_location=loop_head->source_location;
a->source_location.set_comment("Loop invariant violated before entry");
}
@ -124,7 +123,6 @@ static void check_apply_invariants(
{
goto_programt::targett assume=havoc_code.add_instruction(ASSUME);
assume->guard=invariant;
assume->function=loop_head->function;
assume->source_location=loop_head->source_location;
}
@ -135,7 +133,6 @@ static void check_apply_invariants(
jump->guard =
side_effect_expr_nondett(bool_typet(), loop_head->source_location);
jump->targets.push_back(loop_end);
jump->function=loop_head->function;
}
// Now havoc at the loop head. Use insert_swap to
@ -146,7 +143,6 @@ static void check_apply_invariants(
{
goto_programt::instructiont a(ASSERT);
a.guard=invariant;
a.function=loop_end->function;
a.source_location=loop_end->source_location;
a.source_location.set_comment("Loop invariant not preserved");
goto_function.body.insert_before_swap(loop_end, a);
@ -216,7 +212,6 @@ void code_contractst::apply_contract(
{
goto_programt::instructiont a(ASSERT);
a.guard=requires;
a.function=target->function;
a.source_location=target->source_location;
goto_program.insert_before_swap(target, a);
@ -295,7 +290,6 @@ void code_contractst::add_contract_check(
// build skip so that if(nondet) can refer to it
goto_programt tmp_skip;
goto_programt::targett skip=tmp_skip.add_instruction(SKIP);
skip->function=dest.instructions.front().function;
skip->source_location=ensures.source_location();
goto_programt check;
@ -304,7 +298,6 @@ void code_contractst::add_contract_check(
goto_programt::targett g=check.add_instruction();
g->make_goto(
skip, side_effect_expr_nondett(bool_typet(), skip->source_location));
g->function=skip->function;
g->source_location=skip->source_location;
// prepare function call including all declarations
@ -315,7 +308,6 @@ void code_contractst::add_contract_check(
if(gf.type.return_type()!=empty_typet())
{
goto_programt::targett d=check.add_instruction(DECL);
d->function=skip->function;
d->source_location=skip->source_location;
symbol_exprt r=
@ -336,7 +328,6 @@ void code_contractst::add_contract_check(
++p_it)
{
goto_programt::targett d=check.add_instruction(DECL);
d->function=skip->function;
d->source_location=skip->source_location;
symbol_exprt p=
@ -358,7 +349,6 @@ void code_contractst::add_contract_check(
{
goto_programt::targett a=check.add_instruction();
a->make_assumption(requires);
a->function=skip->function;
a->source_location=requires.source_location();
// rewrite any use of parameters
@ -368,13 +358,11 @@ void code_contractst::add_contract_check(
// ret=function(parameter1, ...)
goto_programt::targett f=check.add_instruction();
f->make_function_call(call);
f->function=skip->function;
f->source_location=skip->source_location;
// assert(ensures)
goto_programt::targett a=check.add_instruction();
a->make_assertion(ensures);
a->function=skip->function;
a->source_location=ensures.source_location();
// rewrite any use of __CPROVER_return_value
@ -383,7 +371,6 @@ void code_contractst::add_contract_check(
// assume(false)
goto_programt::targett af=check.add_instruction();
af->make_assumption(false_exprt());
af->function=skip->function;
af->source_location=ensures.source_location();
// prepend the new code to dest

1
src/goto-instrument/cover_instrument.h
View File

@ -74,7 +74,6 @@ protected:
t->source_location.set(ID_coverage_criterion, coverage_criterion);
t->source_location.set_property_class(property_class);
t->source_location.set_function(function_id);
t->function = function_id;
}
bool is_non_cover_assertion(goto_programt::const_targett t) const

3
src/goto-instrument/cover_instrument_mcdc.cpp
View File

@ -667,7 +667,6 @@ void cover_mcdc_instrumentert::instrument(
i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
i_it->source_location.set_property_class(property_class);
i_it->source_location.set_function(function_id);
i_it->function = function_id;
std::string comment_f = description + " `" + p_string + "' false";
goto_program.insert_before_swap(i_it);
@ -677,7 +676,6 @@ void cover_mcdc_instrumentert::instrument(
i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
i_it->source_location.set_property_class(property_class);
i_it->source_location.set_function(function_id);
i_it->function = function_id;
}
std::set<exprt> controlling;
@ -704,7 +702,6 @@ void cover_mcdc_instrumentert::instrument(
i_it->source_location.set(ID_coverage_criterion, coverage_criterion);
i_it->source_location.set_property_class(property_class);
i_it->source_location.set_function(function_id);
i_it->function = function_id;
}
for(std::size_t i = 0; i < both.size() * 2 + controlling.size(); i++)

1
src/goto-instrument/cover_instrument_other.cpp
View File

@ -86,5 +86,4 @@ void cover_instrument_end_of_function(
if_it->source_location.set_comment(comment);
if_it->source_location.set_property_class("reachability_constraint");
if_it->source_location.set_function(function_id);
if_it->function = function_id;
}

3
src/goto-instrument/function.cpp
View File

@ -91,7 +91,6 @@ void function_enter(
body.insert_before(body.instructions.begin());
t->make_function_call(
function_to_call(goto_model.symbol_table, id, f_it->first));
t->function=f_it->first;
}
}
@ -123,7 +122,6 @@ void function_exit(
if(i_it->is_return())
{
goto_programt::instructiont call;
call.function=f_it->first;
call.make_function_call(
function_to_call(goto_model.symbol_table, id, f_it->first));
body.insert_before_swap(i_it, call);
@ -154,7 +152,6 @@ void function_exit(
goto_programt::instructiont call;
call.make_function_call(
function_to_call(goto_model.symbol_table, id, f_it->first));
call.function=f_it->first;
body.insert_before_swap(last, call);
}
}

4
src/goto-instrument/generate_function_bodies.cpp
View File

@ -76,7 +76,6 @@ protected:
// NOLINTNEXTLINE
auto add_instruction = [&]() {
auto instruction = function.body.add_instruction();
instruction->function = function_name;
instruction->source_location = function_symbol.location;
return instruction;
};
@ -99,7 +98,6 @@ protected:
// NOLINTNEXTLINE
auto add_instruction = [&]() {
auto instruction = function.body.add_instruction();
instruction->function = function_name;
instruction->source_location = function_symbol.location;
instruction->source_location.set_function(function_name);
return instruction;
@ -130,7 +128,6 @@ protected:
// NOLINTNEXTLINE
auto add_instruction = [&]() {
auto instruction = function.body.add_instruction();
instruction->function = function_name;
instruction->source_location = function_symbol.location;
instruction->source_location.set_function(function_name);
return instruction;
@ -212,7 +209,6 @@ protected:
// NOLINTNEXTLINE
auto add_instruction = [&]() {
auto instruction = function.body.add_instruction();
instruction->function = function_name;
instruction->source_location = function_symbol.location;
return instruction;
};

4
src/goto-instrument/interrupt.cpp
View File

@ -110,11 +110,9 @@ static void interrupt(
t_goto->make_goto(t_orig);
t_goto->source_location=source_location;
t_goto->guard = side_effect_expr_nondett(bool_typet(), source_location);
t_goto->function=original_instruction.function;
t_call->make_function_call(isr_call);
t_call->source_location=source_location;
t_call->function=original_instruction.function;
t_orig->swap(original_instruction);
@ -138,11 +136,9 @@ static void interrupt(
t_goto->make_goto(t_orig);
t_goto->source_location=source_location;
t_goto->guard = side_effect_expr_nondett(bool_typet(), source_location);
t_goto->function=i_it->function;
t_call->make_function_call(isr_call);
t_call->source_location=source_location;
t_call->function=i_it->function;
i_it=t_call; // the for loop already counts us up
}

1
src/goto-instrument/loop_utils.cpp
View File

@ -50,7 +50,6 @@ void build_havoc_code(
goto_programt::targett t = dest.add(goto_programt::make_assignment(
code_assignt(std::move(lhs), std::move(rhs)),
loop_head->source_location));
t->function=loop_head->function;
t->code.add_source_location()=loop_head->source_location;
}
}

3
src/goto-instrument/model_argc_argv.cpp
View File

@ -152,10 +152,7 @@ bool model_argc_argv(
main_symbol.mode);
Forall_goto_program_instructions(it, init_instructions)
{
it->source_location.set_file("<built-in-library>");
it->function=goto_model.goto_functions.entry_point();
}
goto_functionst::function_mapt::iterator start_entry=
goto_model.goto_functions.function_map.find(

1
src/goto-instrument/nondet_static.cpp
View File

@ -97,7 +97,6 @@ void nondet_static(
side_effect_expr_nondett(
sym.type(), original_instruction.source_location));
i_it->source_location = original_instruction.source_location;
i_it->function = original_instruction.function;
}
}
else if(instruction.is_function_call())

1
src/goto-instrument/skip_loops.cpp
View File

@ -48,7 +48,6 @@ static bool skip_loops(
goto_programt::targett g=goto_program.insert_before(loop_head);
g->make_goto(next, true_exprt());
g->source_location=loop_head->source_location;
g->function=loop_head->function;
++l_it;
}

4
src/goto-instrument/stack_depth.cpp
View File

@ -54,7 +54,6 @@ void stack_depth(
goto_programt::targett assert_ins=goto_program.insert_before(first);
assert_ins->make_assertion(guard);
assert_ins->source_location=first->source_location;
assert_ins->function=first->function;
assert_ins->source_location.set_comment(
"Stack depth exceeds "+std::to_string(i_depth));
@ -65,7 +64,6 @@ void stack_depth(
plus_ins->code=code_assignt(symbol,
plus_exprt(symbol, from_integer(1, symbol.type())));
plus_ins->source_location=first->source_location;
plus_ins->function=first->function;
goto_programt::targett last=--goto_program.instructions.end();
assert(last->is_end_function());
@ -75,7 +73,6 @@ void stack_depth(
minus_ins.code=code_assignt(symbol,
minus_exprt(symbol, from_integer(1, symbol.type())));
minus_ins.source_location=last->source_location;
minus_ins.function=last->function;
goto_program.insert_before_swap(last, minus_ins);
}
@ -108,7 +105,6 @@ void stack_depth(
it->make_assignment();
it->code=code_assignt(sym, from_integer(0, sym.type()));
// no suitable value for source location -- omitted
it->function = INITIALIZE_FUNCTION;
// update counters etc.
goto_model.goto_functions.update();

2
src/goto-instrument/thread_instrumentation.cpp
View File

@ -35,7 +35,6 @@ void thread_exit_instrumentation(goto_programt &goto_program)
assert(end->is_end_function());
source_locationt source_location=end->source_location;
irep_idt function=end->function;
goto_program.insert_before_swap(end);
@ -51,7 +50,6 @@ void thread_exit_instrumentation(goto_programt &goto_program)
end->source_location=source_location;
end->source_location.set_comment("mutexes must not be locked on thread exit");
end->function=function;
}
void thread_exit_instrumentation(goto_modelt &goto_model)

5
src/goto-instrument/unwind.cpp
View File

@ -120,7 +120,6 @@ void goto_unwindt::unwind(
t->make_skip();
t->source_location=loop_head->source_location;
t->function=loop_head->function;
t->location_number=loop_head->location_number;
}
else if(unwind_strategy==unwind_strategyt::CONTINUE)
@ -155,7 +154,6 @@ void goto_unwindt::unwind(
UNREACHABLE;
new_t->source_location=loop_head->source_location;
new_t->function=loop_head->function;
new_t->location_number=loop_head->location_number;
unwind_log.insert(new_t, loop_head->location_number);
}
@ -181,7 +179,6 @@ void goto_unwindt::unwind(
t_goto->make_goto(goto_program.const_cast_target(loop_exit));
t_goto->source_location=loop_exit->source_location;
t_goto->function=loop_exit->function;
t_goto->guard=true_exprt();
t_goto->location_number=loop_exit->location_number;
}
@ -193,7 +190,6 @@ void goto_unwindt::unwind(
t_skip->make_skip();
t_skip->source_location=loop_head->source_location;
t_skip->function=loop_head->function;
t_skip->location_number=loop_head->location_number;
// where to go for the next iteration
@ -236,7 +232,6 @@ void goto_unwindt::unwind(
t_skip->make_skip();
t_skip->source_location=loop_head->source_location;
t_skip->function=loop_head->function;
t_skip->location_number=loop_head->location_number;
// redirect gotos into loop body

1
src/goto-instrument/wmm/weak_memory.cpp
View File

@ -91,7 +91,6 @@ void introduce_temporaries(
new_i.make_assignment();
new_i.code=code_assignt(symbol_expr, instruction.guard);
new_i.source_location=instruction.source_location;
new_i.function=instruction.function;
// replace guard
instruction.guard=symbol_expr;

3
src/goto-programs/goto_convert_functions.cpp
View File

@ -204,9 +204,6 @@ void goto_convert_functionst::convert_function(
// add "end of function"
f.body.destructive_append(tmp_end_function);
// do function tags (they are empty at this point)
f.update_instructions_function(identifier);
f.body.update();
if(hide(f.body))

8
src/goto-programs/goto_function.h
View File

@ -72,14 +72,6 @@ public:
parameter_identifiers.clear();
}
/// update the function member in each instruction
/// \param function_id: the `function_id` used for assigning empty function
/// members
void update_instructions_function(const irep_idt &function_id)
{
body.update_instructions_function(function_id);
}
void swap(goto_functiont &other)
{
body.swap(other.body);

11
src/goto-programs/goto_functions.h
View File

@ -78,23 +78,12 @@ public:
void compute_target_numbers();
void compute_incoming_edges();
/// update the function member in each instruction by setting it to
/// the goto function's identifier
void update_instructions_function()
{
for(auto &func : function_map)
{
func.second.update_instructions_function(func.first);
}
}
void update()
{
compute_incoming_edges();
compute_target_numbers();
compute_location_numbers();
compute_loop_numbers();
update_instructions_function();
}
/// Get the identifier of the entry point to a goto model

11
src/goto-programs/goto_inline_class.cpp
View File

@ -64,7 +64,6 @@ void goto_inlinet::parameter_assignments(
goto_programt::targett decl = dest.add(
goto_programt::make_decl(symbol.symbol_expr(), source_location));
decl->code.add_source_location()=source_location;
decl->function=adjust_function?target->function:function_name;
}
// this is the actual parameter
@ -127,8 +126,6 @@ void goto_inlinet::parameter_assignments(
dest.add_instruction(ASSIGN);
dest.instructions.back().source_location=source_location;
dest.instructions.back().code.swap(assignment);
dest.instructions.back().function=
adjust_function?target->function:function_name;
}
if(it1!=arguments.end())
@ -143,7 +140,6 @@ void goto_inlinet::parameter_assignments(
void goto_inlinet::parameter_destruction(
const goto_programt::targett target,
const irep_idt &function_name, // name of called function
const code_typet &code_type, // type of called function
goto_programt &dest)
{
@ -170,7 +166,6 @@ void goto_inlinet::parameter_destruction(
goto_programt::targett dead = dest.add(
goto_programt::make_dead(symbol.symbol_expr(), source_location));
dead->code.add_source_location()=source_location;
dead->function=adjust_function?target->function:function_name;
}
}
}
@ -277,10 +272,6 @@ void goto_inlinet::insert_function_body(
"final instruction of a function must be an END_FUNCTION");
end.type=LOCATION;
if(adjust_function)
for(auto &instruction : body.instructions)
instruction.function=target->function;
// make sure the inlined function does not introduce hiding
if(goto_function.is_hidden())
{
@ -299,7 +290,7 @@ void goto_inlinet::insert_function_body(
tmp1);
goto_programt tmp2;
parameter_destruction(target, identifier, goto_function.type, tmp2);
parameter_destruction(target, goto_function.type, tmp2);
goto_programt tmp;
tmp.destructive_append(tmp1); // par assignment

1
src/goto-programs/goto_inline_class.h
View File

@ -184,7 +184,6 @@ protected:
void parameter_destruction(
const goto_programt::targett target,
const irep_idt &function_name,
const code_typet &code_type,
goto_programt &dest);

7
src/goto-programs/goto_model.h
View File

@ -194,13 +194,6 @@ public:
goto_functions.compute_location_numbers(goto_function.body);
}
/// Updates the empty function member of each instruction by setting them
/// to `function_id`
void update_instructions_function()
{
goto_function.update_instructions_function(function_id);
}
/// Get symbol table
/// \return journalling symbol table that (a) wraps the global symbol table,
/// and (b) has recorded all symbol mutations (insertions, updates and

91
src/goto-programs/goto_program.h
View File

@ -264,9 +264,6 @@ public:
return code;
}
/// The function this instruction belongs to
irep_idt function;
/// The location of the instruction in the source file
source_locationt source_location;
@ -436,13 +433,11 @@ public:
/// Constructor that can set all members, passed by value
instructiont(
codet _code,
irep_idt _function,
source_locationt _source_location,
goto_program_instruction_typet _type,
exprt _guard,
targetst _targets)
: code(std::move(_code)),
function(_function),
source_location(std::move(_source_location)),
type(_type),
guard(std::move(_guard)),
@ -459,7 +454,6 @@ public:
swap(instruction.type, type);
swap(instruction.guard, guard);
swap(instruction.targets, targets);
swap(instruction.function, function);
}
/// Uniquely identify an invalid target or location
@ -535,42 +529,6 @@ public:
return t;
}
/// Get the id of the function that contains the instruction pointed-to by the
/// given instruction iterator.
///
/// \param l: instruction iterator
/// \return id of the function that contains the pointed-to goto instruction
static const irep_idt get_function_id(
const_targett l)
{
// The field `function` of an instruction may not always contain the id of
// the function it is currently in, due to goto program modifications such
// as inlining. For example, if an instruction in a function `f` is inlined
// into a function `g`, the instruction may, depending on the arguments to
// the inliner, retain the original value of `f` in the function field.
// However, instructions of type END_FUNCTION are never inlined into other
// functions, hence they contain the id of the function they are in. Thus,
// this function takes the END_FUNCTION instruction of the goto program and
// returns the value of its function field.
while(!l->is_end_function())
++l;
return l->function;
}
/// Get the id of the function that contains the given goto program.
///
/// \param p: the goto program
/// \return id of the function that contains the goto program
static const irep_idt get_function_id(
const goto_programt &p)
{
PRECONDITION(!p.empty());
return get_function_id(--p.instructions.end());
}
template <typename Target>
std::list<Target> get_successors(Target target) const;
@ -695,22 +653,6 @@ public:
}
}
/// Sets the `function` member of each instruction if not yet set
/// Note that a goto program need not be a goto function and therefore,
/// we cannot do this in update(), but only at the level of
/// of goto_functionst where goto programs are guaranteed to be
/// named functions.
void update_instructions_function(const irep_idt &function_id)
{
for(auto &instruction : instructions)
{
if(instruction.function.empty())
{
instruction.function = function_id;
}
}
}
/// Compute location numbers
void compute_location_numbers()
{
@ -811,14 +753,14 @@ public:
static instructiont
make_return(const source_locationt &l = source_locationt::nil())
{
return instructiont(code_returnt(), irep_idt(), l, RETURN, nil_exprt(), {});
return instructiont(code_returnt(), l, RETURN, nil_exprt(), {});
}
static instructiont make_return(
code_returnt c,
const source_locationt &l = source_locationt::nil())
{
return instructiont(std::move(c), irep_idt(), l, RETURN, nil_exprt(), {});
return instructiont(std::move(c), l, RETURN, nil_exprt(), {});
}
static instructiont
@ -826,7 +768,6 @@ public:
{
return instructiont(
static_cast<const codet &>(get_nil_irep()),
irep_idt(),
l,
SKIP,
nil_exprt(),
@ -837,7 +778,6 @@ public:
{
return instructiont(
static_cast<const codet &>(get_nil_irep()),
irep_idt(),
l,
LOCATION,
nil_exprt(),
@ -849,7 +789,6 @@ public:
{
return instructiont(
static_cast<const codet &>(get_nil_irep()),
irep_idt(),
l,
THROW,
nil_exprt(),
@ -861,7 +800,6 @@ public:
{
return instructiont(
static_cast<const codet &>(get_nil_irep()),
irep_idt(),
l,
CATCH,
nil_exprt(),
@ -874,7 +812,6 @@ public:
{
return instructiont(
static_cast<const codet &>(get_nil_irep()),
irep_idt(),
l,
ASSERT,
exprt(g),
@ -886,29 +823,26 @@ public:
const source_locationt &l = source_locationt::nil())
{
return instructiont(
static_cast<const codet &>(get_nil_irep()), irep_idt(), l, ASSUME, g, {});
static_cast<const codet &>(get_nil_irep()), l, ASSUME, g, {});
}
static instructiont make_other(const codet &_code)
{
return instructiont(
_code, irep_idt(), source_locationt::nil(), OTHER, nil_exprt(), {});
return instructiont(_code, source_locationt::nil(), OTHER, nil_exprt(), {});
}
static instructiont make_decl(
const symbol_exprt &symbol,
const source_locationt &l = source_locationt::nil())
{
return instructiont(
code_declt(symbol), irep_idt(), l, DECL, nil_exprt(), {});
return instructiont(code_declt(symbol), l, DECL, nil_exprt(), {});
}
static instructiont make_dead(
const symbol_exprt &symbol,
const source_locationt &l = source_locationt::nil())
{
return instructiont(
code_deadt(symbol), irep_idt(), l, DEAD, nil_exprt(), {});
return instructiont(code_deadt(symbol), l, DEAD, nil_exprt(), {});
}
static instructiont
@ -916,7 +850,6 @@ public:
{
return instructiont(
static_cast<const codet &>(get_nil_irep()),
irep_idt(),
l,
ATOMIC_BEGIN,
nil_exprt(),
@ -928,7 +861,6 @@ public:
{
return instructiont(
static_cast<const codet &>(get_nil_irep()),
irep_idt(),
l,
ATOMIC_END,
nil_exprt(),
@ -940,7 +872,6 @@ public:
{
return instructiont(
static_cast<const codet &>(get_nil_irep()),
irep_idt(),
l,
END_FUNCTION,
nil_exprt(),
@ -951,7 +882,7 @@ public:
const code_gotot &_code,
const source_locationt &l = source_locationt::nil())
{
return instructiont(_code, irep_idt(), l, INCOMPLETE_GOTO, nil_exprt(), {});
return instructiont(_code, l, INCOMPLETE_GOTO, nil_exprt(), {});
}
static instructiont make_goto(
@ -960,7 +891,6 @@ public:
{
return instructiont(
static_cast<const codet &>(get_nil_irep()),
irep_idt(),
l,
GOTO,
true_exprt(),
@ -974,7 +904,6 @@ public:
{
return instructiont(
static_cast<const codet &>(get_nil_irep()),
irep_idt(),
l,
GOTO,
g,
@ -985,21 +914,21 @@ public:
const code_assignt &_code,
const source_locationt &l = source_locationt::nil())
{
return instructiont(_code, irep_idt(), l, ASSIGN, nil_exprt(), {});
return instructiont(_code, l, ASSIGN, nil_exprt(), {});
}
static instructiont make_decl(
const code_declt &_code,
const source_locationt &l = source_locationt::nil())
{
return instructiont(_code, irep_idt(), l, DECL, nil_exprt(), {});
return instructiont(_code, l, DECL, nil_exprt(), {});
}
static instructiont make_function_call(
const code_function_callt &_code,
const source_locationt &l = source_locationt::nil())
{
return instructiont(_code, irep_idt(), l, FUNCTION_CALL, nil_exprt(), {});
return instructiont(_code, l, FUNCTION_CALL, nil_exprt(), {});
}
};

2
src/goto-programs/instrument_preconditions.cpp
View File

@ -110,7 +110,6 @@ void instrument_preconditions(
goto_model.goto_functions);
source_locationt source_location=it->source_location;
irep_idt function=it->function;
replace_symbolt r=actuals_replace_map(call, ns);
@ -121,7 +120,6 @@ void instrument_preconditions(
exprt instance=p->guard;
r(instance);
it->make_assertion(instance);
it->function=function;
it->source_location=source_location;
it->source_location.set_property_class(ID_precondition_instance);
it->source_location.set_comment(p->source_location.get_comment());

3
src/goto-programs/link_goto_model.cpp
View File

@ -34,9 +34,6 @@ static void rename_symbols_in_function(
{
rename_symbol(iit->code);
rename_symbol(iit->guard);
// we need to update the instruction's function field as
// well, with the new symbol for the function
iit->function=new_function_name;
}
}

4
src/goto-programs/mm_io.cpp
View File

@ -54,7 +54,6 @@ void mm_io(
{
const dereference_exprt &d=*deref_expr_r.begin();
source_locationt source_location=it->source_location;
irep_idt function=it->function;
const code_typet &ct=to_code_type(mm_io_r.type());
irep_idt identifier=to_symbol_expr(mm_io_r).get_identifier();
@ -72,7 +71,6 @@ void mm_io(
goto_function.body.insert_before_swap(it);
it->make_function_call(fc);
it->source_location=source_location;
it->function=function;
it++;
}
}
@ -83,7 +81,6 @@ void mm_io(
{
const dereference_exprt &d=to_dereference_expr(a.lhs());
source_locationt source_location=it->source_location;
irep_idt function=it->function;
const code_typet &ct=to_code_type(mm_io_w.type());
const typet &pt=ct.parameters()[0].type();
const typet &st=ct.parameters()[1].type();
@ -97,7 +94,6 @@ void mm_io(
goto_function.body.insert_before_swap(it);
it->make_function_call(fc);
it->source_location=source_location;
it->function=function;
it++;
}
}

1
src/goto-programs/parameter_assignments.cpp
View File

@ -76,7 +76,6 @@ void parameter_assignmentst::do_function_calls(
if(rhs.type()!=lhs.type())
rhs.make_typecast(lhs.type());
t->code=code_assignt(lhs, rhs);
t->function=i_it->function;
}
}

2
src/goto-programs/read_bin_goto_object.cpp
View File

@ -100,7 +100,7 @@ static bool read_bin_goto_object_v4(
goto_programt::instructiont &instruction=*itarget;
irepconverter.reference_convert(in, instruction.code);
instruction.function = irepconverter.read_string_ref(in);
irepconverter.read_string_ref(in); // former function
irepconverter.reference_convert(in, instruction.source_location);
instruction.type = (goto_program_instruction_typet)
irepconverter.read_gb_word(in);

2
src/goto-programs/remove_calls_no_body.cpp
View File

@ -38,7 +38,6 @@ void remove_calls_no_bodyt::remove_call_no_body(
goto_programt::targett t = tmp.add_instruction();
t->make_other(code_expressiont(argument));
t->source_location = target->source_location;
t->function = target->function;
}
// return value
@ -51,7 +50,6 @@ void remove_calls_no_bodyt::remove_call_no_body(
goto_programt::targett t = tmp.add_instruction(ASSIGN);
t->source_location = target->source_location;
t->function = target->function;
t->code.swap(code);
}

1
src/goto-programs/remove_function_pointers.cpp
View File

@ -422,7 +422,6 @@ void remove_function_pointerst::remove_function_pointer(
irep_idt property_class=it->source_location.get_property_class();
irep_idt comment=it->source_location.get_comment();
it->source_location=target->source_location;
it->function=target->function;
if(!property_class.empty())
it->source_location.set_property_class(property_class);
if(!comment.empty())

2
src/goto-programs/remove_returns.cpp
View File

@ -210,7 +210,6 @@ void remove_returnst::do_function_calls(
t_a->make_assignment();
t_a->source_location=i_it->source_location;
t_a->code=code_assignt(function_call.lhs(), rhs);
t_a->function=i_it->function;
// fry the previous assignment
function_call.lhs().make_nil();
@ -221,7 +220,6 @@ void remove_returnst::do_function_calls(
t_d->make_dead();
t_d->source_location=i_it->source_location;
t_d->code = code_deadt(*return_value);
t_d->function=i_it->function;
}
}
}

1
src/goto-programs/remove_virtual_functions.cpp
View File

@ -328,7 +328,6 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
const irep_idt property_class=it->source_location.get_property_class();
const irep_idt comment=it->source_location.get_comment();
it->source_location=target->source_location;
it->function=target->function;
if(!property_class.empty())
it->source_location.set_property_class(property_class);
if(!comment.empty())

15
src/goto-programs/string_abstraction.cpp
View File

@ -285,7 +285,6 @@ void string_abstractiont::make_decl_and_def(goto_programt &dest,
goto_programt::targett decl1 =
dest.add(goto_programt::make_decl(sym_expr, ref_instr->source_location));
decl1->function=ref_instr->function;
decl1->code.add_source_location()=ref_instr->source_location;
exprt val=symbol.value;
@ -302,7 +301,6 @@ void string_abstractiont::make_decl_and_def(goto_programt &dest,
goto_programt::targett assignment1=dest.add_instruction();
assignment1->make_assignment();
assignment1->source_location=ref_instr->source_location;
assignment1->function=ref_instr->function;
assignment1->code=code_assignt(sym_expr, val);
assignment1->code.add_source_location()=ref_instr->source_location;
}
@ -362,7 +360,6 @@ exprt string_abstractiont::make_val_or_dummy_rec(goto_programt &dest,
goto_programt::targett assignment1=dest.add_instruction();
assignment1->make_assignment();
assignment1->source_location=ref_instr->source_location;
assignment1->function=ref_instr->function;
assignment1->code=code_assignt(member, sym_expr);
assignment1->code.add_source_location()=ref_instr->source_location;
}
@ -410,7 +407,6 @@ symbol_exprt string_abstractiont::add_dummy_symbol_and_value(
goto_programt::targett decl=dest.add_instruction();
decl->make_decl();
decl->source_location=ref_instr->source_location;
decl->function=ref_instr->function;
decl->code=code_declt(sym_expr);
decl->code.add_source_location()=ref_instr->source_location;
@ -436,7 +432,6 @@ symbol_exprt string_abstractiont::add_dummy_symbol_and_value(
goto_programt::targett assignment1=dest.add_instruction();
assignment1->make_assignment();
assignment1->source_location=ref_instr->source_location;
assignment1->function=ref_instr->function;
assignment1->code=code_assignt(sym_expr, new_symbol.value);
assignment1->code.add_source_location()=ref_instr->source_location;
}
@ -1085,7 +1080,6 @@ goto_programt::targett string_abstractiont::abstract_pointer_assign(
goto_programt::instructiont assignment;
assignment.make_assignment();
assignment.source_location=target->source_location;
assignment.function=target->function;
assignment.code=code_assignt(new_lhs, new_rhs);
assignment.code.add_source_location()=target->source_location;
dest.insert_before_swap(target, assignment);
@ -1181,14 +1175,12 @@ goto_programt::targett string_abstractiont::char_assign(
goto_programt::targett assignment1=tmp.add_instruction();
assignment1->make_assignment();
assignment1->source_location=target->source_location;
assignment1->function=target->function;
assignment1->code=code_assignt(i1, true_exprt());
assignment1->code.add_source_location()=target->source_location;
goto_programt::targett assignment2=tmp.add_instruction();
assignment2->make_assignment();
assignment2->source_location=target->source_location;
assignment2->function=target->function;
assignment2->code=code_assignt(lhs, rhs);
assignment2->code.add_source_location()=target->source_location;
@ -1263,18 +1255,14 @@ goto_programt::targett string_abstractiont::value_assignments_if(
goto_programt::targett else_target=tmp.add_instruction(SKIP);
goto_programt::targett out_target=tmp.add_instruction(SKIP);
goto_else->function=target->function;
goto_else->source_location=target->source_location;
goto_else->make_goto(else_target, boolean_negate(rhs.cond()));
goto_out->function=target->function;
goto_out->source_location=target->source_location;
goto_out->make_goto(out_target, true_exprt());
else_target->function=target->function;
else_target->source_location=target->source_location;
out_target->function=target->function;
out_target->source_location=target->source_location;
value_assignments(tmp, goto_out, lhs, rhs.true_case());
@ -1302,7 +1290,6 @@ goto_programt::targett string_abstractiont::value_assignments_string_struct(
member(lhs, whatt::IS_ZERO),
member(rhs, whatt::IS_ZERO));
assignment->code.add_source_location()=target->source_location;
assignment->function=target->function;
assignment->source_location=target->source_location;
}
@ -1312,7 +1299,6 @@ goto_programt::targett string_abstractiont::value_assignments_string_struct(
member(lhs, whatt::LENGTH),
member(rhs, whatt::LENGTH));
assignment->code.add_source_location()=target->source_location;
assignment->function=target->function;
assignment->source_location=target->source_location;
}
@ -1322,7 +1308,6 @@ goto_programt::targett string_abstractiont::value_assignments_string_struct(
member(lhs, whatt::SIZE),
member(rhs, whatt::SIZE));
assignment->code.add_source_location()=target->source_location;
assignment->function=target->function;
assignment->source_location=target->source_location;
}

2
src/goto-programs/write_goto_binary.cpp
View File

@ -97,7 +97,7 @@ bool write_goto_binary_v4(
const goto_programt::instructiont &instruction = *i_it;
irepconverter.reference_convert(instruction.code, out);
irepconverter.write_string_ref(out, instruction.function);
irepconverter.write_string_ref(out, fct.first);
irepconverter.reference_convert(instruction.source_location, out);
write_gb_word(out, (long)instruction.type);
irepconverter.reference_convert(instruction.guard, out);

1
unit/goto-programs/goto_program_assume.cpp
View File

@ -39,7 +39,6 @@ SCENARIO(
symbol_table.insert(fun_symbol);
namespacet ns(symbol_table);
instructions.back().make_assertion(x_le_10);
instructions.back().function = fun_name;
WHEN("Instruction has no targets")
{

1
unit/goto-programs/goto_program_dead.cpp
View File

@ -37,7 +37,6 @@ SCENARIO(
code_deadt removal(var_a);
instructions.back().make_dead();
instructions.back().code = removal;
instructions.back().function = fun_name;
symbol_table.insert(fun_symbol);
WHEN("Removing known symbol")

1
unit/goto-programs/goto_program_declaration.cpp
View File

@ -36,7 +36,6 @@ SCENARIO(
instructions.emplace_back(goto_program_instruction_typet::DECL);
code_declt declaration(var_a);
instructions.back().make_decl(declaration);
instructions.back().function = fun_name;
symbol_table.insert(fun_symbol);
WHEN("Declaring known symbol")

1
unit/goto-programs/goto_program_function_call.cpp
View File

@ -42,7 +42,6 @@ SCENARIO(
goto_functiont goto_function;
auto &instructions = goto_function.body.instructions;
instructions.emplace_back(goto_program_instruction_typet::FUNCTION_CALL);
instructions.back().function = fun_symbol_name;
var_symbol.type = type1;
var_symbol2.type = type2;

2
unit/goto-programs/goto_program_goto_target.cpp
View File

@ -35,11 +35,9 @@ SCENARIO(
auto &instructions = goto_function.body.instructions;
instructions.emplace_back(goto_program_instruction_typet::ASSERT);
instructions.back().make_assertion(x_le_10);
instructions.back().function = fun_name;
instructions.emplace_back(goto_program_instruction_typet::GOTO);
instructions.back().make_goto(instructions.begin());
instructions.back().function = fun_name;
symbol.type = type1;
symbol_table.insert(symbol);

1
unit/goto-programs/goto_program_symbol_type_table_consistency.cpp
View File

@ -36,7 +36,6 @@ SCENARIO(
auto &instructions = goto_function.body.instructions;
instructions.emplace_back(goto_program_instruction_typet::ASSERT);
instructions.back().make_assertion(x_le_10);
instructions.back().function = function_symbol.name;
symbol_table.insert(function_symbol);
WHEN("Symbol table has the right symbol type")

1
unit/goto-programs/goto_program_table_consistency.cpp
View File

@ -35,7 +35,6 @@ SCENARIO(
auto &instructions = goto_function.body.instructions;
instructions.emplace_back(goto_program_instruction_typet::ASSERT);
instructions.back().make_assertion(x_le_10);
instructions.back().function = function_symbol.name;
symbol_table.insert(function_symbol);
WHEN("Symbol table has the right symbol")