symex_function_call.cpp File Reference

#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/prefix.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	locality (const irep_idt &function_identifier, goto_symext::statet &state, path_storaget &path_storage, const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
	Preserves locality of parameters of a given function by applying L1 renaming to them. More...
static void	pop_frame (goto_symext::statet &state, const path_storaget &path_storage, bool doing_path_exploration)
	pop one call frame More...

Detailed Description

Symbolic Execution of ANSI-C

Definition in file symex_function_call.cpp.

Function Documentation

locality()

static void locality ( const irep_idt &  function_identifier, goto_symext::statet &  state, path_storaget &  path_storage, const goto_functionst::goto_functiont &  goto_function, const namespacet &  ns  )

static

Preserves locality of parameters of a given function by applying L1 renaming to them.

Definition at line 457 of file symex_function_call.cpp.

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 374 of file symex_function_call.cpp.