cprover
goto_harness_generator_factory.cpp
Go to the documentation of this file.
1 /******************************************************************\
2 
3 Module: goto_harness_generator_factory
4 
5 Author: Diffblue Ltd.
6 
7 \******************************************************************/
8 
10 
11 #include <util/exception_utils.h>
12 #include <util/invariant.h>
13 #include <util/make_unique.h>
14 #include <util/string_utils.h>
15 
16 #include <algorithm>
17 #include <functional>
18 #include <iterator>
19 #include <sstream>
20 #include <string>
21 
23  std::string generator_name,
24  build_generatort build_generator)
25 {
26  PRECONDITION(generators.find(generator_name) == generators.end());
27  auto res = generators.insert({generator_name, build_generator});
28  CHECK_RETURN(res.second);
29 }
30 
31 std::unique_ptr<goto_harness_generatort>
33  const std::string &generator_name,
34  const generator_optionst &generator_options,
35  const goto_modelt &goto_model)
36 {
37  auto it = generators.find(generator_name);
38 
39  if(it != generators.end())
40  {
41  auto generator = it->second();
42  for(const auto &option : generator_options)
43  {
44  generator->handle_option(option.first, option.second);
45  }
46  generator->validate_options(goto_model);
47 
48  return generator;
49  }
50  else
51  {
53  "unknown generator type",
56  std::ostringstream(),
57  generators.begin(),
58  generators.end(),
59  ", ",
60  [](const std::pair<std::string, build_generatort> &value) {
61  return value.first;
62  })
63  .str());
64  }
65 }
exception_utils.h
GOTO_HARNESS_GENERATOR_TYPE_OPT
#define GOTO_HARNESS_GENERATOR_TYPE_OPT
Definition: goto_harness_generator_factory.h:19
goto_harness_generator_factoryt::generators
std::map< std::string, build_generatort > generators
Definition: goto_harness_generator_factory.h:55
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
string_utils.h
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_harness_generator_factory.h
invariant.h
goto_modelt
Definition: goto_model.h:26
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
make_unique.h
join_strings
Stream & join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter, TransformFunc &&transform_func)
Prints items to an stream, separated by a constant delimiter.
Definition: string_utils.h:64
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
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
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38