CBMC
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/string_utils.h>
14 
15 #include "goto_harness_generator.h"
16 
18  std::string generator_name,
19  build_generatort build_generator)
20 {
21  PRECONDITION(generators.find(generator_name) == generators.end());
22  auto res = generators.insert({generator_name, build_generator});
23  CHECK_RETURN(res.second);
24 }
25 
26 std::unique_ptr<goto_harness_generatort>
28  const std::string &generator_name,
29  const generator_optionst &generator_options,
30  const goto_modelt &goto_model)
31 {
32  auto it = generators.find(generator_name);
33 
34  if(it != generators.end())
35  {
36  auto generator = it->second();
37  for(const auto &option : generator_options)
38  {
39  generator->handle_option(option.first, option.second);
40  }
41  generator->validate_options(goto_model);
42 
43  return generator;
44  }
45  else
46  {
48  "unknown generator type",
51  std::ostringstream(),
52  generators.begin(),
53  generators.end(),
54  ", ",
55  [](const std::pair<std::string, build_generatort> &value) {
56  return value.first;
57  })
58  .str());
59  }
60 }
std::map< std::string, build_generatort > generators
std::map< std::string, std::list< std::string > > generator_optionst
std::function< std::unique_ptr< goto_harness_generatort >()> build_generatort
the type of a function that produces a goto-harness generator.
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.
void register_generator(std::string generator_name, build_generatort build_generator)
register a new goto-harness generator with the given name.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
#define GOTO_HARNESS_GENERATOR_TYPE_OPT
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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:61