12 #ifndef CPROVER_ANALYSES_AI_H 13 #define CPROVER_ANALYSES_AI_H 84 fixedpoint(goto_function.body, goto_functions, ns);
103 INVARIANT(!l->is_end_function(),
"No state after the last instruction");
115 std::ostream &out)
const;
119 std::ostream &out)
const 128 std::ostream &out)
const 136 std::ostream &out)
const 138 output(ns, goto_function.body,
"", out);
190 return output_xml(ns, goto_function.body,
"");
209 std::ostream &out)
const;
232 std::pair<unsigned, locationt>(l->location_number, l));
266 const exprt &
function,
274 const goto_functionst::function_mapt::const_iterator f_it,
293 template<
typename domainT>
306 typename state_mapt::iterator it=
state_map.find(l);
308 throw "failed to find state";
315 typename state_mapt::const_iterator it=
state_map.find(l);
317 throw "failed to find state";
324 typename state_mapt::const_iterator it =
state_map.find(t);
327 std::unique_ptr<statet> d = util_make_unique<domainT>();
332 return util_make_unique<domainT>(it->second);
343 unordered_map<locationt, domainT, const_target_hash, pointee_address_equalt>
356 typename state_mapt::const_iterator it=
state_map.find(l);
358 throw "failed to find state";
366 return static_cast<domainT &
>(dest).
merge(
367 static_cast<const domainT &>(src), from, to);
372 return util_make_unique<domainT>(
static_cast<const domainT &
>(s));
393 throw "not implemented";
397 template<
typename domainT>
416 static_cast<const domainT &>(src), from, to, ns);
428 #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
std::unique_ptr< statet > abstract_state_before(locationt t) const override
Accessing individual domains at particular locations (without needing to know what kind of domain or ...
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::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.
#define CHECK_RETURN(CONDITION)
virtual std::unique_ptr< statet > abstract_state_before(locationt l) const =0
Accessing individual domains at particular locations (without needing to know what kind of domain or ...
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 clear()
Resets the domain.
std::unordered_map< locationt, domainT, const_target_hash, pointee_address_equalt > state_mapt
#define INVARIANT(CONDITION, REASON)
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)
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
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)
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
Abstract Interpretation Domain.
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)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
bool merge_shared(const statet &, goto_programt::const_targett, goto_programt::const_targett, const namespacet &) override
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(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)
Running the interpreter.
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
The basic interface of an abstract interpreter.
Base class for all expressions.
locationt get_next(working_sett &working_set)
const statet & find_state(locationt l) const override
void clear() override
Resets the domain.
void output(const goto_modelt &goto_model, std::ostream &out) const
virtual void initialize(const goto_programt &)
goto_programt & goto_program
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)
virtual std::unique_ptr< statet > abstract_state_after(locationt l) const
Returns the abstract state after 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)
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