cprover
goto_harness_generator_factory.h
Go to the documentation of this file.
1 /******************************************************************\
2 
3 Module: goto_harness_generator_factory
4 
5 Author: Diffblue Ltd.
6 
7 \******************************************************************/
8 
9 #ifndef CPROVER_GOTO_HARNESS_GOTO_HARNESS_GENERATOR_FACTORY_H
10 #define CPROVER_GOTO_HARNESS_GOTO_HARNESS_GENERATOR_FACTORY_H
11 
12 #include <functional>
13 #include <map>
14 #include <memory>
15 #include <string>
16 
17 #include "goto_harness_generator.h"
18 
19 #define GOTO_HARNESS_GENERATOR_TYPE_OPT "harness-type"
20 #define GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT "harness-function-name"
21 
22 // clang-format off
23 #define GOTO_HARNESS_FACTORY_OPTIONS \
24  "(" GOTO_HARNESS_GENERATOR_TYPE_OPT "):" \
25  "(" GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT "):" \
26 // end GOTO_HARNESS_FACTORY_OPTIONS
27 
28 // clang-format on
29 
32 {
33 public:
36  std::function<std::unique_ptr<goto_harness_generatort>()>;
37 
38  using generator_optionst = std::map<std::string, std::list<std::string>>;
39 
43  void register_generator(
44  std::string generator_name,
45  build_generatort build_generator);
46 
49  std::unique_ptr<goto_harness_generatort> factory(
50  const std::string &generator_name,
51  const generator_optionst &generator_options,
52  const goto_modelt &goto_model);
53 
54 private:
55  std::map<std::string, build_generatort> generators;
56 };
57 
58 #endif // CPROVER_GOTO_HARNESS_GOTO_HARNESS_GENERATOR_FACTORY_H
goto_harness_generator_factoryt::generators
std::map< std::string, build_generatort > generators
Definition: goto_harness_generator_factory.h:55
goto_harness_generator_factoryt::build_generatort
std::function< std::unique_ptr< goto_harness_generatort >()> build_generatort
the type of a function that produces a goto-harness generator.
Definition: goto_harness_generator_factory.h:36
goto_modelt
Definition: goto_model.h:26
goto_harness_generator.h
goto_harness_generator_factoryt::register_generator
void register_generator(std::string generator_name, build_generatort build_generator)
register a new goto-harness generator with the given name.
Definition: goto_harness_generator_factory.cpp:22
goto_harness_generator_factoryt::generator_optionst
std::map< std::string, std::list< std::string > > generator_optionst
Definition: goto_harness_generator_factory.h:38
goto_harness_generator_factoryt
helper to select harness type by name.
Definition: goto_harness_generator_factory.h:32
goto_harness_generator_factoryt::factory
std::unique_ptr< goto_harness_generatort > factory(const std::string &generator_name, const generator_optionst &generator_options, const goto_modelt &goto_model)
return a generator matching the generator name.
Definition: goto_harness_generator_factory.cpp:32