goto_symex.h File Reference

#include <goto-programs/goto_functions.h>
#include <util/base/threeval.h>
#include <goto-programs/abstract-interpretation/interval_domain.h>
#include <goto-symex/state/goto_symex_state.h>
#include <goto-symex/equation/symex_target.h>
#include <functional>
#include <map>
#include <optional>
#include <pointer-analysis/dereference.h>
#include <util/base/i2string.h>
#include <irep2/irep2.h>
#include <util/config/options.h>
#include <util/irep/std_types.h>

Include dependency graph for goto_symex.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	inductive_step_disabled_exceptiont
class	goto_symext
	Primay symbolic execution class. More...
class	goto_symext::allocated_obj
	Records for dynamically allocated blobs of memory. More...
class	goto_symext::symex_resultt
	Class recording the outcome of symbolic execution. More...
struct	goto_symext::deferred_assumptiont
class	symex_dereference_statet

Namespaces
namespace	goto_symex_utils

Functions
expr2tc	goto_symex_utils::gen_byte_memcpy (const expr2tc &src, const expr2tc &dst, const size_t num_of_bytes, const size_t src_offset, const size_t dst_offset)
	Computes the equivalent object value when considering a memcpy operation on it.
bool	goto_symex_utils::is_alloca_return_value_name (const std::string &name)
	Returns true iff name is the goto-program return-value temp for an alloca / __builtin_alloca call, i.e.