Go to the documentation of this file.
12 #ifndef CPROVER_ANALYSES_LOCAL_MAY_ALIAS_H
13 #define CPROVER_ANALYSES_LOCAL_MAY_ALIAS_H
32 dirty(_goto_function),
34 cfg(_goto_function.body)
36 build(_goto_function);
51 const exprt &src)
const;
114 fkt_mapt::iterator f_it=
fkt_map.find(fkt);
116 return *f_it->second;
118 goto_functionst::function_mapt::const_iterator f_it2=
121 return *(
fkt_map[fkt]=util_make_unique<local_may_aliast>(f_it2->second));
126 target_mapt::const_iterator t_it=
134 const exprt &src)
const;
138 typedef std::map<irep_idt, std::unique_ptr<local_may_aliast> >
fkt_mapt;
141 typedef std::map<goto_programt::const_targett, irep_idt >
target_mapt;
145 #endif // CPROVER_ANALYSES_LOCAL_MAY_ALIAS_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
std::map< goto_programt::const_targett, irep_idt > target_mapt
Variables whose address is taken.
unsigned_union_find alias_sett
local_may_alias_factoryt()
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
void operator()(const goto_functionst &_goto_functions)
Base class for all expressions.
function_mapt function_map
local_may_aliast & operator()(goto_programt::const_targett t)
local_may_aliast(const goto_functiont &_goto_function)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::vector< loc_infot > loc_infost
#define PRECONDITION(CONDITION)
Local variables whose address is taken.
bool aliases(const goto_programt::const_targett t, const exprt &src1, const exprt &src2) const
void build(const goto_functiont &goto_function)
const goto_functionst * goto_functions
goto_functionst::goto_functiont goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
std::stack< local_cfgt::node_nrt > work_queuet
void assign_lhs(const exprt &lhs, const exprt &rhs, const loc_infot &loc_info_src, loc_infot &loc_info_dest)
bool merge(const loc_infot &src)
::goto_functiont goto_functiont
A collection of goto functions.
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
numbering< exprt > objects
std::set< unsigned > object_sett
#define forall_goto_functions(it, functions)
instructionst::const_iterator const_targett
local_may_aliast & operator()(const irep_idt &fkt)
std::map< irep_idt, std::unique_ptr< local_may_aliast > > fkt_mapt
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
#define forall_goto_program_instructions(it, program)
void get_rec(object_sett &dest, const exprt &rhs, const loc_infot &loc_info_src) const