17 const std::string &property,
18 const std::string &msg,
29 if(expr.
id()==ID_symbol &&
40 ptr_symbol.
type.
get(
"#failed_symbol");
42 if(failed_symbol!=
"" &&
43 !ns.
lookup(failed_symbol, symbol))
55 else if(expr.
id()==ID_symbol)
61 ptr_symbol.
type.
get(
"#failed_symbol");
63 if(failed_symbol!=
"" &&
64 !ns.
lookup(failed_symbol, symbol))
87 std::cout <<
"**************************\n";
89 std::cout <<
"**************************\n";
97 std::cout <<
"**************************\n";
98 for(value_setst::valuest::const_iterator it=value_set.begin();
102 std::cout <<
"**************************\n";
goto_symext::statet & state
irep_idt name
The unique identifier.
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
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
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
const irep_idt & id() const
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
virtual void get_value_set(const exprt &expr, value_setst::valuest &value_set)
const irep_idt & get(const irep_namet &name) const
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
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)
symbol_tablet & new_symbol_table
typet type
Type of symbol.
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const exprt & get_original_expr() const
Expression to hold a symbol (variable)
void output(const namespacet &ns, std::ostream &out) const
std::list< exprt > valuest
Expression providing an SSA-renamed symbol of expressions.
Symbolic Execution of ANSI-C.