symex_function_call.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/fresh_symbol.h>
#include <util/invariant.h>
#include <util/range.h>
#include <util/std_code.h>
#include "expr_skeleton.h"
#include "path_storage.h"
#include "symex_assign.h"

Include dependency graph for symex_function_call.cpp:

Go to the source code of this file.

Functions
static void	pop_frame (goto_symext::statet &state, const path_storaget &path_storage, bool doing_path_exploration)
	pop one call frame

Detailed Description

Symbolic Execution of ANSI-C.

Definition in file symex_function_call.cpp.

Function Documentation

pop_frame()

static void pop_frame ( goto_symext::statet &  state, const path_storaget &  path_storage, bool  doing_path_exploration  )

static

pop one call frame

Definition at line 387 of file symex_function_call.cpp.