cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
9
#include "
goto_harness_generator_factory.h
"
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
17
void
goto_harness_generator_factoryt::register_generator
(
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>
27
goto_harness_generator_factoryt::factory
(
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
{
47
throw
invalid_command_line_argument_exceptiont
(
48
"unknown generator type"
,
49
"--"
GOTO_HARNESS_GENERATOR_TYPE_OPT
,
50
join_strings
(
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
}
goto_harness_generator_factoryt::generators
std::map< std::string, build_generatort > generators
Definition
goto_harness_generator_factory.h:57
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:37
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:27
goto_harness_generator_factoryt::generator_optionst
std::map< std::string, std::list< std::string > > generator_optionst
Definition
goto_harness_generator_factory.h:40
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:17
goto_modelt
Definition
goto_model.h:27
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:51
exception_utils.h
goto_harness_generator.h
goto_harness_generator_factory.h
GOTO_HARNESS_GENERATOR_TYPE_OPT
#define GOTO_HARNESS_GENERATOR_TYPE_OPT
Definition
goto_harness_generator_factory.h:21
invariant.h
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition
invariant.h:495
PRECONDITION
#define PRECONDITION(CONDITION)
Definition
invariant.h:463
string_utils.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:61
goto-harness
goto_harness_generator_factory.cpp
Generated by
1.17.0