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 "symex_target_equation.h"

Include dependency graph for goto_symex_state.cpp:

Go to the source code of this file.

Functions
static void	get_l1_name (exprt &expr)
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. More...

Detailed Description

Symbolic Execution.

Definition in file goto_symex_state.cpp.

Function Documentation

get_l1_name()

static void get_l1_name ( exprt &  expr )

static

Definition at line 786 of file goto_symex_state.cpp.

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 658 of file goto_symex_state.cpp.