goto_symex_state.cpp File Reference

Symbolic Execution. More...

#include "goto_symex_state.h"
#include <util/as_const.h>
#include <util/base_exceptions.h>
#include <util/byte_operators.h>
#include <util/c_types.h>
#include <util/exception_utils.h>
#include <util/expr_util.h>
#include <util/invariant.h>
#include <util/std_expr.h>
#include <analyses/dirty.h>
#include <pointer-analysis/add_failed_symbols.h>
#include "goto_symex_can_forward_propagate.h"
#include "simplify_expr_with_value_set.h"
#include "symex_target_equation.h"

Include dependency graph for goto_symex_state.cpp:

Go to the source code of this file.

Functions
static bool	requires_renaming (const typet &type, const namespacet &ns)
	Return true if, and only if, the type or one of its subtypes requires SSA renaming.

Detailed Description

Symbolic Execution.

Definition in file goto_symex_state.cpp.

Function Documentation

requires_renaming()

static bool requires_renaming ( const typet &  type, const namespacet &  ns  )

static

Return true if, and only if, the type or one of its subtypes requires SSA renaming.

Renaming is necessary when symbol expressions occur within the type, which is the case for arrays of non-constant size.

Definition at line 649 of file goto_symex_state.cpp.