symex_dereference.cpp File Reference

Symbolic Execution of ANSI-C. More...

#include "goto_symex.h"
#include <util/arith_tools.h>
#include <util/byte_operators.h>
#include <util/c_types.h>
#include <util/exception_utils.h>
#include <util/expr_util.h>
#include <util/fresh_symbol.h>
#include <util/invariant.h>
#include <util/pointer_offset_size.h>
#include <pointer-analysis/value_set_dereference.h>
#include "expr_skeleton.h"
#include "path_storage.h"
#include "symex_assign.h"
#include "symex_dereference_state.h"

Include dependency graph for symex_dereference.cpp:

Go to the source code of this file.

Functions
static exprt	apply_to_objects_in_dereference (exprt e, const std::function< exprt(exprt)> &f)

Detailed Description

Symbolic Execution of ANSI-C.

Definition in file symex_dereference.cpp.

Function Documentation

apply_to_objects_in_dereference()

static exprt apply_to_objects_in_dereference ( exprt  e, const std::function< exprt(exprt)> &  f  )

static

Definition at line 434 of file symex_dereference.cpp.