Loading...

Searching...

No Matches

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 435 of file symex_dereference.cpp.