24#ifndef CPROVER_ANALYSES_FLOW_INSENSITIVE_ANALYSIS_H
25#define CPROVER_ANALYSES_FLOW_INSENSITIVE_ANALYSIS_H
30#include <unordered_set>
65 typedef std::unordered_set<exprt, irep_hash>
expr_sett;
204 const exprt &function,
213 const goto_functionst::function_mapt::const_iterator f_it,
262 state.get_reference_set(
ns, expr, expr_set);
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
std::unordered_set< exprt, irep_hash > expr_sett
exprt get_guard(locationt from, locationt to) const
virtual void output(const namespacet &, std::ostream &) const
virtual ~flow_insensitive_abstract_domain_baset()
virtual void initialize(const namespacet &ns)=0
virtual void clear(void)=0
virtual void get_reference_set(const namespacet &, const exprt &, expr_sett &expr_set)
flow_insensitive_abstract_domain_baset()
exprt get_return_lhs(locationt to) const
virtual bool transform(const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to)=0
goto_programt::const_targett locationt
functions_donet functions_done
std::set< locationt > seen_locations
virtual ~flow_insensitive_analysis_baset()
std::set< irep_idt > recursion_sett
virtual void output(const goto_functionst &goto_functions, std::ostream &out)
virtual void operator()(const irep_idt &function_id, const goto_programt &goto_program)
virtual void get_reference_set(const exprt &expr, expr_sett &expr_set)=0
locationt get_next(working_sett &working_set)
flow_insensitive_analysis_baset(const namespacet &_ns)
recursion_sett recursion_set
bool fixedpoint(const irep_idt &function_id, const goto_programt &goto_program, const goto_functionst &goto_functions)
bool seen(const locationt &l)
bool visit(const irep_idt &function_id, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
std::set< irep_idt > functions_donet
static locationt successor(locationt l)
virtual void update(const goto_programt &goto_program)
flow_insensitive_abstract_domain_baset::expr_sett expr_sett
bool do_function_call_rec(const irep_idt &calling_function, locationt l_call, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
goto_programt::const_targett locationt
virtual void initialize(const goto_programt &)
std::priority_queue< locationt > working_sett
std::map< locationt, unsigned > statistics
virtual void initialize(const goto_functionst &)
void put_in_working_set(working_sett &working_set, locationt l)
virtual const statet & get_state() const =0
bool do_function_call(const irep_idt &calling_function, locationt l_call, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state)
flow_insensitive_abstract_domain_baset statet
virtual statet & get_state()=0
void get_reference_set(const exprt &expr, expr_sett &expr_set)
goto_programt::const_targett locationt
flow_insensitive_analysist(const namespacet &_ns)
virtual statet & get_state()
virtual const statet & get_state() const
const T & get_data() const
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Goto Programs with Functions.