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. More...
void	symex_transition (goto_symext::statet &, goto_programt::const_targett to, bool is_backwards_goto)
renamedt< exprt, L2 >	try_evaluate_pointer_comparisons (renamedt< exprt, L2 > condition, const value_sett &value_set, const irep_idt &language_mode, const namespacet &ns)
	Try to evaluate pointer comparisons where they can be trivially determined using the value-set. More...

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.

try_evaluate_pointer_comparisons()

renamedt<exprt, L2> try_evaluate_pointer_comparisons	(	renamedt< exprt, L2 >	condition,
		const value_sett &	value_set,
		const irep_idt &	language_mode,
		const namespacet &	ns
	)

Try to evaluate pointer comparisons where they can be trivially determined using the value-set.

This is optional as all it does is allow symex to resolve some comparisons itself and therefore create a simpler formula for the SAT solver.

Parameters

[in,out]	condition	An L2-renamed expression with boolean type
	value_set	The value-set for determining what pointer-typed symbols might possibly point to
	language_mode	The language mode
	ns	A namespace

Returns

The possibly modified condition

Definition at line 214 of file symex_goto.cpp.