Skip to content

Commit ba8bbe2

Browse files
author
Daniel Kroening
committed
expand goto_programt and goto_functionst templates
The goto_program_template and the goto_functions_template each only have one instance, but make it much harder to read the code.
1 parent b36a90a commit ba8bbe2

29 files changed

+1074
-1148
lines changed

src/analyses/constant_propagator.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,8 @@ Author: Peter Schrammel
2020
#include <util/simplify_expr.h>
2121
#include <util/cprover_prefix.h>
2222

23+
#include <langapi/language_util.h>
24+
2325
void constant_propagator_domaint::assign_rec(
2426
valuest &values,
2527
const exprt &lhs,

src/analyses/custom_bitvector_analysis.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
1414
#include <util/xml_expr.h>
1515
#include <util/simplify_expr.h>
1616

17+
#include <langapi/language_util.h>
18+
1719
#include <iostream>
1820

1921
void custom_bitvector_domaint::set_bit(

src/analyses/goto_check.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,8 @@ Author: Daniel Kroening, [email protected]
2828
#include <util/cprover_prefix.h>
2929
#include <util/options.h>
3030

31+
#include <langapi/language_util.h>
32+
3133
#include "local_bitvector_analysis.h"
3234

3335
class goto_checkt

src/analyses/goto_rw.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,8 @@ Date: April 2010
2323
#include <util/simplify_expr.h>
2424
#include <util/make_unique.h>
2525

26+
#include <langapi/language_util.h>
27+
2628
#include <goto-programs/goto_functions.h>
2729

2830
#include <pointer-analysis/goto_program_dereference.h>

src/analyses/interval_domain.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
1313

1414
#ifdef DEBUG
1515
#include <iostream>
16+
#include <langapi/language_util.h>
1617
#endif
1718

1819
#include <util/simplify_expr.h>

src/cbmc/bmc_cover.cpp

+3
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
1212
#include "bmc.h"
1313

1414
#include <chrono>
15+
#include <iomanip>
1516

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

29+
#include <langapi/language_util.h>
30+
2831
#include "bv_cbmc.h"
2932

3033
class bmc_covert:

src/cbmc/symex_coverage.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,8 @@ Date: March 2016
2323
#include <util/cprover_prefix.h>
2424
#include <util/prefix.h>
2525

26+
#include <langapi/language_util.h>
27+
2628
#include <goto-programs/goto_functions.h>
2729
#include <goto-programs/remove_returns.h>
2830

src/goto-instrument/call_sequences.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,8 @@ Date: April 2013
2222

2323
#include <goto-programs/goto_model.h>
2424

25+
#include <langapi/language_util.h>
26+
2527
void show_call_sequences(
2628
const irep_idt &caller,
2729
const goto_programt &goto_program)

src/goto-instrument/cover_instrument_condition.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,8 @@ Author: Daniel Kroening
1111

1212
#include "cover_instrument.h"
1313

14+
#include <langapi/language_util.h>
15+
1416
#include "cover_util.h"
1517

1618
void cover_condition_instrumentert::instrument(

src/goto-instrument/cover_instrument_decision.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,8 @@ Author: Daniel Kroening
1111

1212
#include "cover_instrument.h"
1313

14+
#include <langapi/language_util.h>
15+
1416
#include "cover_util.h"
1517

1618
void cover_decision_instrumentert::instrument(

src/goto-instrument/cover_instrument_mcdc.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,8 @@ Author: Daniel Kroening
1111

1212
#include "cover_instrument.h"
1313

14+
#include <langapi/language_util.h>
15+
1416
#include <algorithm>
1517

1618
#include "cover_util.h"

src/goto-instrument/cover_instrument_other.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,8 @@ Author: Daniel Kroening
1111

1212
#include "cover_instrument.h"
1313

14+
#include <langapi/language_util.h>
15+
1416
#include "cover_util.h"
1517

1618
void cover_path_instrumentert::instrument(

src/goto-instrument/dot.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,8 @@ Author: Daniel Kroening, [email protected]
1515
#include <fstream>
1616
#include <sstream>
1717

18+
#include <langapi/language_util.h>
19+
1820
#define DOTGRAPHSETTINGS "color=black;" \
1921
"orientation=portrait;" \
2022
"fontsize=20;"\

src/goto-instrument/wmm/goto2graph.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -1301,7 +1301,7 @@ bool instrumentert::is_cfg_spurious(const event_grapht::critical_cyclet &cyc)
13011301

13021302
/* now test whether this part of the code can exist */
13031303
goto_functionst::function_mapt map;
1304-
goto_function_templatet<goto_programt> one_interleaving;
1304+
goto_functiont one_interleaving;
13051305
one_interleaving.body.copy_from(interleaving);
13061306
map.insert(std::make_pair(
13071307
goto_functionst::entry_point(),

src/goto-programs/builtin_functions.cpp

+3-1
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <cassert>
1515

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

3031
#include <linking/zero_initializer.h>
3132

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

35+
#include <langapi/language_util.h>
36+
3537
#include "format_strings.h"
3638
#include "class_identifier.h"
3739

src/goto-programs/goto_functions.cpp

+63-1
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,70 @@ Date: June 2003
1313

1414
#include "goto_functions.h"
1515

16+
void goto_functionst::output(
17+
const namespacet &ns,
18+
std::ostream &out) const
19+
{
20+
for(const auto &fun : function_map)
21+
{
22+
if(fun.second.body_available())
23+
{
24+
out << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n";
25+
26+
const symbolt &symbol=ns.lookup(fun.first);
27+
out << symbol.display_name() << " /* " << symbol.name << " */\n";
28+
fun.second.body.output(ns, symbol.name, out);
29+
30+
out << std::flush;
31+
}
32+
}
33+
}
34+
35+
void goto_functionst::compute_location_numbers()
36+
{
37+
unused_location_number = 0;
38+
for(auto &func : function_map)
39+
{
40+
// Side-effect: bumps unused_location_number.
41+
func.second.body.compute_location_numbers(unused_location_number);
42+
}
43+
}
44+
45+
void goto_functionst::compute_location_numbers(
46+
goto_programt &program)
47+
{
48+
// Renumber just this single function. Use fresh numbers in case it has
49+
// grown since it was last numbered.
50+
program.compute_location_numbers(unused_location_number);
51+
}
52+
53+
void goto_functionst::compute_incoming_edges()
54+
{
55+
for(auto &func : function_map)
56+
{
57+
func.second.body.compute_incoming_edges();
58+
}
59+
}
60+
61+
void goto_functionst::compute_target_numbers()
62+
{
63+
for(auto &func : function_map)
64+
{
65+
func.second.body.compute_target_numbers();
66+
}
67+
}
68+
69+
void goto_functionst::compute_loop_numbers()
70+
{
71+
for(auto &func : function_map)
72+
{
73+
func.second.body.compute_loop_numbers();
74+
}
75+
}
76+
77+
1678
void get_local_identifiers(
17-
const goto_function_templatet<goto_programt> &goto_function,
79+
const goto_functiont &goto_function,
1880
std::set<irep_idt> &dest)
1981
{
2082
goto_function.body.get_decl_identifiers(dest);

0 commit comments

Comments
 (0)