cprover
show_properties.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Show the properties
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H
13 #define CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H
14 
15 #include <util/ui_message.h>
16 #include <util/optional.h>
17 
18 class namespacet;
19 class goto_modelt;
20 class symbol_tablet;
21 class goto_programt;
22 class goto_functionst;
23 class message_handlert;
24 
25 // clang-format off
26 #define OPT_SHOW_PROPERTIES \
27  "(show-properties)"
28 
29 #define HELP_SHOW_PROPERTIES \
30  " --show-properties show the properties, but don't run analysis\n" // NOLINT(*)
31 // clang-format on
32 
33 void show_properties(
34  const goto_modelt &,
35  ui_message_handlert &ui_message_handler);
36 
37 void show_properties(
38  const namespacet &ns,
39  ui_message_handlert &ui_message_handler,
40  const goto_functionst &goto_functions);
41 
50  const irep_idt &property,
51  const goto_functionst &goto_functions);
52 
59  json_arrayt &json_properties,
60  const namespacet &ns,
61  const irep_idt &identifier,
62  const goto_programt &goto_program);
63 
64 #endif // CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
ui_message_handlert
Definition: ui_message.h:20
convert_properties_json
void convert_properties_json(json_arrayt &json_properties, const namespacet &ns, const irep_idt &identifier, const goto_programt &goto_program)
Collects the properties in the goto program into a json_arrayt
Definition: show_properties.cpp:111
optional.h
goto_modelt
Definition: goto_model.h:26
json_arrayt
Definition: json.h:165
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
show_properties
void show_properties(const goto_modelt &, ui_message_handlert &ui_message_handler)
Definition: show_properties.cpp:175
message_handlert
Definition: message.h:28
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
find_property
optionalt< source_locationt > find_property(const irep_idt &property, const goto_functionst &goto_functions)
Returns a source_locationt that corresponds to the property given by an irep_idt.
Definition: show_properties.cpp:25
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
ui_message.h