goto_symex_state.cpp File Reference

Symbolic Execution. More...

#include "goto_symex_state.h"
#include <cstdlib>
#include <iostream>
#include <util/base_exceptions.h>
#include <util/exception_utils.h>
#include <util/expr_util.h>
#include <util/format.h>
#include <util/format_expr.h>
#include <util/invariant.h>
#include <util/prefix.h>
#include <util/std_expr.h>
#include <analyses/dirty.h>

Include dependency graph for goto_symex_state.cpp:

Go to the source code of this file.

Classes
class	goto_symex_is_constantt

Functions
static void	get_l1_name (exprt &expr)
static bool	check_renaming (const exprt &expr)
	write to a variable More...
static bool	check_renaming (const typet &type)
static bool	check_renaming_l1 (const exprt &expr)

Detailed Description

Symbolic Execution.

Definition in file goto_symex_state.cpp.

Function Documentation

check_renaming() [1/2]

static bool check_renaming ( const exprt &  expr )

static

write to a variable

Definition at line 90 of file goto_symex_state.cpp.

check_renaming() [2/2]

static bool check_renaming ( const typet &  type )

static

Definition at line 48 of file goto_symex_state.cpp.

check_renaming_l1()

static bool check_renaming_l1 ( const exprt &  expr )

static

Definition at line 66 of file goto_symex_state.cpp.

get_l1_name()

static void get_l1_name ( exprt &  expr )

static

Definition at line 755 of file goto_symex_state.cpp.