goto_symex.h File Reference

Symbolic Execution. More...

#include <util/message.h>
#include "complexity_limiter.h"
#include "shadow_memory.h"
#include "symex_config.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	goto_symext
	The main class for the forward symbolic simulator. More...

Functions
void	symex_transition (goto_symext::statet &state)
	Transition to the next instruction, which increments the internal program counter and initializes the loop counter when it detects a loop (or recursion) being entered.
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,
		goto_programt::const_targett	to,
		bool	is_backwards_goto
	)

Definition at line 73 of file symex_main.cpp.

symex_transition() [2/2]

void symex_transition

(

goto_symext::statet &

state

)

Transition to the next instruction, which increments the internal program counter and initializes the loop counter when it detects a loop (or recursion) being entered.

'Next instruction' in this situation refers to the next one in program order, so it ignores things like unconditional GOTOs, and only goes until the end of the current function.

Parameters

state

Symbolic execution state to be transformed

Definition at line 144 of file symex_main.cpp.