12 #ifndef CPROVER_ANALYSES_AI_H 13 #define CPROVER_ANALYSES_AI_H 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;
280 std::pair<unsigned, locationt>(l->location_number, l));
314 const exprt &
function,
322 const goto_functionst::function_mapt::const_iterator f_it,
341 template<
typename domainT>
354 typename state_mapt::iterator it=
state_map.find(l);
356 throw "failed to find state";
363 typename state_mapt::const_iterator it=
state_map.find(l);
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);
391 throw "failed to find state";
399 return static_cast<domainT &
>(dest).
merge(
400 static_cast<const domainT &>(src), from, to);
405 return new domainT(static_cast<const domainT &>(s));
426 throw "not implemented";
430 template<
typename domainT>
449 static_cast<const domainT &>(src), from, to, ns);
461 #endif // CPROVER_ANALYSES_AI_H const domainT & operator[](locationt l) const
virtual statet & get_state(locationt l)=0
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
virtual bool merge(const statet &src, locationt from, locationt to)=0
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 jsont output_json(const namespacet &ns, const goto_functionst &goto_functions) const
Output the domains for the whole program as JSON.
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
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
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
bool do_function_call_rec(locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, const goto_functionst &goto_functions, const namespacet &ns)
bool 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, const namespacet &ns)
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 entry_state(const goto_programt &)
virtual const statet & find_state(locationt l) const =0
virtual bool merge_shared(const statet &src, locationt from, locationt to, const namespacet &ns)=0
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
void sequential_fixedpoint(const goto_functionst &goto_functions, const namespacet &ns)
std::vector< exprt > operandst
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
bool fixedpoint(const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
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
bool visit(locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
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
locationt get_next(working_sett &working_set)
const statet & find_state(locationt l) const override
void output(const goto_modelt &goto_model, std::ostream &out) const
virtual statet * make_temporary_state(const statet &s)=0
virtual void initialize(const goto_programt &)
virtual ~ai_domain_baset()
void output(const namespacet &ns, const goto_programt &goto_program, std::ostream &out) const
void concurrent_fixedpoint(const goto_functionst &goto_functions, const namespacet &ns)
goto_programt::const_targett locationt
recursion_sett recursion_set
virtual xmlt output_xml(const namespacet &ns, const goto_functionst &goto_functions) const
Output the domains for the whole program as XML.
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