cprover
goto_symex.h File Reference
+ 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 ,
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.