35 typedef std::list<value_set_fit::entryt>
entry_listt;
46 typedef std::unordered_map<irep_idt, entry_listt>
entry_cachet;
51 for(goto_programt::instructionst::const_iterator
58 for(goto_programt::decl_identifierst::const_iterator
82 std::list<value_set_fit::entryt> &
dest)
89 const std::string &suffix,
91 std::list<value_set_fit::entryt> &
dest)
119 std::list<value_set_fit::entryt>
globals;
128 std::set<irep_idt> locals;
135 std::list<value_set_fit::entryt> entries;
143 std::list<value_set_fit::entryt> &
dest)
162 {
return true;
break; }
167 const typet *t = &type;
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
const typet & element_type() const
The type of the elements of the array.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
goto_programt::const_targett locationt
virtual void initialize(const goto_programt &)
value_set_domain_fit state
A collection of goto functions.
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
std::set< irep_idt > decl_identifierst
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
const irep_idt & id() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
const typet & base_type() const
The type of the data what we point to.
const componentst & components() const
const symbolst & symbols
Read-only field, used to look up symbols given their names.
typet type
Type of symbol.
irep_idt name
The unique identifier.
The type of an expression, extends irept.
bool check_type(const typet &type)
std::vector< exprt > get_values(const irep_idt &function_id, locationt l, const exprt &expr) override
void get_entries(const symbolt &symbol, std::list< value_set_fit::entryt > &dest)
void add_vars(const goto_functionst &goto_functions)
void get_entries_rec(const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fit::entryt > &dest)
void get_globals(std::list< value_set_fit::entryt > &dest)
@ TRACK_FUNCTION_POINTERS
track_optionst track_options
void initialize(const goto_programt &goto_program) override
static numberingt< irep_idt > function_numbering
void add_vars(const std::list< entryt > &vars)
std::vector< exprt > get_value_set(const exprt &expr, const namespacet &ns) const
unsigned from_target_index
void get_local_identifiers(const goto_functiont &goto_function, std::set< irep_idt > &dest)
Return in dest the identifiers of the local variables declared in the goto_function and the identifie...
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Value Set Propagation (flow insensitive)