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 #define OPT_SHOW_GOTO_FUNCTIONS \
21  "(show-goto-functions)" \
22  "(list-goto-functions)"
23 
24 #define HELP_SHOW_GOTO_FUNCTIONS \
25  " {y--show-goto-functions} \t show loaded goto program\n" \
26  " {y--list-goto-functions} \t list loaded goto functions\n"
27 
28 void show_goto_functions(
29  const namespacet &ns,
30  ui_message_handlert &ui_message_handler,
31  const goto_functionst &goto_functions,
32  bool list_only);
33 
34 void show_goto_functions(
35  const goto_modelt &,
36  ui_message_handlert &ui_message_handler,
37  bool list_only);
38 
39 #endif // CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_H
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
goto_modelt
Definition: goto_model.h:27
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
ui_message_handlert
Definition: ui_message.h:22
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