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";
An abstract version of a program environment.
std::shared_ptr< variable_sensitivity_object_factoryt > variable_sensitivity_object_factory_ptrt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
This is the basic interface of the abstract interpreter with default implementations of the core func...
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
ai_history_baset::trace_ptrt trace_ptrt
goto_programt::const_targett locationt
ai_domain_baset::locationt locationt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::unique_ptr< statet > make(locationt l) const override
const vsd_configt configuration
variable_sensitivity_object_factory_ptrt object_factory
variable_sensitivity_domain_factoryt(variable_sensitivity_object_factory_ptrt _object_factory, const vsd_configt &_configuration)
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.
void make_bottom() override
Sets the domain to bottom (no states / unreachable).
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Basic text output of the abstract domain.
void make_top() override
Sets the domain to top (all states).
variable_sensitivity_domaint(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.
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.
abstract_environmentt abstract_state
void output(std::ostream &out) const
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
virtual bool merge(const variable_sensitivity_domaint &b, locationt from, locationt to)
Computes the join between "this" and "b".
std::vector< irep_idt > get_modified_symbols(const variable_sensitivity_domaint &other) const
Get symbols that have been modified since this domain and other.
bool is_bottom() const override
Find out if the domain is currently unreachable.
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...
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.
flow_sensitivityt flow_sensitivity
bool is_top() const override
Is the domain completely top at this state.
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...
void make_entry() override
Set up a reasonable entry-point state.
#define CHECK_RETURN(CONDITION)
Captures the user-supplied configuration for VSD, determining which domain abstractions are used,...