cprover
variable_sensitivity_configuration.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: variable sensitivity domain configuration
4 
5  Author: Jez Higgins
6 
7 \*******************************************************************/
12 
14 {
16 
17  config.value_abstract_type =
19 
20  config.pointer_abstract_type = option_to_abstract_type(
21  options, "pointers", pointer_option_mappings, POINTER_INSENSITIVE);
22 
23  config.struct_abstract_type = option_to_abstract_type(
24  options, "structs", struct_option_mappings, STRUCT_INSENSITIVE);
25 
26  config.array_abstract_type = option_to_abstract_type(
27  options, "arrays", array_option_mappings, ARRAY_INSENSITIVE);
28 
29  config.union_abstract_type = option_to_abstract_type(
30  options, "unions", union_option_mappings, UNION_INSENSITIVE);
31 
32  // This should always be on (for efficiency with 3-way merge)
33  config.context_tracking.last_write_context = true;
34  config.context_tracking.data_dependency_context =
35  options.get_bool_option("data-dependencies");
36  config.advanced_sensitivities.new_value_set =
37  options.get_bool_option("new-value-set");
38 
39  config.flow_sensitivity = (options.get_bool_option("flow-insensitive"))
42 
43  return config;
44 }
45 
47 {
49  config.context_tracking.last_write_context = true;
50  config.value_abstract_type = CONSTANT;
51  config.pointer_abstract_type = POINTER_SENSITIVE;
52  config.struct_abstract_type = STRUCT_SENSITIVE;
53  config.array_abstract_type = ARRAY_SENSITIVE;
54  return config;
55 }
56 
58 {
60  config.value_abstract_type = VALUE_SET;
61  config.pointer_abstract_type = VALUE_SET_OF_POINTERS;
62  config.struct_abstract_type = STRUCT_SENSITIVE;
63  config.array_abstract_type = ARRAY_SENSITIVE;
64  return config;
65 }
66 
68 {
70  config.context_tracking.last_write_context = true;
71  config.value_abstract_type = INTERVAL;
72  config.pointer_abstract_type = POINTER_SENSITIVE;
73  config.struct_abstract_type = STRUCT_SENSITIVE;
74  config.array_abstract_type = ARRAY_SENSITIVE;
75  return config;
76 }
77 
79  {"intervals", INTERVAL},
80  {"constants", CONSTANT},
81  {"set-of-constants", VALUE_SET}};
82 
84  {"top-bottom", POINTER_INSENSITIVE},
85  {"constants", POINTER_SENSITIVE},
86  {"value-set", VALUE_SET_OF_POINTERS}};
87 
89  {"top-bottom", STRUCT_INSENSITIVE},
90  {"every-field", STRUCT_SENSITIVE}};
91 
93  {"top-bottom", ARRAY_INSENSITIVE},
94  {"every-element", ARRAY_SENSITIVE}};
95 
97  {"top-bottom", UNION_INSENSITIVE}};
98 
100  const std::string &option_name,
101  const std::string &bad_argument,
102  const option_mappingt &mapping)
103 {
104  auto option = "--vsd-" + option_name;
105  auto choices = std::string("");
106  for(auto &kv : mapping)
107  {
108  choices += (!choices.empty() ? "|" : "");
109  choices += kv.first;
110  }
111 
113  "Unknown argument '" + bad_argument + "'", option, option + " " + choices};
114 }
115 
117  const optionst &options,
118  const std::string &option_name,
119  const option_mappingt &mapping,
120  ABSTRACT_OBJECT_TYPET default_type)
121 {
122  const auto argument = options.get_option(option_name);
123 
124  if(argument.empty())
125  return default_type;
126 
127  auto selected = mapping.find(argument);
128  if(selected == mapping.end())
129  {
130  throw invalid_argument(option_name, argument, mapping);
131  }
132  return selected->second;
133 }
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
configt config
Definition: config.cpp:24
std::map< std::string, ABSTRACT_OBJECT_TYPET > option_mappingt
static vsd_configt value_set()
static const option_mappingt array_option_mappings
static ABSTRACT_OBJECT_TYPET option_to_abstract_type(const optionst &options, const std::string &option_name, const option_mappingt &mapping, ABSTRACT_OBJECT_TYPET default_type)
static const option_mappingt struct_option_mappings
static const option_mappingt value_option_mappings
static const option_mappingt pointer_option_mappings
static const option_mappingt union_option_mappings
static vsd_configt intervals()
static vsd_configt from_options(const optionst &options)
static vsd_configt constant_domain()
static invalid_command_line_argument_exceptiont invalid_argument(const std::string &option_name, const std::string &bad_argument, const option_mappingt &mapping)
Captures the user-supplied configuration for VSD, determining which domain abstractions are used,...