cprover
symex_main.cpp File Reference

Symbolic Execution. More...

#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>
+ Include dependency graph for symex_main.cpp:

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)
 

Detailed Description

Symbolic Execution.

Definition in file symex_main.cpp.

Function Documentation

◆ get_function_from_goto_functions()

static goto_symext::get_goto_functiont get_function_from_goto_functions ( const goto_functionst goto_functions)
static

Definition at line 218 of file symex_main.cpp.

◆ switch_to_thread()

static void switch_to_thread ( goto_symex_statet state,
const unsigned int  thread_nb 
)
static

Definition at line 177 of file symex_main.cpp.

◆ symex_transition() [1/2]

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.

◆ symex_transition() [2/2]

void symex_transition ( goto_symext::statet state)

Definition at line 66 of file symex_main.cpp.