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);
 
#define OPT_REPLACE_FUNCTION_BODY \
  "(generate-function-body):" \
  "(generate-havocing-body):" \
  "(generate-function-body-options):"
 
#define HELP_REPLACE_FUNCTION_BODY                                             \
  " {y--generate-function-body} {uregex} \t "                                  \
  "generate bodies for functions matching {uregex}\n"                          \
  " {y--generate-havocing-body} <option> "                                     \
  "{ufun_name},{yparams}:{up1};{up2};.. \t "                                   \
  "generate havocing body\n"                                                   \
  " {y--generate-havocing-body} <option> "                                     \
  "{ufun_name}[,{ucall-site-id},{yparams}:{up1};{up2};..]+ \t "                \
  "generate havocing body\n"                                                   \
  " {y--generate-function-body-options} {uoption} \t "                         \
  "One of {yassert-false}, {yassume-false}, {ynondet-return}, "                \
  "{yassert-false-assume-false} and "                                          \
  "{yhavoc}[,{yparams}:{uregex}][,{yglobals}:{uregex}]"                        \
  "[,{yparams}:{up1};{up2};..] (default: {ynondet-return})\n"
 
#endif // CPROVER_GOTO_PROGRAMS_GENERATE_FUNCTION_BODIES_H