CBMC
show_goto_functions.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Show the goto functions
4 
5 Author: Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_H
13 #define CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_H
14 
15 class namespacet;
16 class goto_modelt;
17 class goto_functionst;
18 class ui_message_handlert;
19 
20 // clang-format off
21 #define OPT_SHOW_GOTO_FUNCTIONS \
22  "(show-goto-functions)" \
23  "(list-goto-functions)"
24 
25 #define HELP_SHOW_GOTO_FUNCTIONS \
26  " --show-goto-functions show loaded goto program\n" \
27  " --list-goto-functions list loaded goto functions\n"
28 // clang-format on
29 
30 void show_goto_functions(
31  const namespacet &ns,
32  ui_message_handlert &ui_message_handler,
33  const goto_functionst &goto_functions,
34  bool list_only);
35 
36 void show_goto_functions(
37  const goto_modelt &,
38  ui_message_handlert &ui_message_handler,
39  bool list_only);
40 
41 #endif // CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_H
ui_message_handlert
Definition: ui_message.h:21
goto_modelt
Definition: goto_model.h:25
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
show_goto_functions
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
Definition: show_goto_functions.cpp:20
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:24