Skip to content

Commit 1264b4d

Browse files
committed
Re-enable old function signatures for test-gen compat
1 parent 63c9a1e commit 1264b4d

File tree

7 files changed

+50
-4
lines changed

7 files changed

+50
-4
lines changed

src/analyses/call_graph.cpp

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,9 +18,14 @@ call_grapht::call_grapht()
1818
{
1919
}
2020

21-
call_grapht::call_grapht(const goto_modelt &goto_model)
21+
call_grapht::call_grapht(const goto_modelt &goto_model):
22+
call_grapht(goto_model.goto_functions)
2223
{
23-
forall_goto_functions(f_it, goto_model.goto_functions)
24+
}
25+
26+
call_grapht::call_grapht(const goto_functionst &goto_functions)
27+
{
28+
forall_goto_functions(f_it, goto_functions)
2429
{
2530
const goto_programt &body=f_it->second.body;
2631
add(f_it->first, body);

src/analyses/call_graph.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ class call_grapht
2222
public:
2323
call_grapht();
2424
explicit call_grapht(const goto_modelt &);
25+
explicit call_grapht(const goto_functionst &);
2526

2627
void output_dot(std::ostream &out) const;
2728
void output(std::ostream &out) const;

src/goto-instrument/nondet_static.h

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,12 @@ Date: November 2011
1616
#define CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H
1717

1818
class goto_modelt;
19+
class namespacet;
20+
class goto_functionst;
21+
22+
void nondet_static(
23+
const namespacet &ns,
24+
goto_functionst &goto_functions);
1925

2026
void nondet_static(goto_modelt &);
2127

src/goto-programs/remove_static_init_loops.cpp

Lines changed: 15 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -109,6 +109,19 @@ void remove_static_init_loops(
109109
optionst &options,
110110
message_handlert &msg)
111111
{
112-
remove_static_init_loopst remove_loops(goto_model.symbol_table);
113-
remove_loops.unwind_enum_static(goto_model.goto_functions, options, msg);
112+
remove_static_init_loops(
113+
goto_model.symbol_table,
114+
goto_model.goto_functions,
115+
options,
116+
msg);
117+
}
118+
119+
void remove_static_init_loops(
120+
const symbol_tablet &symbol_table,
121+
const goto_functionst &goto_functions,
122+
optionst &options,
123+
message_handlert &msg)
124+
{
125+
remove_static_init_loopst remove_loops(symbol_table);
126+
remove_loops.unwind_enum_static(goto_functions, options, msg);
114127
}

src/goto-programs/remove_static_init_loops.h

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,10 +19,18 @@ Author: Daniel Kroening, [email protected]
1919
#include <util/symbol_table.h>
2020

2121
class goto_modelt;
22+
class symbol_tablet;
23+
class goto_functionst;
2224

2325
void remove_static_init_loops(
2426
const goto_modelt &,
2527
optionst &,
2628
message_handlert &);
2729

30+
void remove_static_init_loops(
31+
const symbol_tablet &symbol_table,
32+
const goto_functionst &goto_functions,
33+
optionst &,
34+
message_handlert &);
35+
2836
#endif // CPROVER_GOTO_PROGRAMS_REMOVE_STATIC_INIT_LOOPS_H

src/goto-programs/show_goto_functions.h

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,13 +16,19 @@ Author: Peter Schrammel
1616

1717
class namespacet;
1818
class goto_modelt;
19+
class goto_functionst;
1920

2021
#define OPT_SHOW_GOTO_FUNCTIONS \
2122
"(show-goto-functions)"
2223

2324
#define HELP_SHOW_GOTO_FUNCTIONS \
2425
" --show-goto-functions show goto program\n"
2526

27+
void show_goto_functions(
28+
const namespacet &ns,
29+
ui_message_handlert::uit ui,
30+
const goto_functionst &goto_functions);
31+
2632
void show_goto_functions(
2733
const goto_modelt &,
2834
ui_message_handlert::uit ui);

src/goto-programs/show_properties.h

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,16 @@ Author: Daniel Kroening, [email protected]
1616

1717
class namespacet;
1818
class goto_modelt;
19+
class symbol_tablet;
20+
class goto_functionst;
1921

2022
void show_properties(
2123
const goto_modelt &,
2224
ui_message_handlert::uit ui);
2325

26+
void show_properties(
27+
const namespacet &ns,
28+
ui_message_handlert::uit ui,
29+
const goto_functionst &goto_functions);
30+
2431
#endif // CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H

0 commit comments

Comments
 (0)