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 )