12 #ifndef CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H 13 #define CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H 26 #define OPT_SHOW_PROPERTIES \ 29 #define HELP_SHOW_PROPERTIES \ 30 " --show-properties show the properties, but don't run analysis\n" // NOLINT(*) 66 #endif // CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H
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
nonstd::optional< T > optionalt
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
A collection of goto functions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
void show_properties(const goto_modelt &, message_handlert &message_handler, ui_message_handlert::uit ui)
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. ...
A generic container class for the GOTO intermediate representation of one function.