Loading...

Searching...

No Matches

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.