13 #ifndef CPROVER_ANALYSES_FLOW_INSENSITIVE_ANALYSIS_H 14 #define CPROVER_ANALYSES_FLOW_INSENSITIVE_ANALYSIS_H 19 #include <unordered_set> 47 std::ostream &out)
const 51 typedef std::unordered_set<exprt, irep_hash>
expr_sett;
62 virtual void clear(
void)=0;
86 bool seen(
const locationt &l)
88 return (seen_locations.find(l)!=seen_locations.end());
119 virtual void operator()(
122 virtual void operator()(
142 output(goto_program,
"", out);
151 std::ostream &out)
const;
155 locationt get_next(working_sett &working_set);
158 working_sett &working_set,
170 goto_functionst::function_mapt::const_iterator it,
179 working_sett &working_set,
198 bool do_function_call_rec(
200 const exprt &
function,
205 bool do_function_call(
208 const goto_functionst::function_mapt::const_iterator f_it,
214 virtual statet &get_state()=0;
215 virtual const statet &get_state()
const=0;
221 expr_sett &expr_set)=0;
257 state.get_reference_set(ns, expr, expr_set);
265 #endif // CPROVER_ANALYSES_FLOW_INSENSITIVE_ANALYSIS_H
std::set< irep_idt > functions_donet
std::map< locationt, unsigned > statistics
exprt get_guard(locationt from, locationt to) const
std::set< locationt > seen_locations
Goto Programs with Functions.
functions_donet functions_done
virtual bool transform(const namespacet &ns, locationt from, locationt to)=0
std::unordered_set< exprt, irep_hash > expr_sett
virtual void output(const goto_programt &goto_program, std::ostream &out)
virtual statet & get_state()
virtual void output(const namespacet &ns, std::ostream &out) const
flow_insensitive_analysis_baset(const namespacet &_ns)
const T & get_data() const
goto_programt::const_targett locationt
virtual ~flow_insensitive_abstract_domain_baset()
virtual void initialize(const goto_functionst &goto_functions)
instructionst::const_iterator const_targett
flow_insensitive_abstract_domain_baset::expr_sett expr_sett
flow_insensitive_abstract_domain_baset()
flow_insensitive_abstract_domain_baset statet
std::set< irep_idt > recursion_sett
goto_programt::const_targett locationt
virtual void initialize(const goto_programt &goto_program)
virtual void clear(void)=0
static locationt successor(locationt l)
std::vector< exprt > operandst
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
bool seen(const locationt &l)
goto_programt::const_targett locationt
exprt get_return_lhs(locationt to) const
Base class for all expressions.
void get_reference_set(const exprt &expr, expr_sett &expr_set)
virtual void initialize(const namespacet &ns)=0
flow_insensitive_analysist(const namespacet &_ns)
virtual ~flow_insensitive_analysis_baset()
virtual const statet & get_state() const
void put_in_working_set(working_sett &working_set, locationt l)
std::priority_queue< locationt > working_sett
recursion_sett recursion_set
virtual void get_reference_set(const namespacet &ns, const exprt &expr, expr_sett &expr_set)