cprover
|
#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"
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) |
Symbolic Execution
Definition in file goto_symex.h.
void symex_transition | ( | goto_symext::statet & | , |
goto_programt::const_targett | to, | ||
bool | is_backwards_goto | ||
) |
Definition at line 42 of file symex_main.cpp.
void symex_transition | ( | goto_symext::statet & | state | ) |
Definition at line 66 of file symex_main.cpp.