29 if(expr.
id()==ID_symbol &&
39 const irep_idt &failed_symbol = ptr_symbol.
type.
get(ID_C_failed_symbol);
41 if(failed_symbol!=
"" &&
42 !ns.
lookup(failed_symbol, symbol))
54 else if(expr.
id()==ID_symbol)
59 const irep_idt &failed_symbol = ptr_symbol.
type.
get(ID_C_failed_symbol);
61 if(failed_symbol!=
"" &&
62 !ns.
lookup(failed_symbol, symbol))
85 std::cout <<
"**************************\n";
87 std::cout <<
"**************************\n";
95 std::cout <<
"**************************\n";
96 for(value_setst::valuest::const_iterator it=value_set.begin();
100 std::cout <<
"**************************\n";
goto_symext::statet & state
irep_idt name
The unique identifier.
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
const irep_idt & get_identifier() const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void get_value_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
bool get_bool(const irep_namet &name) const
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
const irep_idt & id() const
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
virtual void get_value_set(const exprt &expr, value_setst::valuest &value_set)
const irep_idt & get(const irep_namet &name) const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
virtual bool has_failed_symbol(const exprt &expr, const symbolt *&symbol)
virtual void dereference_failure(const std::string &property, const std::string &msg, const guardt &guard)
typet type
Type of symbol.
Base class for all expressions.
const exprt & get_original_expr() const
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc...
Expression to hold a symbol (variable)
void output(const namespacet &ns, std::ostream &out) const
Pretty-print this value-set.
std::list< exprt > valuest
Expression providing an SSA-renamed symbol of expressions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Symbolic Execution of ANSI-C.