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"))
41  : flow_sensitivityt::sensitive;
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 }
VALUE_SET_OF_POINTERS
@ VALUE_SET_OF_POINTERS
Definition: variable_sensitivity_configuration.h:24
optionst
Definition: options.h:23
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
vsd_configt::value_option_mappings
static const option_mappingt value_option_mappings
Definition: variable_sensitivity_configuration.h:93
CONSTANT
@ CONSTANT
Definition: variable_sensitivity_configuration.h:20
vsd_configt::value_set
static vsd_configt value_set()
Definition: variable_sensitivity_configuration.cpp:57
ARRAY_INSENSITIVE
@ ARRAY_INSENSITIVE
Definition: variable_sensitivity_configuration.h:23
vsd_configt
Definition: variable_sensitivity_configuration.h:41
UNION_INSENSITIVE
@ UNION_INSENSITIVE
Definition: variable_sensitivity_configuration.h:30
flow_sensitivityt::sensitive
@ sensitive
vsd_configt::pointer_option_mappings
static const option_mappingt pointer_option_mappings
Definition: variable_sensitivity_configuration.h:94
VALUE_SET
@ VALUE_SET
Definition: variable_sensitivity_configuration.h:31
INTERVAL
@ INTERVAL
Definition: variable_sensitivity_configuration.h:21
vsd_configt::from_options
static vsd_configt from_options(const optionst &options)
Definition: variable_sensitivity_configuration.cpp:13
ARRAY_SENSITIVE
@ ARRAY_SENSITIVE
Definition: variable_sensitivity_configuration.h:22
vsd_configt::struct_option_mappings
static const option_mappingt struct_option_mappings
Definition: variable_sensitivity_configuration.h:95
vsd_configt::array_option_mappings
static const option_mappingt array_option_mappings
Definition: variable_sensitivity_configuration.h:96
vsd_configt::invalid_argument
static invalid_command_line_argument_exceptiont invalid_argument(const std::string &option_name, const std::string &bad_argument, const option_mappingt &mapping)
Definition: variable_sensitivity_configuration.cpp:99
vsd_configt::option_mappingt
std::map< std::string, ABSTRACT_OBJECT_TYPET > option_mappingt
Definition: variable_sensitivity_configuration.h:80
vsd_configt::intervals
static vsd_configt intervals()
Definition: variable_sensitivity_configuration.cpp:67
vsd_configt::option_to_abstract_type
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)
Definition: variable_sensitivity_configuration.cpp:116
vsd_configt::constant_domain
static vsd_configt constant_domain()
Definition: variable_sensitivity_configuration.cpp:46
config
configt config
Definition: config.cpp:24
POINTER_SENSITIVE
@ POINTER_SENSITIVE
Definition: variable_sensitivity_configuration.h:25
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
POINTER_INSENSITIVE
@ POINTER_INSENSITIVE
Definition: variable_sensitivity_configuration.h:26
ABSTRACT_OBJECT_TYPET
ABSTRACT_OBJECT_TYPET
Definition: variable_sensitivity_configuration.h:18
STRUCT_SENSITIVE
@ STRUCT_SENSITIVE
Definition: variable_sensitivity_configuration.h:27
vsd_configt::union_option_mappings
static const option_mappingt union_option_mappings
Definition: variable_sensitivity_configuration.h:97
variable_sensitivity_configuration.h
Captures the user-supplied configuration for VSD, determining which domain abstractions are used,...
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:38
STRUCT_INSENSITIVE
@ STRUCT_INSENSITIVE
Definition: variable_sensitivity_configuration.h:28