Go to the documentation of this file.
37 if(expr.
id()==ID_symbol &&
47 const irep_idt &failed_symbol = ptr_symbol.
type.
get(ID_C_failed_symbol);
50 if(!failed_symbol.
empty() && !
ns.
lookup(failed_symbol, symbol))
61 else if(expr.
id()==ID_symbol)
66 const irep_idt &failed_symbol = ptr_symbol.
type.
get(ID_C_failed_symbol);
69 if(!failed_symbol.
empty() && !
ns.
lookup(failed_symbol, symbol))
92 std::cout <<
"symex_dereference_statet state.value_set={\n";
94 std::cout <<
"}" << std::endl;
102 std::cout <<
"**************************\n";
103 for(value_setst::valuest::const_iterator it=value_set.begin();
107 std::cout <<
"**************************\n";
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void get_value_set(exprt expr, value_setst::valuest &dest, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
goto_symext::statet & state
typet type
Type of symbol.
const symbolt * get_or_create_failed_symbol(const exprt &expr) override
Get or create a failed symbol for the given pointer-typed expression.
Base class for all expressions.
NODISCARD renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
Symbolic Execution of ANSI-C.
const exprt & get_original_expr() const
Expression providing an SSA-renamed symbol of expressions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
bool get_bool(const irep_namet &name) const
std::list< exprt > valuest
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
void output(std::ostream &out, const std::string &indent="") const
Pretty-print this value-set.
const irep_idt & get_identifier() const
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
void get_value_set(const exprt &expr, value_setst::valuest &value_set) const override
Just forwards a value-set query to state.value_set
const irep_idt & get(const irep_namet &name) const
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
irep_idt name
The unique identifier.