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 <optional>
 
class json_arrayt;
class namespacet;
class goto_modelt;
class goto_programt;
class goto_functionst;
class source_locationt;
class ui_message_handlert;
 
#define OPT_SHOW_PROPERTIES \
  "(show-properties)"
 
#define HELP_SHOW_PROPERTIES                                                   \
  " {y--show-properties} \t show the properties, but don't run analysis\n"
 
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);

std::optional<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