goto_harness_generator_factory.h

Go to the documentation of this file.

/******************************************************************\
 
Module: goto_harness_generator_factory
 
Author: Diffblue Ltd.
 
\******************************************************************/
 
#ifndef CPROVER_GOTO_HARNESS_GOTO_HARNESS_GENERATOR_FACTORY_H
#define CPROVER_GOTO_HARNESS_GOTO_HARNESS_GENERATOR_FACTORY_H
 
#include <functional>
#include <list>
#include <map>
#include <memory>
#include <string>
 
class goto_harness_generatort;
class goto_modelt;
 
#define GOTO_HARNESS_GENERATOR_TYPE_OPT "harness-type"
#define GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT "harness-function-name"
 
// clang-format off
#define GOTO_HARNESS_FACTORY_OPTIONS                                           \
  "(" GOTO_HARNESS_GENERATOR_TYPE_OPT "):"                                     \
  "(" GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT "):"                    \
// end GOTO_HARNESS_FACTORY_OPTIONS
 
// clang-format on
 
class goto_harness_generator_factoryt
{
public:
  using build_generatort =
    std::function<std::unique_ptr<goto_harness_generatort>()>;
 
  using generator_optionst = std::map<std::string, std::list<std::string>>;
 
  void register_generator(
    std::string generator_name,
    build_generatort build_generator);
 
  std::unique_ptr<goto_harness_generatort> factory(
    const std::string &generator_name,
    const generator_optionst &generator_options,
    const goto_modelt &goto_model);
 
private:
  std::map<std::string, build_generatort> generators;
};
 
#endif // CPROVER_GOTO_HARNESS_GOTO_HARNESS_GENERATOR_FACTORY_H