CBMC
goto_harness_generator.cpp
Go to the documentation of this file.
1 /******************************************************************\
2 
3 Module: goto_harness_generator
4 
5 Author: Diffblue Ltd.
6 
7 \******************************************************************/
8 
10 
11 #include <list>
12 #include <string>
13 
14 #include <util/exception_utils.h>
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);
46  auto value = string2optional<std::size_t>(string_value, 10);
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
exception_utils.h
invariant.h
goto_harness_generator.h
harness_options_parser::require_exactly_one_value
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...
Definition: goto_harness_generator.cpp:21
string2int.h
harness_options_parser
Definition: goto_harness_generator.cpp:19
PRECONDITION_WITH_DIAGNOSTICS
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:464
harness_options_parser::require_one_size_value
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...
Definition: goto_harness_generator.cpp:41
harness_options_parser::assert_no_values
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.
Definition: goto_harness_generator.cpp:34
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:50