12 #ifndef CPROVER_ANALYSES_AI_H 13 #define CPROVER_ANALYSES_AI_H 94 virtual bool is_top()
const=0;
179 fixedpoint(goto_function.body, goto_functions, ns);
201 std::ostream &out)
const;
205 std::ostream &out)
const 214 std::ostream &out)
const 222 std::ostream &out)
const 224 output(ns, goto_function.body,
"", out);
276 return output_xml(ns, goto_function.body,
"");
295 std::ostream &out)
const;
318 std::pair<unsigned, locationt>(l->location_number, l));
349 const exprt &
function,
357 const goto_functionst::function_mapt::const_iterator f_it,
376 template<
typename domainT>
389 typename state_mapt::iterator it=
state_map.find(l);
391 throw "failed to find state";
398 typename state_mapt::const_iterator it=
state_map.find(l);
400 throw "failed to find state";
419 unordered_map<locationt, domainT, const_target_hash, pointee_address_equalt>
432 typename state_mapt::const_iterator it=
state_map.find(l);
434 throw "failed to find state";
442 return static_cast<domainT &
>(dest).
merge(
443 static_cast<const domainT &>(src), from, to);
448 return util_make_unique<domainT>(
static_cast<const domainT &
>(s));
469 throw "not implemented";
473 template<
typename domainT>
492 static_cast<const domainT &>(src), from, to, ns);
504 #endif // CPROVER_ANALYSES_AI_H const domainT & operator[](locationt l) const
virtual statet & get_state(locationt l)=0
virtual bool is_top() const =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
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
virtual const ai_domain_baset & abstract_state_after(goto_programt::const_targett t) const
Returns the abstract state after the given instruction.
virtual jsont output_json(const ai_baset &ai, const namespacet &ns) const
std::unique_ptr< statet > make_temporary_state(const statet &s) override
void output(const namespacet &ns, const goto_functionst::goto_functiont &goto_function, std::ostream &out) const
symbol_tablet symbol_table
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 bool is_bottom() const =0
virtual void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0
std::unordered_map< locationt, domainT, const_target_hash, pointee_address_equalt > state_mapt
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)
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
instructionst::const_iterator const_targett
::goto_functiont goto_functiont
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)
void sequential_fixedpoint(const goto_functionst &goto_functions, const namespacet &ns)
std::vector< exprt > operandst
A generic container class for the GOTO intermediate representation of one function.
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)
virtual std::unique_ptr< statet > make_temporary_state(const statet &s)=0
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
const ai_domain_baset & abstract_state_before(goto_programt::const_targett t) const override
Returns the abstract state before the given instruction.
void output(const goto_modelt &goto_model, std::ostream &out) const
virtual void initialize(const goto_programt &)
goto_programt & goto_program
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
virtual const ai_domain_baset & abstract_state_before(goto_programt::const_targett t) const =0
Returns the abstract state before the given instruction.
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
GOTO functions.
jsont output_json(const namespacet &ns, const goto_programt &goto_program) const
virtual void make_entry()=0