goto_symex.h File Reference

Symbolic Execution. More...

#include <util/options.h>
#include <util/message.h>
#include <goto-programs/goto_functions.h>
#include "goto_symex_state.h"
#include "path_storage.h"
#include "symex_target_equation.h"

Include dependency graph for goto_symex.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	symex_nondet_generatort
	Functor generating fresh nondet symbols. More...
struct	symex_configt
	Configuration of the symbolic execution. More...
class	goto_symext
	The main class for the forward symbolic simulator. More...

Functions
void	symex_transition (goto_symext::statet &state)
void	symex_transition (goto_symext::statet &, goto_programt::const_targett to, bool is_backwards_goto)

Detailed Description

Symbolic Execution.

Definition in file goto_symex.h.

Function Documentation

symex_transition() [1/2]

void symex_transition

(

goto_symext::statet &

state

)

Definition at line 66 of file symex_main.cpp.

symex_transition() [2/2]

void symex_transition	(	goto_symext::statet &	,
		goto_programt::const_targett	to,
		bool	is_backwards_goto
	)

Definition at line 42 of file symex_main.cpp.