cprover
|
#include "goto_symex.h"
#include <cassert>
#include <memory>
#include <util/exception_utils.h>
#include <util/make_unique.h>
#include <util/replace_symbol.h>
#include <util/std_expr.h>
#include <util/string2int.h>
#include <util/symbol_table.h>
#include <analyses/dirty.h>
Go to the source code of this file.
Functions | |
void | symex_transition (goto_symext::statet &state, goto_programt::const_targett to, bool is_backwards_goto) |
void | symex_transition (goto_symext::statet &state) |
static void | switch_to_thread (goto_symex_statet &state, const unsigned int thread_nb) |
static goto_symext::get_goto_functiont | get_function_from_goto_functions (const goto_functionst &goto_functions) |
Symbolic Execution
Definition in file symex_main.cpp.
|
static |
Definition at line 218 of file symex_main.cpp.
|
static |
Definition at line 177 of file symex_main.cpp.
void symex_transition | ( | goto_symext::statet & | state | ) |
Definition at line 66 of file symex_main.cpp.
void symex_transition | ( | goto_symext::statet & | state, |
goto_programt::const_targett | to, | ||
bool | is_backwards_goto | ||
) |
Definition at line 42 of file symex_main.cpp.