12 #ifndef CPROVER_ANALYSES_STATIC_ANALYSIS_H 13 #define CPROVER_ANALYSES_STATIC_ANALYSIS_H 15 #ifndef USE_DEPRECATED_STATIC_ANALYSIS_H 16 #error Deprecated, use ai.h instead 22 #include <unordered_set> 66 std::ostream &out)
const 70 typedef std::unordered_set<exprt, irep_hash>
expr_sett;
76 std::list<exprt> &dest)
149 std::ostream &out)
const;
153 std::ostream &out)
const 180 std::ostream &out)
const;
191 std::pair<unsigned, locationt>(l->location_number, l));
241 const exprt &
function,
249 const goto_functionst::function_mapt::const_iterator f_it,
265 std::list<exprt> &dest)=0;
283 typename state_mapt::iterator it=
state_map.find(l);
285 throw "failed to find state";
292 typename state_mapt::const_iterator it=
state_map.find(l);
294 throw "failed to find state";
316 typename state_mapt::iterator it=
state_map.find(l);
318 throw "failed to find state";
325 typename state_mapt::const_iterator it=
state_map.find(l);
327 throw "failed to find state";
334 return static_cast<T &
>(a).
merge(static_cast<const T &>(b), to);
339 return util_make_unique<T>(
static_cast<T &
>(s));
350 std::list<exprt> &dest)
370 throw "not implemented";
391 static_cast<const T &>(b),
402 #endif // CPROVER_ANALYSES_STATIC_ANALYSIS_H
static exprt get_guard(locationt from, locationt to)
virtual std::unique_ptr< statet > make_temporary_state(statet &s)=0
std::map< unsigned, locationt > working_sett
std::map< locationt, T > state_mapt
virtual statet & get_state(locationt l)=0
recursion_sett recursion_set
void sequential_fixedpoint(const goto_functionst &goto_functions)
virtual void transform(const namespacet &ns, locationt from, locationt to)=0
Goto Programs with Functions.
virtual void output(const goto_functionst &goto_functions, std::ostream &out) const
domain_baset::expr_sett expr_sett
virtual std::unique_ptr< statet > make_temporary_state(statet &s)
virtual bool merge_shared(statet &a, const statet &b, locationt to)=0
static exprt get_return_lhs(locationt to)
bool fixedpoint(const goto_programt &goto_program, const goto_functionst &goto_functions)
goto_programt::const_targett locationt
virtual bool has_location(locationt l) const =0
static_analysist(const namespacet &_ns)
virtual const statet & get_state(locationt l) const
virtual void generate_state(locationt l)=0
functions_donet functions_done
concurrency_aware_static_analysist(const namespacet &_ns)
void do_function_call_rec(locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
void put_in_working_set(working_sett &working_set, locationt l)
goto_programt::const_targett locationt
virtual bool merge(statet &a, const statet &b, locationt to)=0
virtual void fixedpoint(const goto_functionst &goto_functions)
virtual void fixedpoint(const goto_functionst &goto_functions)
virtual void get_reference_set(const namespacet &ns, const exprt &expr, std::list< exprt > &dest)
instructionst::const_iterator const_targett
void concurrent_fixedpoint(const goto_functionst &goto_functions)
std::unordered_set< exprt, irep_hash > expr_sett
virtual bool merge_shared(statet &a, const statet &b, goto_programt::const_targett to)
goto_programt::const_targett locationt
void output(const goto_programt &goto_program, std::ostream &out) const
virtual bool has_location(locationt l) const
virtual void get_reference_set(locationt l, const exprt &expr, std::list< exprt > &dest)=0
std::set< irep_idt > recursion_sett
const T & operator[](locationt l) const
std::vector< exprt > operandst
void generate_states(const goto_functionst &goto_functions)
T & operator[](locationt l)
A generic container class for the GOTO intermediate representation of one function.
virtual void output(const namespacet &ns, std::ostream &out) const
virtual bool merge(statet &a, const statet &b, locationt to)
static locationt successor(locationt l)
std::set< irep_idt > functions_donet
virtual void get_reference_set(locationt l, const exprt &expr, std::list< exprt > &dest)
Base class for all expressions.
virtual void operator()(const goto_programt &goto_program)
virtual ~static_analysis_baset()
virtual void initialize(const goto_functionst &goto_functions)
virtual void update(const goto_programt &goto_program)
virtual void initialize(const namespacet &ns, locationt l)
goto_programt & goto_program
virtual void generate_state(locationt l)
locationt get_next(working_sett &working_set)
void do_function_call(locationt l_call, locationt l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state)
virtual statet & get_state(locationt l)
virtual void initialize(const goto_programt &goto_program)
virtual bool merge_shared(static_analysis_baset::statet &a, const static_analysis_baset::statet &b, goto_programt::const_targett to)
bool visit(locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
static_analysis_baset(const namespacet &_ns)