Skip to content

expand goto_programt and goto_functionst templates #1835

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Feb 20, 2018
Merged
Show file tree
Hide file tree
Changes from all commits
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
2 changes: 2 additions & 0 deletions src/analyses/constant_propagator.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,8 @@ Author: Peter Schrammel
#include <util/simplify_expr.h>
#include <util/cprover_prefix.h>

#include <langapi/language_util.h>

Copy link
Collaborator

Choose a reason for hiding this comment

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

What does this change have to do with the subject of the PR?

Copy link
Member Author

Choose a reason for hiding this comment

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

It was a missing header, which was hidden by the fact that goto_program_template.h included it.

void constant_propagator_domaint::assign_rec(
valuest &values,
const exprt &lhs,
Expand Down
2 changes: 2 additions & 0 deletions src/analyses/custom_bitvector_analysis.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
#include <util/xml_expr.h>
#include <util/simplify_expr.h>

#include <langapi/language_util.h>

#include <iostream>

void custom_bitvector_domaint::set_bit(
Expand Down
2 changes: 2 additions & 0 deletions src/analyses/goto_check.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,8 @@ Author: Daniel Kroening, [email protected]
#include <util/cprover_prefix.h>
#include <util/options.h>

#include <langapi/language_util.h>

#include "local_bitvector_analysis.h"

class goto_checkt
Expand Down
2 changes: 2 additions & 0 deletions src/analyses/goto_rw.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,8 @@ Date: April 2010
#include <util/simplify_expr.h>
#include <util/make_unique.h>

#include <langapi/language_util.h>

#include <goto-programs/goto_functions.h>

#include <pointer-analysis/goto_program_dereference.h>
Expand Down
1 change: 1 addition & 0 deletions src/analyses/interval_domain.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]

#ifdef DEBUG
#include <iostream>
#include <langapi/language_util.h>
#endif

#include <util/simplify_expr.h>
Expand Down
3 changes: 3 additions & 0 deletions src/cbmc/bmc_cover.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
#include "bmc.h"

#include <chrono>
#include <iomanip>

#include <util/xml.h>
#include <util/xml_expr.h>
Expand All @@ -25,6 +26,8 @@ Author: Daniel Kroening, [email protected]
#include <goto-programs/xml_goto_trace.h>
#include <goto-programs/json_goto_trace.h>

#include <langapi/language_util.h>

#include "bv_cbmc.h"

class bmc_covert:
Expand Down
3 changes: 3 additions & 0 deletions src/cbmc/symex_coverage.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ Date: March 2016

#include "symex_coverage.h"

#include <ctime>
#include <chrono>
#include <iostream>
#include <fstream>
Expand All @@ -23,6 +24,8 @@ Date: March 2016
#include <util/cprover_prefix.h>
#include <util/prefix.h>

#include <langapi/language_util.h>

#include <goto-programs/goto_functions.h>
#include <goto-programs/remove_returns.h>

Expand Down
2 changes: 2 additions & 0 deletions src/goto-instrument/call_sequences.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,8 @@ Date: April 2013

#include <goto-programs/goto_model.h>

#include <langapi/language_util.h>

void show_call_sequences(
const irep_idt &caller,
const goto_programt &goto_program)
Expand Down
2 changes: 2 additions & 0 deletions src/goto-instrument/cover_instrument_condition.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,8 @@ Author: Daniel Kroening

#include "cover_instrument.h"

#include <langapi/language_util.h>

#include "cover_util.h"

void cover_condition_instrumentert::instrument(
Expand Down
2 changes: 2 additions & 0 deletions src/goto-instrument/cover_instrument_decision.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,8 @@ Author: Daniel Kroening

#include "cover_instrument.h"

#include <langapi/language_util.h>

#include "cover_util.h"

void cover_decision_instrumentert::instrument(
Expand Down
2 changes: 2 additions & 0 deletions src/goto-instrument/cover_instrument_mcdc.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,8 @@ Author: Daniel Kroening

#include "cover_instrument.h"

#include <langapi/language_util.h>

#include <algorithm>

#include "cover_util.h"
Expand Down
2 changes: 2 additions & 0 deletions src/goto-instrument/cover_instrument_other.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,8 @@ Author: Daniel Kroening

#include "cover_instrument.h"

#include <langapi/language_util.h>

#include "cover_util.h"

void cover_path_instrumentert::instrument(
Expand Down
2 changes: 2 additions & 0 deletions src/goto-instrument/dot.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,8 @@ Author: Daniel Kroening, [email protected]
#include <fstream>
#include <sstream>

#include <langapi/language_util.h>

#define DOTGRAPHSETTINGS "color=black;" \
"orientation=portrait;" \
"fontsize=20;"\
Expand Down
2 changes: 1 addition & 1 deletion src/goto-instrument/wmm/goto2graph.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1301,7 +1301,7 @@ bool instrumentert::is_cfg_spurious(const event_grapht::critical_cyclet &cyc)

/* now test whether this part of the code can exist */
goto_functionst::function_mapt map;
goto_function_templatet<goto_programt> one_interleaving;
goto_functiont one_interleaving;
Copy link
Collaborator

Choose a reason for hiding this comment

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

Yes; this shouldn't have ever been like this.

one_interleaving.body.copy_from(interleaving);
map.insert(std::make_pair(
goto_functionst::entry_point(),
Expand Down
4 changes: 3 additions & 1 deletion src/goto-programs/builtin_functions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]

#include <cassert>

#include <util/c_types.h>
#include <util/rational.h>
#include <util/replace_expr.h>
#include <util/rational_tools.h>
Expand All @@ -29,9 +30,10 @@ Author: Daniel Kroening, [email protected]

#include <linking/zero_initializer.h>

#include <util/c_types.h>
#include <ansi-c/string_constant.h>

#include <langapi/language_util.h>

#include "format_strings.h"
#include "class_identifier.h"

Expand Down
64 changes: 63 additions & 1 deletion src/goto-programs/goto_functions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,70 @@ Date: June 2003

#include "goto_functions.h"

void goto_functionst::output(
const namespacet &ns,
std::ostream &out) const
{
for(const auto &fun : function_map)
{
if(fun.second.body_available())
{
out << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n";

const symbolt &symbol=ns.lookup(fun.first);
out << symbol.display_name() << " /* " << symbol.name << " */\n";
fun.second.body.output(ns, symbol.name, out);

out << std::flush;
}
}
}

void goto_functionst::compute_location_numbers()
{
unused_location_number = 0;
for(auto &func : function_map)
{
// Side-effect: bumps unused_location_number.
func.second.body.compute_location_numbers(unused_location_number);
}
}

void goto_functionst::compute_location_numbers(
goto_programt &program)
{
// Renumber just this single function. Use fresh numbers in case it has
// grown since it was last numbered.
program.compute_location_numbers(unused_location_number);
}

void goto_functionst::compute_incoming_edges()
{
for(auto &func : function_map)
{
func.second.body.compute_incoming_edges();
}
}

void goto_functionst::compute_target_numbers()
{
for(auto &func : function_map)
{
func.second.body.compute_target_numbers();
}
}

void goto_functionst::compute_loop_numbers()
{
for(auto &func : function_map)
{
func.second.body.compute_loop_numbers();
}
}


void get_local_identifiers(
const goto_function_templatet<goto_programt> &goto_function,
const goto_functiont &goto_function,
std::set<irep_idt> &dest)
{
goto_function.body.get_decl_identifiers(dest);
Expand Down
Loading