Go to the documentation of this file.
64 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DOMAIN_H
65 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DOMAIN_H
165 bool is_top()
const override;
203 std::vector<irep_idt>
212 std::vector<symbol_exprt> modified_symbols,
238 auto d = util_make_unique<variable_sensitivity_domaint>(
241 return std::unique_ptr<statet>(d.release());
257 auto statistics = domain.gather_statistics(ns);
258 total_statistics.number_of_interval_abstract_objects +=
259 statistics.number_of_interval_abstract_objects;
260 total_statistics.number_of_globals += statistics.number_of_globals;
261 total_statistics.number_of_single_value_intervals +=
262 statistics.number_of_single_value_intervals;
263 total_statistics.number_of_constants += statistics.number_of_constants;
264 total_statistics.number_of_pointers += statistics.number_of_constants;
265 total_statistics.number_of_arrays += statistics.number_of_arrays;
266 total_statistics.number_of_structs += statistics.number_of_arrays;
267 total_statistics.objects_memory_usage += statistics.objects_memory_usage;
270 void print(std::ostream &out)
const
272 out <<
"<< Begin Variable Sensitivity Domain Statistics >>\n"
274 << total_statistics.objects_memory_usage.to_string() <<
'\n'
275 <<
" Number of structs: " << total_statistics.number_of_structs <<
'\n'
276 <<
" Number of arrays: " << total_statistics.number_of_arrays <<
'\n'
277 <<
" Number of pointers: " << total_statistics.number_of_pointers
279 <<
" Number of constants: " << total_statistics.number_of_constants
281 <<
" Number of intervals: "
282 << total_statistics.number_of_interval_abstract_objects <<
'\n'
283 <<
" Number of single value intervals: "
284 << total_statistics.number_of_single_value_intervals <<
'\n'
285 <<
" Number of globals: " << total_statistics.number_of_globals <<
'\n'
286 <<
"<< End Variable Sensitivity Domain Statistics >>\n";
291 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DOMAIN_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
sharing_ptrt< class abstract_objectt > abstract_object_pointert
#define CHECK_RETURN(CONDITION)
variable_sensitivity_domaint(variable_sensitivity_object_factory_ptrt _object_factory, const vsd_configt &_configuration)
bool is_bottom() const override
Find out if the domain is currently unreachable.
virtual bool merge(const variable_sensitivity_domaint &b, locationt from, locationt to)
Computes the join between "this" and "b".
bool ignore_function_call_transform(const irep_idt &function_id) const
Used to specify which CPROVER internal functions should be skipped over when doing function call tran...
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
Base class for all expressions.
variable_sensitivity_domain_factoryt(variable_sensitivity_object_factory_ptrt _object_factory, const vsd_configt &_configuration)
ai_history_baset::trace_ptrt trace_ptrt
std::vector< irep_idt > get_modified_symbols(const variable_sensitivity_domaint &other) const
Get symbols that have been modified since this domain and other.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void make_bottom() override
Sets the domain to bottom (no states / unreachable).
variable_sensitivity_object_factory_ptrt object_factory
const vsd_configt configuration
void apply_domain(std::vector< symbol_exprt > modified_symbols, const variable_sensitivity_domaint &target, const namespacet &ns)
Given a domain and some symbols, apply those symbols values to the current domain.
std::shared_ptr< variable_sensitivity_object_factoryt > variable_sensitivity_object_factory_ptrt
virtual void merge_three_way_function_return(const ai_domain_baset &function_call, const ai_domain_baset &function_start, const ai_domain_baset &function_end, const namespacet &ns)
Perform a context aware merge of the changes that have been applied between function_start and the cu...
abstract_environmentt abstract_state
An abstract version of a program environment.
std::unique_ptr< statet > make(locationt l) const override
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) override
Compute the abstract transformer for a single instruction.
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
bool is_top() const override
Is the domain completely top at this state.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Basic text output of the abstract domain.
goto_programt::const_targett locationt
bool ai_simplify(exprt &condition, const namespacet &ns) const override
Use the information in the domain to simplify the expression with respect to the current location.
This is the basic interface of the abstract interpreter with default implementations of the core func...
void make_entry() override
Set up a reasonable entry-point state.
ai_domain_baset::locationt locationt
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Captures the user-supplied configuration for VSD, determining which domain abstractions are used,...
void make_top() override
Sets the domain to top (all states).
flow_sensitivityt flow_sensitivity
void output(std::ostream &out) const
void transform_function_call(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
Used by variable_sensitivity_domaint::transform to handle FUNCTION_CALL transforms.