CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
goto_harness_generator_factory.cpp
Go to the documentation of this file.
1/******************************************************************\
2
3Module: goto_harness_generator_factory
4
5Author: Diffblue Ltd.
6
7\******************************************************************/
8
10
12#include <util/invariant.h>
13#include <util/string_utils.h>
14
16
25
26std::unique_ptr<goto_harness_generatort>
28 const std::string &generator_name,
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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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.