Skip to content
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions src/analyses/ai.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -122,7 +122,7 @@ void ai_baset::output(
find_state(i_it).output(out, *this, ns);
out << "\n";
#if 1
goto_program.output_instruction(ns, identifier, out, i_it);
goto_program.output_instruction(ns, identifier, out, *i_it);
out << "\n";
#endif
}
Expand Down Expand Up @@ -174,7 +174,7 @@ jsont ai_baset::output_json(

// Ideally we need output_instruction_json
std::ostringstream out;
goto_program.output_instruction(ns, identifier, out, i_it);
goto_program.output_instruction(ns, identifier, out, *i_it);
location["instruction"]=json_stringt(out.str());

contents.push_back(location);
Expand Down Expand Up @@ -235,7 +235,7 @@ xmlt ai_baset::output_xml(

// Ideally we need output_instruction_xml
std::ostringstream out;
goto_program.output_instruction(ns, identifier, out, i_it);
goto_program.output_instruction(ns, identifier, out, *i_it);
location.set_attribute("instruction", out.str());

function_body.new_element(location);
Expand Down
2 changes: 1 addition & 1 deletion src/analyses/local_bitvector_analysis.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -349,7 +349,7 @@ void local_bitvector_analysist::output(
}

out << "\n";
goto_function.body.output_instruction(ns, "", out, i_it);
goto_function.body.output_instruction(ns, "", out, *i_it);
out << "\n";

l++;
Expand Down
2 changes: 1 addition & 1 deletion src/analyses/local_may_alias.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -466,7 +466,7 @@ void local_may_aliast::output(
}

out << "\n";
goto_function.body.output_instruction(ns, "", out, i_it);
goto_function.body.output_instruction(ns, "", out, *i_it);
out << "\n";

l++;
Expand Down
4 changes: 2 additions & 2 deletions src/goto-analyzer/unreachable_instructions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ static void output_dead_plain(
for(dead_mapt::const_iterator it=dead_map.begin();
it!=dead_map.end();
++it)
goto_program.output_instruction(ns, "", os, it->second);
goto_program.output_instruction(ns, "", os, *it->second);
}

static void add_to_json(
Expand Down Expand Up @@ -101,7 +101,7 @@ static void add_to_json(
++it)
{
std::ostringstream oss;
goto_program.output_instruction(ns, "", oss, it->second);
goto_program.output_instruction(ns, "", oss, *it->second);
std::string s=oss.str();

std::string::size_type n=s.find('\n');
Expand Down
2 changes: 1 addition & 1 deletion src/goto-diff/change_impact.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -732,7 +732,7 @@ void change_impactt::output_instruction(char prefix,
else
{
std::cout << prefix;
goto_program.output_instruction(ns, function, std::cout, target);
goto_program.output_instruction(ns, function, std::cout, *target);
}
}

Expand Down
18 changes: 3 additions & 15 deletions src/goto-diff/unified_diff.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -132,27 +132,15 @@ void unified_difft::output_diff(
{
case differencet::SAME:
os << ' ';
new_goto_program.output_instruction(
ns_new,
identifier,
os,
d.first);
new_goto_program.output_instruction(ns_new, identifier, os, *d.first);
break;
case differencet::DELETED:
os << '-';
old_goto_program.output_instruction(
ns_old,
identifier,
os,
d.first);
old_goto_program.output_instruction(ns_old, identifier, os, *d.first);
break;
case differencet::NEW:
os << '+';
new_goto_program.output_instruction(
ns_new,
identifier,
os,
d.first);
new_goto_program.output_instruction(ns_new, identifier, os, *d.first);
break;
}
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ bool disjunctive_polynomial_accelerationt::accelerate(
{
if(loop.find(it)!=loop.end())
{
goto_program.output_instruction(ns, "scratch", std::cout, it);
goto_program.output_instruction(ns, "scratch", std::cout, *it);
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ bool enumerating_loop_accelerationt::accelerate(
it!=path.end();
++it)
{
goto_program.output_instruction(ns, "OMG", std::cout, it->loc);
goto_program.output_instruction(ns, "OMG", std::cout, *it->loc);
}
#endif

Expand Down
2 changes: 1 addition & 1 deletion src/goto-instrument/accelerate/path.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -22,5 +22,5 @@ void output_path(
std::ostream &str)
{
for(const auto &step : path)
program.output_instruction(ns, "path", str, step.loc);
program.output_instruction(ns, "path", str, *step.loc);
}
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ bool polynomial_acceleratort::accelerate(
it!=body.end();
++it)
{
program.output_instruction(ns, "scratch", std::cout, it);
program.output_instruction(ns, "scratch", std::cout, *it);
}

std::cout << "Modified:\n";
Expand Down
2 changes: 1 addition & 1 deletion src/goto-instrument/goto_instrument_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -250,7 +250,7 @@ int goto_instrument_parse_optionst::doit()

forall_goto_program_instructions(i_it, goto_program)
{
goto_program.output_instruction(ns, "", std::cout, i_it);
goto_program.output_instruction(ns, "", std::cout, *i_it);
std::cout << "Is threaded: " << (is_threaded(i_it)?"True":"False")
<< "\n\n";
}
Expand Down
2 changes: 1 addition & 1 deletion src/goto-instrument/unwind.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -328,7 +328,7 @@ void goto_unwindt::unwind(
symbol_tablet st;
namespacet ns(st);
std::cout << "Instruction:\n";
goto_program.output_instruction(ns, "", std::cout, i_it);
goto_program.output_instruction(ns, "", std::cout, *i_it);
#endif

if(!i_it->is_backwards_goto())
Expand Down
4 changes: 2 additions & 2 deletions src/goto-programs/goto_inline_class.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -444,7 +444,7 @@ void goto_inlinet::expand_function_call(

#ifdef DEBUG
std::cout << "Expanding call:\n";
dest.output_instruction(ns, "", std::cout, target);
dest.output_instruction(ns, "", std::cout, *target);
#endif

exprt lhs;
Expand Down Expand Up @@ -815,7 +815,7 @@ void goto_inlinet::output_inline_map(
bool transitive=call.second;

out << " Call:\n";
goto_program.output_instruction(ns, "", out, target);
goto_program.output_instruction(ns, "", out, *target);
out << " Transitive: " << transitive << "\n";
}
}
Expand Down
16 changes: 0 additions & 16 deletions src/goto-programs/goto_program.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -17,22 +17,6 @@ Author: Daniel Kroening, [email protected]

#include <langapi/language_util.h>

/// See below.
/// \param ns: the namespace to resolve the expressions in
/// \param identifier: the identifier used to find a symbol to identify the
/// source language
/// \param out: the stream to write the goto string to
/// \param it: an iterator pointing to the instruction to convert
/// \return See below.
std::ostream &goto_programt::output_instruction(
const class namespacet &ns,
const irep_idt &identifier,
std::ostream &out,
instructionst::const_iterator it) const
{
return output_instruction(ns, identifier, out, *it);
}

/// Writes to \p out a two/three line string representation of a given
/// \p instruction. The output is of the format:
/// ```
Expand Down
8 changes: 1 addition & 7 deletions src/goto-programs/goto_program.h
Original file line number Diff line number Diff line change
Expand Up @@ -28,13 +28,7 @@ class goto_programt:public goto_program_templatet<codet, exprt>
const class namespacet &ns,
const irep_idt &identifier,
std::ostream &out,
instructionst::const_iterator it) const;

std::ostream &output_instruction(
const class namespacet &ns,
const irep_idt &identifier,
std::ostream &out,
const instructiont &instruction) const;
const instructiont &instruction) const override;

goto_programt() { }

Expand Down
9 changes: 3 additions & 6 deletions src/goto-programs/goto_program_template.h
Original file line number Diff line number Diff line change
Expand Up @@ -503,7 +503,7 @@ class goto_program_templatet
const namespacet &ns,
const irep_idt &identifier,
std::ostream &out,
typename instructionst::const_iterator it) const=0;
const typename instructionst::value_type &it) const = 0;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit: I don't think we should have spaces around =

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I had let that one go in light of #1324.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, I was not aware of the discussion about the spaces around operators before reviewing this PR.


/// Compute the target numbers
void compute_target_numbers();
Expand Down Expand Up @@ -665,11 +665,8 @@ std::ostream &goto_program_templatet<codeT, guardT>::output(
{
// output program

for(typename instructionst::const_iterator
it=instructions.begin();
it!=instructions.end();
++it)
output_instruction(ns, identifier, out, it);
for(const auto &instruction : instructions)
output_instruction(ns, identifier, out, instruction);

return out;
}
Expand Down
2 changes: 1 addition & 1 deletion src/goto-programs/interpreter.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -114,7 +114,7 @@ void interpretert::show_state()
ns,
function->first,
status(),
pc);
*pc);

status() << eom;
}
Expand Down
2 changes: 1 addition & 1 deletion src/pointer-analysis/value_set_analysis_fivr.h
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ class value_set_analysis_fivrt:
out << "**** " << it->source_location << '\n';
output(it, out);
out << '\n';
goto_program.output_instruction(ns, "", out, it);
goto_program.output_instruction(ns, "", out, *it);
out << '\n';
}
}
Expand Down
2 changes: 1 addition & 1 deletion src/pointer-analysis/value_set_analysis_fivrns.h
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ class value_set_analysis_fivrnst:
out << "**** " << it->source_location << '\n';
output(it, out);
out << '\n';
goto_program.output_instruction(ns, "", out, it);
goto_program.output_instruction(ns, "", out, *it);
out << '\n';
}
}
Expand Down