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()(goto_programt::const_targett t)
local_may_aliast & operator()(const irep_idt &fkt)
std::map< goto_programt::const_targett, irep_idt, goto_programt::target_less_than > target_mapt
local_may_alias_factoryt()
void operator()(const goto_functionst &_goto_functions)
std::map< irep_idt, std::unique_ptr< local_may_aliast > > fkt_mapt
const goto_functionst * goto_functions
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
bool merge(const loc_infot &src)
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)
void build(const goto_functiont &goto_function)
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
std::stack< local_cfgt::node_nrt > work_queuet
std::vector< loc_infot > loc_infost
local_may_aliast(const goto_functiont &_goto_function)
unsigned_union_find alias_sett
bool aliases(const goto_programt::const_targett t, const exprt &src1, const exprt &src2) const
std::set< unsigned > object_sett
goto_functionst::goto_functiont goto_functiont
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)