CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
goto_harness_generator.cpp
Go to the documentation of this file.
1/******************************************************************\
2
3Module: goto_harness_generator
4
5Author: Diffblue Ltd.
6
7\******************************************************************/
8
10
11#include <list>
12#include <string>
13
15#include <util/invariant.h>
16#include <util/string2int.h>
17
18// NOLINTNEXTLINE(readability/namespace)
20{
22 const std::string &option,
23 const std::list<std::string> &values)
24{
25 if(values.size() != 1)
26 {
27 throw invalid_command_line_argument_exceptiont{"expected exactly one value",
28 "--" + option};
29 }
30
31 return values.front();
32}
33
35 const std::string &option,
36 const std::list<std::string> &values)
37{
38 PRECONDITION_WITH_DIAGNOSTICS(values.empty(), option);
39}
40
42 const std::string &option,
43 const std::list<std::string> &values)
44{
45 auto const string_value = require_exactly_one_value(option, values);
47 if(value.has_value())
48 {
49 return value.value();
50 }
51 else
52 {
54 "failed to parse '" + string_value + "' as integer", "--" + option};
55 }
56}
57// NOLINTNEXTLINE(readability/namespace)
58} // namespace harness_options_parser
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
std::string require_exactly_one_value(const std::string &option, const std::list< std::string > &values)
Returns the only value of a single element list, throws an exception if not passed a single element l...
void assert_no_values(const std::string &option, const std::list< std::string > &values)
Asserts that the list of values to an option passed is empty.
std::size_t require_one_size_value(const std::string &option, const std::list< std::string > &values)
Returns the only Nat value of a single element list, throws an exception if not passed a single eleme...
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition invariant.h:464