12 #ifndef CPROVER_ANALYSES_AI_H 13 #define CPROVER_ANALYSES_AI_H 127 initialize(goto_program);
128 entry_state(goto_program);
129 fixedpoint(goto_program, goto_functions, ns);
136 initialize(goto_functions);
137 entry_state(goto_functions);
138 fixedpoint(goto_functions, ns);
154 initialize(goto_function);
155 entry_state(goto_function.body);
156 fixedpoint(goto_function.body, goto_functions, ns);
166 std::ostream &out)
const;
170 std::ostream &out)
const 179 std::ostream &out)
const 181 output(ns, goto_program,
"", out);
187 std::ostream &out)
const 189 output(ns, goto_function.body,
"", out);
241 return output_xml(ns, goto_function.body,
"");
257 std::ostream &out)
const;
273 locationt get_next(working_sett &working_set);
276 working_sett &working_set,
280 std::pair<unsigned, locationt>(l->location_number, l));
289 virtual void fixedpoint(
293 void sequential_fixedpoint(
296 void concurrent_fixedpoint(
303 working_sett &working_set,
312 bool do_function_call_rec(
313 locationt l_call, locationt l_return,
314 const exprt &
function,
319 bool do_function_call(
320 locationt l_call, locationt l_return,
322 const goto_functionst::function_mapt::const_iterator f_it,
328 virtual bool merge(
const statet &src, locationt from, locationt to)=0;
330 virtual bool merge_shared(
335 virtual statet &get_state(locationt l)=0;
336 virtual const statet &find_state(locationt l)
const=0;
337 virtual statet* make_temporary_state(
const statet &s)=0;
341 template<
typename domainT>
354 typename state_mapt::iterator it=state_map.find(l);
355 if(it==state_map.end())
356 throw "failed to find state";
363 typename state_mapt::const_iterator it=state_map.find(l);
364 if(it==state_map.end())
365 throw "failed to find state";
377 typedef std::unordered_map<locationt, domainT, const_target_hash>
state_mapt;
389 typename state_mapt::const_iterator it=state_map.find(l);
390 if(it==state_map.end())
391 throw "failed to find state";
396 bool merge(
const statet &src, locationt from, locationt to)
override 398 statet &dest=get_state(to);
399 return static_cast<domainT &
>(dest).merge(
400 static_cast<const domainT &>(src), from, to);
405 return new domainT(static_cast<const domainT &>(s));
412 sequential_fixedpoint(goto_functions, ns);
426 throw "not implemented";
430 template<
typename domainT>
447 statet &dest=this->get_state(to);
448 return static_cast<domainT &
>(dest).merge_shared(
449 static_cast<const domainT &>(src), from, to, ns);
457 this->concurrent_fixedpoint(goto_functions, ns);
461 #endif // CPROVER_ANALYSES_AI_H const domainT & operator[](locationt l) const
void dummy(const domainT &s)
void fixedpoint(const goto_functionst &goto_functions, const namespacet &ns) override
virtual statet & get_state(locationt l) override
virtual void make_bottom()=0
std::unordered_map< locationt, domainT, const_target_hash > state_mapt
void put_in_working_set(working_sett &working_set, locationt l)
goto_programt::const_targett locationt
goto_programt::const_targett locationt
std::set< irep_idt > recursion_sett
virtual jsont output_json(const ai_baset &ai, const namespacet &ns) const
void output(const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const
symbol_tablet symbol_table
virtual void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0
statet * make_temporary_state(const statet &s) override
std::map< unsigned, locationt > working_sett
bool merge_shared(const statet &src, goto_programt::const_targett from, goto_programt::const_targett to, const namespacet &ns) override
domainT & operator[](locationt l)
instructionst::const_iterator const_targett
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const
void operator()(const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
xmlt output_xml(const namespacet &ns, const goto_programt &goto_program) const
ait< domainT >::statet statet
void fixedpoint(const goto_functionst &goto_functions, const namespacet &ns) override
void operator()(const goto_modelt &goto_model)
goto_function_templatet< goto_programt > goto_functiont
std::vector< exprt > operandst
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
bool merge_shared(const statet &src, goto_programt::const_targett from, goto_programt::const_targett to, const namespacet &ns) override
bool merge(const statet &src, locationt from, locationt to) override
void operator()(const goto_programt &goto_program, const namespacet &ns)
jsont output_json(const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
virtual bool ai_simplify_lhs(exprt &condition, const namespacet &ns) const
Use the information in the domain to simplify the expression on the LHS of an assignment.
virtual xmlt output_xml(const ai_baset &ai, const namespacet &ns) const
Base class for all expressions.
virtual void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const
const statet & find_state(locationt l) const override
void output(const goto_modelt &goto_model, std::ostream &out) const
virtual ~ai_domain_baset()
void output(const namespacet &ns, const goto_programt &goto_program, std::ostream &out) const
goto_programt::const_targett locationt
recursion_sett recursion_set
xmlt output_xml(const goto_modelt &goto_model) const
void operator()(const goto_functionst &goto_functions, const namespacet &ns)
virtual void make_top()=0
xmlt output_xml(const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const
jsont output_json(const goto_modelt &goto_model) const
goto_functionst goto_functions
jsont output_json(const namespacet &ns, const goto_programt &goto_program) const
virtual void make_entry()=0