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 21 #include <unordered_set> 63 std::ostream &out)
const 67 typedef std::unordered_set<exprt, irep_hash>
expr_sett;
73 std::list<exprt> &dest)
112 generate_states(goto_program);
122 generate_states(goto_functions);
129 virtual void operator()(
132 virtual void operator()(
146 std::ostream &out)
const;
150 std::ostream &out)
const 152 output(goto_program,
"", out);
155 virtual bool has_location(locationt l)
const=0;
165 static exprt get_guard(locationt from, locationt to);
169 static exprt get_return_lhs(locationt to);
177 std::ostream &out)
const;
181 locationt get_next(working_sett &working_set);
184 working_sett &working_set,
188 std::pair<unsigned, locationt>(l->location_number, l));
196 virtual void fixedpoint(
199 void sequential_fixedpoint(
201 void concurrent_fixedpoint(
207 working_sett &working_set,
217 virtual bool merge(statet &a,
const statet &b, locationt to)=0;
219 virtual bool merge_shared(statet &a,
const statet &b, locationt to)=0;
227 void generate_states(
230 void generate_states(
236 void do_function_call_rec(
237 locationt l_call, locationt l_return,
238 const exprt &
function,
243 void do_function_call(
244 locationt l_call, locationt l_return,
246 const goto_functionst::function_mapt::const_iterator f_it,
252 virtual void generate_state(locationt l)=0;
253 virtual statet &get_state(locationt l)=0;
254 virtual const statet &get_state(locationt l)
const=0;
255 virtual statet* make_temporary_state(statet &s)=0;
262 std::list<exprt> &dest)=0;
280 typename state_mapt::iterator it=state_map.find(l);
281 if(it==state_map.end())
282 throw "failed to find state";
289 typename state_mapt::const_iterator it=state_map.find(l);
290 if(it==state_map.end())
291 throw "failed to find state";
304 return state_map.count(l)!=0;
313 typename state_mapt::iterator it=state_map.find(l);
314 if(it==state_map.end())
315 throw "failed to find state";
322 typename state_mapt::const_iterator it=state_map.find(l);
323 if(it==state_map.end())
324 throw "failed to find state";
331 return static_cast<T &
>(a).merge(static_cast<const T &>(b), to);
336 return new T(static_cast<T &>(s));
341 state_map[l].initialize(ns, l);
347 std::list<exprt> &dest)
349 state_map[l].get_reference_set(ns, expr, dest);
354 sequential_fixedpoint(goto_functions);
367 throw "not implemented";
386 return static_cast<T &
>(a).merge_shared(
388 static_cast<const T &>(b),
395 this->concurrent_fixedpoint(goto_functions);
399 #endif // CPROVER_ANALYSES_STATIC_ANALYSIS_H
std::map< unsigned, locationt > working_sett
std::map< locationt, T > state_mapt
recursion_sett recursion_set
virtual void transform(const namespacet &ns, locationt from, locationt to)=0
Goto Programs with Functions.
domain_baset::expr_sett expr_sett
goto_programt::const_targett locationt
static_analysist(const namespacet &_ns)
virtual const statet & get_state(locationt l) const
functions_donet functions_done
concurrency_aware_static_analysist(const namespacet &_ns)
instructionst::const_iterator const_targett
void put_in_working_set(working_sett &working_set, locationt l)
goto_programt::const_targett locationt
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)
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
std::set< irep_idt > recursion_sett
const T & operator[](locationt l) const
virtual statet * make_temporary_state(statet &s)
std::vector< exprt > operandst
T & operator[](locationt l)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
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 ~static_analysis_baset()
virtual void initialize(const goto_functionst &goto_functions)
virtual void initialize(const namespacet &ns, locationt l)
virtual void generate_state(locationt l)
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)
static_analysis_baset(const namespacet &_ns)