generate_function_bodies.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Replace bodies of goto functions
 
Author: Diffblue Ltd.
 
\*******************************************************************/
 
#ifndef CPROVER_GOTO_PROGRAMS_GENERATE_FUNCTION_BODIES_H
#define CPROVER_GOTO_PROGRAMS_GENERATE_FUNCTION_BODIES_H
 
#include <memory>
#include <regex>
 
#include <util/irep.h>
 
class goto_functiont;
class goto_modelt;
class message_handlert;
class symbol_tablet;
struct c_object_factory_parameterst;
 
class generate_function_bodiest
{
protected:
  virtual void generate_function_body_impl(
    goto_functiont &function,
    symbol_tablet &symbol_table,
    const irep_idt &function_name) const = 0;
 
public:
  virtual ~generate_function_bodiest() = default;
 
  void generate_function_body(
    goto_functiont &function,
    symbol_tablet &symbol_table,
    const irep_idt &function_name) const;
 
private:
  void generate_parameter_names(
    goto_functiont &function,
    symbol_tablet &symbol_table,
    const irep_idt &function_name) const;
};
 
std::unique_ptr<generate_function_bodiest> generate_function_bodies_factory(
  const std::string &options,
  const c_object_factory_parameterst &object_factory_parameters,
  const symbol_tablet &symbol_table,
  message_handlert &message_handler);
 
void generate_function_bodies(
  const std::regex &functions_regex,
  const generate_function_bodiest &generate_function_body,
  goto_modelt &model,
  message_handlert &message_handler);
 
void generate_function_bodies(
  const std::string &function_name,
  const std::string &call_site_id,
  const generate_function_bodiest &generate_function_body,
  goto_modelt &model,
  message_handlert &message_handler);
 
// clang-format off
#define OPT_REPLACE_FUNCTION_BODY \
  "(generate-function-body):" \
  "(generate-havocing-body):" \
  "(generate-function-body-options):"
 
#define HELP_REPLACE_FUNCTION_BODY \
  " --generate-function-body <regex>\n" \
  /* NOLINTNEXTLINE(whitespace/line_length) */ \
  "                              Generate bodies for functions matching regex\n" \
  " --generate-havocing-body <option>\n" \
  /* NOLINTNEXTLINE(whitespace/line_length) */ \
  "                              <fun_name>,params:<p_n1;p_n2;..>\n" \
  "                              or\n" \
  /* NOLINTNEXTLINE(whitespace/line_length) */ \
  "                              <fun_name>[,<call-site-id>,params:<p_n1;p_n2;..>]+\n" \
  " --generate-function-body-options <option>\n" \
  "                              One of assert-false, assume-false,\n" \
  /* NOLINTNEXTLINE(whitespace/line_length) */ \
  "                              nondet-return, assert-false-assume-false and\n" \
  "                              havoc[,params:<regex>][,globals:<regex>]\n" \
  "                                   [,params:<p_n1;p_n2;..>]\n" \
  "                              (default: nondet-return)\n"
// clang-format on
 
#endif // CPROVER_GOTO_PROGRAMS_GENERATE_FUNCTION_BODIES_H