Go to the documentation of this file.
59 rhs=
exprt(ID_invalid);
71 const auto level2_it =
85 state.
source.
pc->source_location.get_hide();
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define PRECONDITION(CONDITION)
const code_declt & to_code_decl(const codet &code)
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets)
Transforms this value-set by executing executing the assignment lhs := rhs against it.
goto_programt::const_targett pc
symex_target_equationt & target
virtual void symex_decl(statet &)
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
Base class for all expressions.
irep_idt get_object_name() const
symex_targett::sourcet source
static void increase_counter(const current_namest::iterator &it)
Increase the counter corresponding to an identifier.
Expression to hold a symbol (variable)
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)
Declare a fresh variable.
exprt get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
Get the failed-dereference symbol for the given symbol.
Expression providing an SSA-renamed symbol of expressions.
std::map< irep_idt, exprt > propagation
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
unsigned atomic_section_id
const irep_idt & get_identifier() const
const irep_idt & id() const
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
Write to a shared variable ssa_object: we effectively assign a value from this thread to be visible b...
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Operator to return the address of an object.
This class represents an instruction in the GOTO intermediate representation.
current_namest current_names
Data structure for representing an arbitrary statement in a program.