Skip to content

Re-enable old function signatures for test-gen compat #1383

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.

Sign up for GitHub

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 1 commit into from
Sep 14, 2017
Merged

Re-enable old function signatures for test-gen compat #1383

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
9 changes: 7 additions & 2 deletions src/analyses/call_graph.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,9 +18,14 @@ call_grapht::call_grapht()
{
}

call_grapht::call_grapht(const goto_modelt &goto_model)
call_grapht::call_grapht(const goto_modelt &goto_model):
call_grapht(goto_model.goto_functions)
{
forall_goto_functions(f_it, goto_model.goto_functions)
}

call_grapht::call_grapht(const goto_functionst &goto_functions)
{
forall_goto_functions(f_it, goto_functions)
{
const goto_programt &body=f_it->second.body;
add(f_it->first, body);
Expand Down
1 change: 1 addition & 0 deletions src/analyses/call_graph.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ class call_grapht
public:
call_grapht();
explicit call_grapht(const goto_modelt &);
explicit call_grapht(const goto_functionst &);

void output_dot(std::ostream &out) const;
void output(std::ostream &out) const;
Expand Down
6 changes: 6 additions & 0 deletions src/goto-instrument/nondet_static.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,12 @@ Date: November 2011
#define CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H

class goto_modelt;
class namespacet;
class goto_functionst;

void nondet_static(
Copy link
Contributor

Choose a reason for hiding this comment

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

This appears to be missing an implementation? Perhaps it isn't needed?

Copy link
Contributor

Choose a reason for hiding this comment

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

Nope never deleted.

const namespacet &ns,
goto_functionst &goto_functions);

void nondet_static(goto_modelt &);

Expand Down
17 changes: 15 additions & 2 deletions src/goto-programs/remove_static_init_loops.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -109,6 +109,19 @@ void remove_static_init_loops(
optionst &options,
message_handlert &msg)
{
remove_static_init_loopst remove_loops(goto_model.symbol_table);
remove_loops.unwind_enum_static(goto_model.goto_functions, options, msg);
remove_static_init_loops(
goto_model.symbol_table,
goto_model.goto_functions,
options,
msg);
}

void remove_static_init_loops(
const symbol_tablet &symbol_table,
const goto_functionst &goto_functions,
optionst &options,
message_handlert &msg)
{
remove_static_init_loopst remove_loops(symbol_table);
remove_loops.unwind_enum_static(goto_functions, options, msg);
}
8 changes: 8 additions & 0 deletions src/goto-programs/remove_static_init_loops.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,10 +19,18 @@ Author: Daniel Kroening, [email protected]
#include <util/symbol_table.h>

class goto_modelt;
class symbol_tablet;
class goto_functionst;

void remove_static_init_loops(
const goto_modelt &,
optionst &,
message_handlert &);

void remove_static_init_loops(
const symbol_tablet &symbol_table,
const goto_functionst &goto_functions,
optionst &,
message_handlert &);

#endif // CPROVER_GOTO_PROGRAMS_REMOVE_STATIC_INIT_LOOPS_H
6 changes: 6 additions & 0 deletions src/goto-programs/show_goto_functions.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,13 +16,19 @@ Author: Peter Schrammel

class namespacet;
class goto_modelt;
class goto_functionst;

#define OPT_SHOW_GOTO_FUNCTIONS \
"(show-goto-functions)"

#define HELP_SHOW_GOTO_FUNCTIONS \
" --show-goto-functions show goto program\n"

void show_goto_functions(
const namespacet &ns,
Copy link
Contributor

Choose a reason for hiding this comment

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

This appears to be missing an implementation? Perhaps it isn't needed?

Copy link
Contributor

Choose a reason for hiding this comment

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

Nope never deleted

ui_message_handlert::uit ui,
const goto_functionst &goto_functions);

void show_goto_functions(
const goto_modelt &,
ui_message_handlert::uit ui);
Expand Down
7 changes: 7 additions & 0 deletions src/goto-programs/show_properties.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,9 +16,16 @@ Author: Daniel Kroening, [email protected]

class namespacet;
class goto_modelt;
class symbol_tablet;
class goto_functionst;

void show_properties(
const goto_modelt &,
ui_message_handlert::uit ui);

void show_properties(
Copy link
Contributor

Choose a reason for hiding this comment

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

This appears to be missing an implementation? Perhaps it isn't needed?

Copy link
Contributor

Choose a reason for hiding this comment

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

Nope, never deleted.

const namespacet &ns,
ui_message_handlert::uit ui,
const goto_functionst &goto_functions);

#endif // CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H