12#ifndef CPROVER_ANALYSES_LOCAL_MAY_ALIAS_H
13#define CPROVER_ANALYSES_LOCAL_MAY_ALIAS_H
31 dirty(_goto_function),
33 cfg(_goto_function.body)
35 build(_goto_function);
50 const exprt &src)
const;
105 for(
const auto &gf_entry : _goto_functions.
function_map)
115 fkt_mapt::iterator f_it=
fkt_map.find(fkt);
117 return *f_it->second;
119 goto_functionst::function_mapt::const_iterator f_it2=
122 return *(
fkt_map[fkt] = std::make_unique<local_may_aliast>(f_it2->second));
127 target_mapt::const_iterator t_it=
135 const exprt &src)
const;
139 typedef std::map<irep_idt, std::unique_ptr<local_may_aliast> >
fkt_mapt;
143 map<goto_programt::const_targett, irep_idt, goto_programt::target_less_than>
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
instructionst::const_iterator const_targett
local_may_aliast & operator()(const irep_idt &fkt)
local_may_aliast & operator()(goto_programt::const_targett t)
local_may_alias_factoryt()
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
void operator()(const goto_functionst &_goto_functions)
std::map< goto_programt::const_targett, irep_idt, goto_programt::target_less_than > target_mapt
std::map< irep_idt, std::unique_ptr< local_may_aliast > > fkt_mapt
const goto_functionst * goto_functions
bool merge(const loc_infot &src)
std::set< unsigned > object_sett
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
void assign_lhs(const exprt &lhs, const exprt &rhs, const loc_infot &loc_info_src, loc_infot &loc_info_dest)
std::vector< loc_infot > loc_infost
void build(const goto_functiont &goto_function)
std::stack< local_cfgt::node_nrt > work_queuet
numberingt< exprt, irep_hash > objects
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
void get_rec(object_sett &dest, const exprt &rhs, const loc_infot &loc_info_src) const
local_may_aliast(const goto_functiont &_goto_function)
goto_functionst::goto_functiont goto_functiont
unsigned_union_find alias_sett
bool aliases(const goto_programt::const_targett t, const exprt &src1, const exprt &src2) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Variables whose address is taken.
#define forall_goto_program_instructions(it, program)
Local variables whose address is taken.
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)