symex_clean_expr.cpp File Reference

Symbolic Execution of ANSI-C. More...

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

Include dependency graph for symex_clean_expr.cpp:

Go to the source code of this file.

Functions
static void	process_array_expr (exprt &expr, const namespacet &ns)
	Given an expression, find the root object and the offset into it.
static void	adjust_byte_extract_rec (exprt &expr, const namespacet &ns)
	Rewrite index/member expressions in byte_extract to offset.
static void	replace_nondet (exprt &expr, symex_nondet_generatort &build_symex_nondet)

Detailed Description

Symbolic Execution of ANSI-C.

Definition in file symex_clean_expr.cpp.

Function Documentation

adjust_byte_extract_rec()

static void adjust_byte_extract_rec ( exprt &  expr, const namespacet &  ns  )

static

Rewrite index/member expressions in byte_extract to offset.

Definition at line 142 of file symex_clean_expr.cpp.

process_array_expr()

static void process_array_expr ( exprt &  expr, const namespacet &  ns  )

static

Given an expression, find the root object and the offset into it.

The extra complication to be considered here is that the expression may have any number of ternary expressions mixed with type casts.

Definition at line 30 of file symex_clean_expr.cpp.

replace_nondet()

static void replace_nondet ( exprt &  expr, symex_nondet_generatort &  build_symex_nondet  )

static

Definition at line 164 of file symex_clean_expr.cpp.