Go to the documentation of this file.
12 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DEPENDENCE_GRAPH_H
13 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DEPENDENCE_GRAPH_H
158 node_id != std::numeric_limits<node_indext>::max(),
159 "Check for the old uninitialised value");
175 return a->location_number < b->location_number;
179 map<goto_programt::const_targett, std::set<exprt>, dependency_ordert>
219 public grapht<vs_dep_nodet>
258 for(
const auto &location_state :
261 std::static_pointer_cast<variable_sensitivity_dependence_domaint>(
262 location_state.second)
263 ->populate_dep_graph(*
this, location_state.first);
287 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DEPENDENCE_GRAPH_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool merge(const variable_sensitivity_domaint &b, trace_ptrt from, trace_ptrt to) override
Computes the join between "this" and "b".
void make_bottom() override
no states
control_depst control_deps
void add_dep(vs_dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
void data_dependencies(goto_programt::const_targett from, goto_programt::const_targett to, variable_sensitivity_dependence_grapht &dep_graph, const namespacet &ns)
goto_programt::const_targett locationt
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Basic text output of the abstract domain.
bool operator()(const goto_programt::const_targett &a, const goto_programt::const_targett &b) const
bool is_bottom() const override
Find out if the domain is currently unreachable.
A generic directed graph with a parametric node type.
state_mapt & internal(void)
std::set< goto_programt::const_targett > control_dep_callst
std::map< goto_programt::const_targett, std::set< exprt >, dependency_ordert > data_depst
friend variable_sensitivity_dependence_domain_factoryt
data_depst domain_data_deps
Base class for all expressions.
An abstract interpreter, based on the default recursive-interprocedural that uses variable sensitivit...
bool is_top() const override
statet & get_state(trace_ptrt p, const ai_domain_factory_baset &fac) override
Look up the analysis state for a given history, instantiating a new domain if required.
ai_history_baset::trace_ptrt trace_ptrt
const goto_functionst & goto_functions
graph_nodet< vs_dep_edget >::edget edget
Compute dominators for CFG of goto_function.
void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
void make_entry() override
Make this domain a reasonable entry-point state.
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).
virtual statet & get_state(trace_ptrt p)
Get the state for the given history, creating it with the factory if it doesn't exist.
bool is_bottom() const override
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
friend variable_sensitivity_dependence_domaint
goto_programt::const_targett PC
void make_top() override
all states – the analysis doesn't use this, and domains may refuse to implement it.
std::shared_ptr< variable_sensitivity_object_factoryt > variable_sensitivity_object_factory_ptrt
std::unique_ptr< ai_domain_factory_baset > domain_factory
For creating domain objects.
std::set< goto_programt::const_targett > control_dep_candidatest
variable_sensitivity_dependence_grapht(const goto_functionst &goto_functions, const namespacet &_ns, variable_sensitivity_object_factory_ptrt object_factory, const vsd_configt &_configuration)
exprt object_factory(const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_table_baset &symbol_table, java_object_factory_parameterst parameters, lifetimet lifetime, const source_locationt &loc, const select_pointer_typet &pointer_type_selector, message_handlert &log)
Similar to gen_nondet_init below, but instead of allocating and non-deterministically initializing th...
void control_dependencies(const irep_idt &from_function, goto_programt::const_targett from, const irep_idt &to_function, goto_programt::const_targett to, variable_sensitivity_dependence_grapht &dep_graph)
void eval_data_deps(const exprt &expr, const namespacet &ns, data_depst &deps) const
Evaluate an expression and accumulate all the data dependencies involved in the evaluation.
void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
post_dominators_mapt post_dominators
bool is_top() const override
Is the domain completely top at this state.
The most conventional storage; one domain per location.
post_dominators_mapt & cfg_post_dominators()
std::map< goto_programt::const_targett, tvt > control_depst
grapht< vs_dep_nodet >::node_indext node_indext
bool merge_control_dependencies(const control_depst &other_control_deps, const control_dep_candidatest &other_control_dep_candidates, const control_dep_callst &other_control_dep_calls, const control_dep_callst &other_control_dep_call_candidates)
void populate_dep_graph(variable_sensitivity_dependence_grapht &, goto_programt::const_targett) const
virtual void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
A collection of goto functions.
jsont output_json(const ai_baset &ai, const namespacet &ns) const override
Outputs the current value of the domain.
A Template Class for Graphs.
variable_sensitivity_dependence_domaint(node_indext id, variable_sensitivity_object_factory_ptrt object_factory, const vsd_configt &configuration)
virtual statet & get_state(trace_ptrt p)
Get the state for the given history, creating it with the factory if it doesn't exist.
This class represents a node in a directed graph.
There are different ways of handling arrays, structures, unions and pointers.
This ensures that all domains are constructed with the node ID that links them to the graph part of t...
node_indext get_node_id() const
This is the basic interface of the abstract interpreter with default implementations of the core func...
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
graph_nodet< vs_dep_edget >::edgest edgest
void make_top() override
Sets the domain to top (all states).
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) override
Perform a context aware merge of the changes that have been applied between function_start and the cu...
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.
control_dep_callst control_dep_calls
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
virtual statet & get_state(locationt l)
control_dep_candidatest control_dep_candidates
control_dep_callst control_dep_call_candidates
variable_sensitivity_dependence_domaint & operator[](locationt l)