show_properties.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Show the properties
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H
#define CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H
 
#include <util/irep.h>
#include <util/optional.h>
 
class json_arrayt;
class namespacet;
class goto_modelt;
class goto_programt;
class goto_functionst;
class source_locationt;
class ui_message_handlert;
 
// clang-format off
#define OPT_SHOW_PROPERTIES \
  "(show-properties)"
 
#define HELP_SHOW_PROPERTIES \
  " --show-properties            show the properties, but don't run analysis\n" // NOLINT(*)
// clang-format on
 
void show_properties(
  const goto_modelt &,
  ui_message_handlert &ui_message_handler);
 
void show_properties(
  const namespacet &ns,
  ui_message_handlert &ui_message_handler,
  const goto_functionst &goto_functions);
 
optionalt<source_locationt> find_property(
    const irep_idt &property,
    const goto_functionst &goto_functions);
 
void convert_properties_json(
  json_arrayt &json_properties,
  const namespacet &ns,
  const irep_idt &identifier,
  const goto_programt &goto_program);
 
#endif // CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H