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
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